cps
Continuation calculus
Formalization of a calculus for structured continuations in Coq
A formalization of continuation-passing style calculi in Coq [WIP]
36 stars
1 watching
0 forks
Language: Coq
last commit: 3 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 dschepler/coq-sequent-calculus | Formalizations of logical deduction systems using Coq | 44 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 anton-trunov/coq-lecture-notes | Lecture notes and resources for learning the Coq proof assistant | 50 |
 coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 fblanqui/color | A comprehensive Coq library providing formal definitions and proofs of rewriting theory, lambda-calculus, and termination. | 35 |
 yosuke-ito-345/actuary | Formalizes basic actuarial mathematics using Coq | 21 |
| coq-community/coq-art | Coq proof assistant book with exercises and examples | 114 |
 dboulytchev/minikanren-coq | A certified semantics for relational programming language specification, providing verified implementations of syntax and semantics for miniKanren languages | 26 |
| coq-community/sudoku | A formalisation of Sudoku in Coq to solve the puzzle using a naive Davis-Putnam procedure | 20 |
 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-concurrency/pluto | A Coq-based web server written in a functional programming language | 86 |
| coq-community/aac-tactics | Tactics for rewriting and proving equations with associativity and commutativity properties | 29 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/dedekind-reals | A formalization of Dedekind reals numbers in the Coq programming language | 43 |