theoremprover-museum / theoremprover-museum.github.io
☆51Updated last month
Related projects: ⓘ
- A (formalised) general definition of type theories☆56Updated 3 years ago
- General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]☆46Updated last month
- Documentation on goals of the coq-community organization, the shared contributing guide and code of conduct.☆68Updated 4 months ago
- Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]☆108Updated 2 weeks ago
- Interpreter for the reversible functional language rFun☆35Updated 6 years ago
- Notes and handouts from OPLSS 2019☆34Updated 5 years ago
- SML code for Handbook of Practical Logic and Automated Reasoning - For Isabelle too☆34Updated 7 years ago
- Algebraic Combinatorics in Coq☆34Updated 7 months ago
- The opentheory tool processes higher order logic theory packages☆15Updated last year
- A Scheme-like CBPV language with Racket Interoperability☆39Updated 6 months ago
- The Mechanization of Standard ML☆72Updated 2 years ago
- Alg is a program that generates all finite models of a first-order theory. It is optimized for equational theories.☆83Updated 3 years ago
- HoTT in Lean 3☆75Updated 4 years ago
- Hoare Type Theory☆68Updated 4 months ago
- A blog about Coq☆46Updated 2 years ago
- Coq library for working with de Bruijn indices [maintainer=@KevOrr]☆28Updated 3 years ago
- Generates natural language versions of Coq proofs☆51Updated 6 years ago
- Implementation of Nuprl's type theory in Coq☆44Updated 3 years ago
- A formalization of the Dedekind real numbers in Coq [maintainer=@andrejbauer]☆43Updated 2 months ago
- A proof of Abel-Ruffini theorem.☆28Updated last month
- Formalising Type Theory in a modular way for translations between type theories☆90Updated 6 years ago
- Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]☆50Updated this week
- Graph Theory [maintainers=@chdoc,@damien-pous]☆32Updated 2 months ago
- A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.☆32Updated 7 years ago
- An interactive theorem prover based on lambda-tree syntax☆89Updated 3 weeks ago
- ☆58Updated 5 years ago
- Standard ML compiler based on typed intermediate languages.☆46Updated 10 years ago
- An enhanced unification algorithm for Coq☆49Updated 3 months ago
- The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]☆65Updated last month
- An equational theorem prover based on Knuth-Bendix completion☆49Updated 3 months ago