system-F
Lambda calculus formalization
A formalization of polymorphic lambda calculus with a proof of parametricity theorem.
Formalization of the polymorphic lambda calculus and its parametricity theorem
33 stars
4 watching
2 forks
Language: Coq
last commit: almost 6 years ago coqdenotational-semanticsformalizationlambda-calculusparametricitypolymorphismsystem-f
Related projects:
| Repository | Description | Stars |
|---|---|---|
 pi8027/lambda-calculus | A formalization of typed and untyped lambda calculus in Coq and Agda2, aiming to provide a rigorous foundation for understanding the properties of these systems. | 78 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 142 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 bobatkey/system-f-parametricity-model | An implementation of System F type theory with parametricity models in Coq | 22 |
 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 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 thma/lambda-ski | Implementing a graph-reduction machine for a small functional language based on λ-calculus and combinatory logic | 28 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 94 |
 coq-community/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 45 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |
 blaisorblade/dot-iris | Mechanized formalization of soundness for DOT with logical relations in Coq | 30 |
 thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |
 ilya-klyuchnikov/lambdapi | Reorganization of source code for dependently typed lambda calculus paper to improve readability and understandability | 112 |