cdf-program-logics
Program logic textbook
Companion Coq development for teaching program logics
Companion Coq development for Xavier Leroy's 2021 lectures on program logics
40 stars
2 watching
7 forks
Language: Coq
last commit: over 3 years ago
Linked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
| xavierleroy/cdf-mech-sem | Development of formal semantics and verification tools for imperative languages and functional programming languages. | 64 |
| 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 |
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 math-comp/tutorial_material | Tutorials and materials for teaching Coq-based mathematical component development | 17 |
 thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |
 charguer/tlc | A Coq library providing an alternative set of axioms and type class mechanisms for building and proving mathematical theorems. | 38 |
 princeton-vl/coqgym | A learning environment for theorem proving with the Coq proof assistant | 384 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 vlopezj/coq-course | A self-reading Coq course for PhD students covering fundamental topics in functional programming and formal verification. | 38 |
 coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/coqeal | A Coq library providing algebraic data structures and algorithms | 66 |
 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 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
| coq-community/semantics | A comprehensive survey of programming language semantics styles implemented in Coq | 45 |