Developing a Dependently Typed Language with Runtime Proof Search
summary
Prototype implements a call-by-value dependently typed language that delays constraint solving by adding an admit syntax and a three-stage pipeline: light type checking, an exploration phase that enumerates consistent instantiations of higher-order inputs to discover needed proofs, and a runtime that uses discovered terms. Claim: exploration is complete (will find an execution that triggers an admit) but not sound in all cases; guarantee: for ground types termination implies the returned values satisfy their proofs. Implementation is in progress, can non-deterministically choose poor witnesses and can break parametric reasoning.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 0:11Motivation
- 3:13Design
- 4:32Type checking
- 5:44Evaluation
- 6:47Exploration
- 10:14Exploration Strategy
- 12:02Quirks
- 16:36Audience Questions
related talks
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
19mA Dependently Typed Language with Dynamic Equality
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
18mDeferring the Details and Deriving Programs
32mDon’t Call Us, We’ll Call You
19mIll-Typed Programs Don't Evaluate
30mConstrained generation of well-typed programs
19mDeriving Dependently-Typed OOP from First Principles