Cedille-Core

Tech stack & purpose

Cedille-Core is a minimal proof language consisting of roughly 1,000 lines of code that enables theorem proving about its own terms, addressing a gap in programming language design. While larger languages like Idris, Agda, and Coq support practical theorem proving, and smaller calculi like the Calculus of Constructions exist, Cedille-Core aims to be both small and practical for proving useful properties about programs. Developed by Aaron Stump, the language includes constructs for lambda abstraction, function types, dependent intersections, equality propositions, and rewriting, allowing users to express and verify mathematical theorems within a compact implementation.

Community & reference links

• Agda
• Brainfuck
• Calculus of Constructions
• Lambda Calculus

Languages

Contributors

• Victor Maia25 commits
• MaiaVictor3 commits
• Aaron Stump1 commits