grammars-and-semantic-actions

Tech stack & purpose

This project implements Dependent Lambek Calculus (Lambekᴰ), a domain-specific dependent type theory for verified parsing and formal grammar theory, as a shallow embedding in Cubical Agda. The codebase formalizes key results in automata theory and formal language theory, including a verification of Thompson's construction for converting regular expressions to nondeterministic finite automata and a verification of the powerset construction for NFA determinization. It provides intrinsically verified parsers written in Lambekᴰ for several grammars including the Dyck language of balanced parentheses, arithmetic expressions, and arbitrary regular expressions, along with broader constructions such as a grammar accepting the same language as any given Turing machine. The project is built entirely in Agda and depends on the Cubical and cubical-categorical-logic libraries.

Languages

Contributors

• Steven Schaefer296 commits
• 
  Max S. New101 commits · 179 followers
• Pedro Amorim28 commits
• 
  Max S. New6 commits · 179 followers
• Pedro Henrique Azevedo de Amorim2 commits
• Boarders2 commits
• nvarner1 commits
• symiont-callan-mcgill1 commits
• Cass Alexandru1 commits