A regression proof selection tool for the Coq proof assistant
-
Updated
Dec 1, 2017 - Shell
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
A regression proof selection tool for the Coq proof assistant
OCaml module of Nijn to generate coq scripts for checking termination proofs of higher-order rewriting systems.
A verification tool developed in Coq for analyzing cloud block storage
Calvin Talks Types
Configuring Proof General for use with Coq is hard and the defaults suck. This is a simple baseline configuration for Emacs.
Rounds and renders huge rational numbers to human-readable decimals.
Machine-checked proofs of secrecy and authentication using CCSA framework
Coq Implementation of the (vis, ar) Specification Framework for Replicated Data Types
A formal specification and verification of Tree Sort algorithm in Coq
COQ. Certified Programming with Dependent Types by Adam Chlipala. Exercises from the book. Solutions.
Software Foundations book and exercises taken from https://www.cis.upenn.edu/~bcpierce/sf/current/index.html
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 2 months ago