NuprlInCoq
Type theory implementation
Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency.
Implementation of Nuprl's type theory in Coq
44 stars
8 watching
3 forks
Language: Coq
last commit: almost 4 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 154 |
 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 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 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,259 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 bobatkey/system-f-parametricity-model | An implementation of System F type theory with parametricity models in Coq | 22 |