Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus
summary
Presents LambekD, a dependent, ordered linear type theory that makes parsers sound by construction and, with a complement/disjointness proof, complete. Implements a shallow embedding in Agda and encodes regular and context-free grammars plus automaton traces; shipped examples include a balanced‑parentheses parser, an LL(1) arithmetic parser, and a verified regex→automaton parser generator. Gives a denotational semantics mapping types to string→parse‑tree sets and provides artifacts evaluated and reusable.
AI-written summary · about
chapters (14)
- 0:00Verified parsing in Lambek calculus
- 1:24Verified and correct parsers
- 3:10Dependent Lambek calculus foundation
- 4:11Structure and types in Lambek
- 6:40Parse trees with linear types
- 8:45Verified parser for parentheses
- 10:30Parser completeness with complement grammars
- 11:11Automata as linear types
- 13:16Recap and applications
- 15:19Future directions and extensions
- 16:23Q&A: Determinism and completeness
- 17:05Q&A: Denotational semantics choice
- 17:50Q&A: Proving ambiguity
- 18:33Q&A: Meta-theorems and closure
related talks
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
01h 03mVerifying Dependent Type-checkers
22mA Dependent Language with Type-Safe Program Extraction
45mLogic Meta Programming for Functional Languages
19mType Inference Logics
31mDependent tagless final
22mA Calculus of Inductive Linear Constructions
19mDeriving Dependently-Typed OOP from First Principles