Czajka, Łukasz A new coinductive confluence proof for infinitary lambda calculus. (English) Zbl 07199590 Log. Methods Comput. Sci. 16, No. 1, Paper No. 31, 31 p. (2020). MSC: 03B70 68-XX PDF BibTeX XML Cite \textit{Ł. Czajka}, Log. Methods Comput. Sci. 16, No. 1, Paper No. 31, 31 p. (2020; Zbl 07199590) Full Text: arXiv Link OpenURL
Uustalu, Tarmo; Veltri, Niccolò Finiteness and rational sequences, constructively. (English) Zbl 1418.68069 J. Funct. Program. 27, Paper No. e13, 20 p. (2017). MSC: 68N30 03F50 PDF BibTeX XML Cite \textit{T. Uustalu} and \textit{N. Veltri}, J. Funct. Program. 27, Paper No. e13, 20 p. (2017; Zbl 1418.68069) Full Text: DOI OpenURL
Firsov, Denis; Uustalu, Tarmo; Veltri, Niccolò Variations on Noetherianness. (English) Zbl 1477.68070 Atkey, Robert (ed.) et al., Proceedings of the sixth workshop on mathematically structured functional programming, MSFP 2016, Eindhoven, Netherlands, April 8, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 207, 76-88 (2016). MSC: 68N18 03F65 PDF BibTeX XML Cite \textit{D. Firsov} et al., Electron. Proc. Theor. Comput. Sci. (EPTCS) 207, 76--88 (2016; Zbl 1477.68070) Full Text: arXiv Link OpenURL
Coquand, Thierry; Siles, Vincent A decision procedure for regular expression equivalence in type theory. (English) Zbl 1350.68228 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 119-134 (2011). MSC: 68T15 PDF BibTeX XML Cite \textit{T. Coquand} and \textit{V. Siles}, Lect. Notes Comput. Sci. 7086, 119--134 (2011; Zbl 1350.68228) Full Text: DOI OpenURL