Constable, Robert; Bickford, Mark Intuitionistic completeness of first-order logic. (English) Zbl 1345.03114 Ann. Pure Appl. Logic 165, No. 1, 164-198 (2014). MSC: 03F55 03B20 68T15 PDFBibTeX XMLCite \textit{R. Constable} and \textit{M. Bickford}, Ann. Pure Appl. Logic 165, No. 1, 164--198 (2014; Zbl 1345.03114) Full Text: DOI arXiv
Constable, Robert L. Building mathematics-based software systems to advance science and create knowledge. (English) Zbl 1258.68170 Albers, Susanne (ed.) et al., Efficient algorithms. Essays dedicated to Kurt Mehlhorn on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-03455-8/pbk). Lecture Notes in Computer Science 5760, 3-17 (2009). MSC: 68U05 03F65 68T15 PDFBibTeX XMLCite \textit{R. L. Constable}, Lect. Notes Comput. Sci. 5760, 3--17 (2009; Zbl 1258.68170) Full Text: DOI
Allen, S. F.; Bickford, M.; Constable, R. L.; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. Innovations in computational type theory using Nuprl. (English) Zbl 1107.68090 J. Appl. Log. 4, No. 4, 428-469 (2006). MSC: 68T15 03B35 PDFBibTeX XMLCite \textit{S. F. Allen} et al., J. Appl. Log. 4, No. 4, 428--469 (2006; Zbl 1107.68090) Full Text: DOI
Constable, Robert L. Recent results in type theory and their relationship to Automath. (English) Zbl 1063.68090 Kamareddine, Fairouz D. (ed.), Thirty-five years of automating mathematics. Dedicated to 35 years of de Bruijn’s Automath. Dordrecht: Kluwer Academic Publishers (ISBN 1-4020-1656-5/hbk). Applied Logic Series 28, 37-48 (2003). MSC: 68T15 68N15 PDFBibTeX XMLCite \textit{R. L. Constable}, Appl. Log. Ser. 28, 37--48 (2003; Zbl 1063.68090)
Constable, Robert L. A note on complexity measures for inductive classes in constructive type theory. (English) Zbl 0916.03039 Inf. Comput. 143, No. 2, 137-153 (1998). Reviewer: M.Hofmann MSC: 03F35 03D15 68Q15 03D20 PDFBibTeX XMLCite \textit{R. L. Constable}, Inf. Comput. 143, No. 2, 137--153 (1998; Zbl 0916.03039) Full Text: DOI
Constable, Robert L. Expressing computational complexity in constructive type theory. (English) Zbl 07776718 Leivant, Daniel (ed.), Logic and computational complexity. International workshop, LCC ’94, Indianapolis, IN, USA, October 13–16, 1994. Selected Papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 960, 131-144 (1995). MSC: 03-XX PDFBibTeX XMLCite \textit{R. L. Constable}, Lect. Notes Comput. Sci. 960, 131--144 (1995; Zbl 07776718) Full Text: DOI
Constable, R. L.; Knoblock, T. B.; Bates, J. L. Writing programs that construct proofs. (English) Zbl 0615.68063 J. Autom. Reasoning 1, 285-326 (1985). MSC: 68T15 PDFBibTeX XMLCite \textit{R. L. Constable} et al., J. Autom. Reasoning 1, 285--326 (1985; Zbl 0615.68063) Full Text: DOI
Constable, Robert L. Programs as proofs: A synopsis. (English) Zbl 0514.68043 Inf. Process. Lett. 16, 105-112 (1983). MSC: 68Q65 68W99 PDFBibTeX XMLCite \textit{R. L. Constable}, Inf. Process. Lett. 16, 105--112 (1983; Zbl 0514.68043) Full Text: DOI