Lang-n-Prove: A Domain-Specific Language for Language Proofs

Explore a 22-minute conference talk from ACM SIGPLAN on Lang-n-Prove, a domain-specific language designed for expressing theorems and proofs applicable to multiple languages within a certain class. Discover how Lang-n-Prove incorporates linguistic features specific to language design, enabling the expression of canonical forms lemmas, progress theorem, and type preservation theorem for a restricted class of functional languages. Learn about the application of Lang-n-Prove proofs to various functional languages, including those with polymorphism, exceptions, recursive types, list operations, and other common types and operators. Understand how the tool generates proof code in Abella, machine-checking the type safety of these languages when provided with correct substitution lemma code.

[SLE] Lang-n-Prove: A DSL for Language Proofs