Certified LambdaJS semantics and interpreter.
-
Updated
Jan 30, 2017 - Coq
Certified LambdaJS semantics and interpreter.
Coq implementations and proof scripts developed for a course in mechanical reasoning.
Formalized Mathematics
Deadlock avoidance on using futures in shared memory. The project includes the formalization of a trace language and results on a policy on safe joins (through a notion of known tasks) and we show that data-race-freedom implies deadlock freedom.
A proof that Coq contains any total mu-recursive function
Coq formalization of the Habanero programming model.
The Tortoise and the Hare in Coq. Constructive extraction via Bar inductive predicates (see README.md below).
LVC verified compiler
A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.
A vector library specialized in the formalization of SPMD programs
This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
Certifying Answers of Boolean SAT-Solvers (with a proof combining Coq and OCaml typecheckers)
A study of a simplified Call-By-Push-Value lambda-calculus in Coq.
Fortune's algorithm described in coq
Formal semantics for Solidity in Coq
Add a description, image, and links to the coq-formalization topic page so that developers can more easily learn about it.
To associate your repository with the coq-formalization topic, visit your repo's landing page and select "manage topics."