A Dependent Language with Type-Safe Program Extraction
summary
Extractly is a first‑order language inspired by Polarity that removes large elimination and requires all data type definitions to be small, so extraction becomes simple type erasure only rather than inserting casts. The repo currently implements a type checker; erasure to a non‑dependent target and formal source definitions are missing. A conjectured translation from MLTT handles examples including a meta‑circular STLC evaluator and heterogeneous lists, but singleton pattern matches and small‑index restrictions introduce extra runtime patterning and unresolved generality.
AI-written summary · about
chapters (8)
- 0:00Dependent language extraction
- 2:31Extractly language
- 3:57Extractly features and limits
- 9:13Code data types in Extractly
- 13:53Challenges without large elimination
- 15:36Potential Extractly extensions
- 18:48Summary and future work
- 19:35Q&A
related talks
24mCode Extraction from Coq to ML-like languages
14mA dependently typed calculus with pattern matching and erasure inference
21mVerified Extraction from Coq to OCaml
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
19mDeriving Dependently-Typed OOP from First Principles
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2
31mDependent tagless final
19mIntrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus