Kaufmann, Matt; Moore, J Strother Limited second-order functionality in a first-order setting. (English) Zbl 1468.68291 J. Autom. Reasoning 64, No. 3, 391-422 (2020). MSC: 68V15 03B35 68N15 68N18 PDFBibTeX XMLCite \textit{M. Kaufmann} and \textit{J S. Moore}, J. Autom. Reasoning 64, No. 3, 391--422 (2020; Zbl 1468.68291) Full Text: DOI
Steinberg, Florian; Théry, Laurent; Thies, Holger Quantitative continuity and computable analysis in Coq. (English) Zbl 07649977 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 28, 21 p. (2019). MSC: 68V15 PDFBibTeX XMLCite \textit{F. Steinberg} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 28, 21 p. (2019; Zbl 07649977) Full Text: DOI
Paulin-Mohring, Christine; Werner, Benjamin Synthesis of ML programs in the system Coq. (English) Zbl 0804.68132 J. Symb. Comput. 15, No. 5-6, 607-640 (1993). MSC: 68T15 68Q60 68N15 PDFBibTeX XMLCite \textit{C. Paulin-Mohring} and \textit{B. Werner}, J. Symb. Comput. 15, No. 5--6, 607--640 (1993; Zbl 0804.68132) Full Text: DOI