system-f-parametricity-model
Type theory library
An implementation of System F type theory with parametricity models in Coq
A Model of Relationally Parametric System F in Coq
22 stars
4 watching
3 forks
Language: Coq
last commit: over 9 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |
 heades/system-f-coq | An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages. | 19 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 82 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
| coq-community/fav-ssr | A comprehensive library of verified data structures and algorithms in Coq | 45 |
 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 |
 vafeiadis/hahn | A collection of lemmas and tactics about lists and binary relations for a proof assistant | 30 |
 mit-plv/fiat | A Coq-based library for synthesizing correct-by-construction abstract data types and parsers from formal specifications | 149 |
 jtassarotti/coq-proba | A Coq-based probability theory library providing results and definitions for discrete probability, measure theory, and probabilistic choice monads. | 50 |
 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 |
 jwiegley/category-theory | An axiomatic formalization of category theory in Coq for personal study and practical work | 759 |