Coq
---

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _See also: [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving), [Calculus of Constructions](../Calculus%20of%20Constructions/README.md#calculus-of-constructions)_

- - - -


### Web resources

[Standard Library | The Coq Proof Assistant](https://coq.inria.fr/doc/V8.19.0/stdlib/) ★

[implication - Transitivity of -\> in Coq - Stack Overflow](https://stackoverflow.com/questions/55295029/transitivity-of-in-coq) ★

[proof - Proving (\~A -\> \~B)-\> (\~A -\> B) -\> A in Coq - Stack Overflow](https://stackoverflow.com/questions/55232025/proving-a-b-a-b-a-in-coq) ★

[coq - Proving f (f bool) = bool - Stack Overflow](https://stackoverflow.com/questions/1674018/proving-f-f-bool-bool) ★

[DProp.Prop](https://dunnl.github.io/dprop/DProp.Prop.html) ★ [💭](commentary/Chris%20Pressey.md#dpropprop)

[Address a \"setoid hell\"? · Issue \#10871 · coq/coq](https://github.com/coq/coq/issues/10871) ★

[coq - Defining Kripke models and the canonical model for $S4$ modal logic - Proof Assistants Stack Exchange](https://proofassistants.stackexchange.com/questions/2312/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](https://github.com/JasonGross/coq-union-find) ★

[codyroux/tinymatch: A teeny language with nats, lists and pattern matching, static and dynamic semantics and a proof of progress and preservation.](https://github.com/codyroux/tinymatch) ★

[plclub/hs-to-coq: Convert Haskell source code to Coq source code.](https://github.com/plclub/hs-to-coq) ★

[Ana de Almeida Borges / Coq formalization of QRC1 · GitLab](https://gitlab.com/ana-borges/QRC1-Coq)

_(in [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving))_ [stepchowfun/proofs: My personal repository of formally verified mathematics.](https://github.com/stepchowfun/proofs) ★★


### Papers

Recursive Datatypes and Inductive Proofs (online @ [www.inf.ed.ac.uk](https://www.inf.ed.ac.uk/teaching/courses/ar/slides/lec14/Coq_Induction.pdf))

Interactive Theorem Proving with Coq (online @ [people.eecs.berkeley.edu](https://people.eecs.berkeley.edu/~necula/autded/lecture18-coq.pdf))

Pragmatic Quotient Types in Coq (online @ [perso.crans.org](https://perso.crans.org/cohen/papers/quotients.pdf)) ★ [💭](commentary/Chris%20Pressey.md#pragmatic-quotient-types-in-coq)

Interaction Trees (online @ [archive.org](https://archive.org/details/interaction-trees-representing-recursive-and-impure-programs-in-coq)) ★★ [💭](commentary/Chris%20Pressey.md#interaction-trees)

_(in [Calculus of Constructions](../Calculus%20of%20Constructions/README.md#calculus-of-constructions))_ [Introduction to the Calculus of Inductive Constructions](https://inria.hal.science/hal-01094195/document) ★ [💭](commentary/Chris%20Pressey.md#introduction-to-the-calculus-of-inductive-constructions)

_(in [Term Rewriting](../Term%20Rewriting/README.md#term-rewriting))_ [A Constructive Semantics for Rewriting Logic](https://digitalcommons.uri.edu/oa_diss/268/) ★★ [💭](commentary/Chris%20Pressey.md#a-constructive-semantics-for-rewriting-logic)

_(in [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving))_ Theorem proving support in programming language semantics (online @ [arxiv.org](https://arxiv.org/abs/0707.0926)) ★ [💭](commentary/Chris%20Pressey.md#theorem-proving-support-in-programming-language-semantics)


### Books

Software Foundations (online @ [softwarefoundations.cis.upenn.edu](https://softwarefoundations.cis.upenn.edu/)) ★★★ [💭](commentary/Chris%20Pressey.md#software-foundations)

Certified Programming with Dependent Types (online @ [archive.org](https://archive.org/details/CertifiedProgrammingWithDependentTypes)) [💭](commentary/Chris%20Pressey.md#certified-programming-with-dependent-types)

Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft) (online @ [www.ps.uni-saarland.de](https://www.ps.uni-saarland.de/~smolka/drafts/icl2021.pdf)) [💭](commentary/Chris%20Pressey.md#modeling-and-proving-in-computational-type-theory-using-the-coq-proof-assistant-draft)