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 days 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 | 110 |
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 |