iron
Functional language formalization
Formalizations of functional languages with a focus on proof and verification
Coq formalizations of functional languages.
142 stars
20 watching
9 forks
Language: Coq
last commit: about 6 years agocoqcoq-formalizationslambda-calculusprooftheory
Related projects:
| Repository | Description | Stars |
|---|---|---|
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 llee454/functional-algebra | A Coq formalization of abstract algebra using functional programming style | 28 |
 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 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 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 |
 coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 292 |
 thery/flocqlecture | An introductory course on floating-point numbers and formal proof using Coq | 6 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 reynir/brainfuck | Formalizing Brainfuck in Coq to prove its properties and verify a compiler for simple arithmetic expressions. | 26 |
| coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
 thma/lambda-ski | Implementing a graph-reduction machine for a small functional language based on λ-calculus and combinatory logic | 28 |
 zatonovo/lambda.r | A programming language and syntax for functional programs in R with type checking and pattern matching | 216 |