System-F-Coq
Formal language system
An implementation of System F in Coq, aiming to provide a rigorous and expressive formal system for describing programming languages.
System F in coq.
19 stars
4 watching
0 forks
Language: Coq
last commit: over 11 years agoRelated projects:
| Repository | Description | Stars |
|---|---|---|
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 142 |
 xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
 coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 46 |
 lysxia/system-f | A formalization of polymorphic lambda calculus with a proof of parametricity theorem. | 33 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
 coq-io/system | A library of Unix effects implemented in the Coq functional programming language | 23 |
 bobatkey/system-f-parametricity-model | An implementation of System F type theory with parametricity models in Coq | 22 |
 starkware-libs/cairo-lang | A language and package for writing provable programs in Python. | 1,350 |
 coq-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 153 |
| xavierleroy/cdf-program-logics | Companion Coq development for teaching program logics | 40 |
 mit-pdos/fscq | A file system written and verified in the Coq proof assistant with a focus on security. | 237 |