cdf-mech-sem
Formal semantics tools
Development of formal semantics and verification tools for imperative languages and functional programming languages.
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
64 stars
4 watching
4 forks
Language: Coq
last commit: 8 months ago
Linked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| xavierleroy/cdf-sem-meca | This project provides a development environment and software tools for formalizing the semantics of programming languages in the Coq proof assistant. | 21 |
| xavierleroy/cdf-program-logics | Companion Coq development for teaching program logics | 40 |
 coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 45 |
 discus-lang/iron | Formalizations of functional languages with a focus on proof and verification | 141 |
 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 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 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 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
| coq-community/topology | Develops and formalizes basic concepts and results of general topology in Coq. | 47 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 tezos/tezoscoq | A Coq-based library providing a formal verification framework for the Tezos smart contract language | 28 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 snu-sf/promising-coq | Development of a promising semantics for relaxed-memory concurrency | 33 |