In our fifth episode, we speak with Bob Constable from Cornell University. In addition to having been doctoral advisor to many of the leading researchers in programming languages, Bob leads the PRL research group in constructive type theory, which has produced the Nuprl proof assistant. In this interview, we discuss Nuprl and its underlying type theory, along with the intellectual context within which they have developed.
Reading:
- Naïve Computational Type Theory by Robert Constable, Marktoberdorf Summer School 2001
- Two Lectures on Computational Type Theory by Robert Constable, Oregon Programming Languages Summer School 2015
- The Nuprl book by the PRL Group
- Infinite Objects in Type Theory by Nax Mendler, Robert Constable, and Prakash Panangaden, LICS 1986
- A Non-Type-Theoretic Definition of Martin-Löf’s Types by Stuart Allen, LICS 1987
- Constructing Type Systems over an Operational Semantics by Robert Harper, JSC 1992
- Equality in Lazy Computation Systems by Douglas Howe, LICS 1989
- Partial Objects in Constructive Type Theory by Scott Smith and Robert Constable, LICS 1987
- Aspects of the Implementation of Type Theory by Robert Harper, PhD Thesis 1985
- Constructive Mathematics and Computer Programming by Per Martin-Löf, 1979
- Towards a Formally Verified Proof Assistant by Abhishek Anand and Vincent Rahli, ITP 2014
- Innovations in Computational Type Theory using Nuprl by Stuart Allen, Mark Bickford, Robert Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran, JAL 2006
- A Causal Logic of Events in Formalized Computational Type Theory by Mark Bickford and Robert Constable, Tech Report
- Virtual Evidence: A Constructive Semantics for Classical Logics by Robert Constable, 2014
- Intuitionistic Completeness of First-Order Logic by Robert Constable and Mark Bickford, 2011
- A Machine-Independent Theory of the Complexity of Recursive Functions by Manuel Blum, JACM 1967
- Induction-Recursion and Initial Algebras by Peter Dybjer and Anton Setzer, Annals of Pure and Applied Logic 2003
- JonPRL, a proof assistant for Computational Type Theory inspired by Nuprl
Additionally, the entire publication history of the PRL group is available from their Web site.
- Download:
- AAC27 MB
- MP329 MB
- FLAC112 MB
- Opus Audio34 MB