MPCTT
type theory development tool
A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory
Modeling and Proving in Computational Type Theory
82 stars
9 watching
10 forks
Language: Coq
last commit: 5 months ago
Linked from 1 awesome list
coq-community/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| uds-psl/autosubst2 | A tool for generating Coq code from syntactic theories with variable binders | 17 |
 hott/coq-hott | A Coq library for interpreting Martin-Löf's intensional type theory into abstract homotopy theory and relating it to higher category theory. | 1,262 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
| uds-psl/coq-library-undecidability | A collection of mechanized undecidability proofs in Coq | 111 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 155 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 jozefg/learn-tt | A collection of resources for learning type theory and related fields | 2,180 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 21 |
| uwplse/pumpkin-pi | Automatically discovers and proves relationships between types in Coq to simplify proof development and code reuse. | 49 |
 ilyasergey/pnp | A tutorial project on using Coq to mechanize mathematics with dependent types | 160 |
 eashanhatti/konna | An experimental language exploring two-level type theory to achieve compile-time evaluation of dynamic features | 11 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 220 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |