cps

Continuation calculus

Formalization of a calculus for structured continuations in Coq

A formalization of continuation-passing style calculi in Coq [WIP]

GitHub

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