Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L. Bar induction is compatible with constructive type theory. (English) Zbl 1427.03066 J. ACM 66, No. 2, Article No. 13, 35 p. (2019). MSC: 03F50 03B38 68V15 PDFBibTeX XMLCite \textit{V. Rahli} et al., J. ACM 66, No. 2, Article No. 13, 35 p. (2019; Zbl 1427.03066) Full Text: DOI
Constable, Robert L. Partial functions in constructive formal theories. (English) Zbl 0505.03027 Theoretical computer science, 6th GI-Conf., Dortmund 1983, Lect. Notes Comput. Sci. 145, 1-18 (1982). MSC: 03F50 03D70 68N01 PDFBibTeX XML