Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus (Extended Version)

Steven Schaefer, Nathan Varner, Pedro H. Azevedo de Amorim +1

We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In ${\text{Lambek}}^D$, linear types are used as a syn…