In our sixth episode, we speak with Professor Aaron Stump from the University of Iowa. We discuss Cedille, a proof assistant based on the Calculus of Dependent Lambda Eliminations, which allows impredicative lambda-encodings to be used for dependently typed programming, instead of a separate notion of inductive datatypes.
Reading:
Additional links:
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.
In our fourth episode, we speak with Stephanie Weirich from the University of Pennsylvania on the Zombie language and Dependent Haskell. Stephanie is a long-time contributor to Haskell, having been involved in the design and implementation of features such as generalized algebraic datatypes, higher-rank polymorphism, type families, and promoted datatypes. She has also been a participant in Trellys, a project with the goal of combining proofs and programming in the same language.
Zombie is a different kind of dependently typed language, eschewing automatic β-reduction in the type checker for an approach based on explicit equality rewriting, which enables new ways of combining proofs and programs, as well as new forms of proof automation. Meanwhile, as languages designed for dependently typed programming come closer to practical applicability, Haskell is also moving towards full dependent types. We discuss the challenges and opportunities available at the cutting edge of Haskell.
Reading:
Video:
Code:
In our third episode, we dicuss homotopy type theory (HoTT) with Wesleyan University’s Dan Licata. Dan has participated during much of the development of HoTT, having completed his PhD at CMU and having been a part of the Institute for Advanced Study’s special year on the subject. In our interview, we discuss the basics of HoTT, some potential applications in both mathematics and computing, as well as ongoing work on computation, univalence, and cubes.
Reading:
- The HoTT book is a collaborative effort from the IAS’s Univalent Foundations program. It presents the basics of HoTT, and then demonstrates how a number of different branches of mathematics can be developed within it.
- Homotopical Patch Theory by Carlo Angiuli, Edward Morehouse, Dan Licata, and Bob Harper is the expanded version of the ICFP paper mentioned in the podcast. This paper applies HoTT to a programmer-relevant topic: Darcs’s patch theory. It can serve as a good introduction to higher inductive types for those whose intuitions are based in code.
- Dan’s Oxford talk: A Cubical Infinite-Dimensional Type Theory. slides / video
- Dan’s publications and talks page has a number of papers and presentations on HoTT.
- Overview of Nuprl: Innovations in Computational Type Theory using Nuprl
In our second episode, we speak with Edwin Brady from the University of St. Andrews. Since 2008, Edwin has been working on Idris, a functional programming language with dependent types. This episode is very much about programming: we discuss the language Idris, its history, its implementation strategies, and plans for the future.
Reading:
Resources:
- The Idris homepage, with links to mailing lists, Git repository, tutorial, etc
- The idris-hackers organization on Github, with tools and libraries
In our inaugural episode, we speak with Peter Dybjer from Chalmers University of Technology. Peter has made significant contributions to type theory, including inductive families, induction-recursion, and categorical models of dependent types. He is generally interested in program correctness, programming language semantics, and the connection between mathematics and programming. Today, we will talk about the relationship between QuickCheck-style testing and proofs and verification in type theory.