Ratings by cpressey of Coq works

Software Foundations

• rating: 3

.

Certified Programming with Dependent Types

• rating: TODO

.

Modeling and Proving in Computational Type Theory Using the Coq Proof Assistant (Draft)

• rating: TODO

.

Recursive Datatypes and Inductive Proofs

• rating: TODO

.

Interactive Theorem Proving with Coq

• rating: TODO

.

Pragmatic Quotient Types in Coq

• rating: 1

.

Interaction Trees

• rating: 2

.

Standard Library | The Coq Proof Assistant

• rating: 1

.

implication - Transitivity of -> in Coq - Stack Overflow

• rating: 1

.

proof - Proving (\~A -> \~B)-> (\~A -> B) -> A in Coq - Stack Overflow

• rating: 1

.

coq - Proving f (f bool) = bool - Stack Overflow

• rating: 1

.

DProp.Prop

• rating: 1

.

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

• rating: 1

.

coq - Defining Kripke models and the canonical model for $S4$ modal logic - Proof Assistants Stack Exchange

• rating: 1

.

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

• rating: 1

.

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

• rating: 1

.

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

• rating: 1

.

Ana de Almeida Borges / Coq formalization of QRC1 · GitLab

• rating: 0

.