README.md

Coq

(Up) | Wikipedia: Rocq | See also: Theorem Proving, Calculus of Constructions

Web resources

Introduction and Contents — The Rocq Prover 9.0.0 documentation ★

Logic in Coq (CS3110) ★

Transitivity of -> in Coq ★

Proving (\~A -> \~B)-> (\~A -> B) -> A in Coq ★

Proving f (f bool) = bool ★

Is eta-equality provable in Coq? ★

Coq functional extensionality ★

DProp.Prop ★ 💭

Address a \"setoid hell\"? · Issue #10871 · coq/coq ★

Defining Kripke models and the canonical model for $S4$ modal logic ★

Repositories

JasonGross/coq-union-find: A repository for playing with union-find in Coq ★

codyroux/tinymatch: A teeny language with nats, lists and pattern matching, static and dynamic semantics and a proof of progress and preservation. ★

plclub/hs-to-coq: Convert Haskell source code to Coq source code. ★

Ana de Almeida Borges / Coq formalization of QRC1 · GitLab

(in Theorem Proving) stepchowfun/proofs: My personal repository of formally verified mathematics. ★★

Papers

Recursive Datatypes and Inductive Proofs (online @ www.inf.ed.ac.uk)

Interactive Theorem Proving with Coq (online @ people.eecs.berkeley.edu)

Pragmatic Quotient Types in Coq (online @ perso.crans.org) ★ 💭

Interaction Trees (online @ archive.org) ★★ 💭

(in Calculus of Constructions) Introduction to the Calculus of Inductive Constructions ★ 💭

(in Term Rewriting) A Constructive Semantics for Rewriting Logic ★★ 💭

(in Theorem Proving) Theorem proving support in programming language semantics (online @ arxiv.org) ★ 💭

Books

Software Foundations (online @ softwarefoundations.cis.upenn.edu) ★★★ 💭

Certified Programming with Dependent Types (online @ archive.org) 💭

Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) (online @ www.ps.uni-saarland.de) 💭