Logic Meta Programming for Functional Languages
summary
Shows a working meta-programming pipeline: encoding lambda terms with higher-order abstract syntax in Lambda Prolog (LP), implementing a real type-checker for ML fragment and a simply-typed lambda calculus that performs both inference and elaboration, and building proof-transfer tooling named track and truck that rewrites goals between encodings and produces justificatory proof terms (integrated with an SMT plugin). Demonstrations include running the LP-based checker, reconstructing inferred types, and successfully transferring proofs between number encodings.
AI-written summary · about
chapters (14)
- 0:00Logic meta programming intro
- 1:54Logic programming origins
- 3:41Prolog syntax & semantics
- 8:03Lambda calculus basics
- 10:37Simply typed Lambda
- 13:05Encoding Lambda in Lambda Prolog
- 15:59Type checker in Lambda Prolog
- 21:45Beyond simply typed Lambda
- 25:43Proof assistants overview
- 29:23Coq proof demo
- 33:19Proof transfer problem
- 36:47Track & Truck tools
- 38:12Track proof transfer demo
- 41:24Key takeaways
related talks
50mA Type-Theoretic Framework for Certified Meta-programming
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
24mCode Extraction from Coq to ML-like languages
36mDependently Typed Multi-Stage Programming, Revisited
19mType Inference Logics
23mBetter Defunctionalization through Lambda Set Specialization
53mSemantics-based program manipulation in the age of LLMs
15mType-safe generation of modules in applicative and generative styles