Ratings by cpressey of Coq works

Software Foundations

• rating: 3

Logic in Coq (CS3110)

• rating: 1

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

Introduction and Contents — The Rocq Prover 9.0.0 documentation

• rating: 1

Transitivity of -> in Coq

• rating: 1

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

• rating: 1

Proving f (f bool) = bool

• rating: 1

Is eta-equality provable in Coq?

• rating: 1

Coq functional extensionality

• rating: 1

DProp.Prop

• rating: 1

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

• rating: 1

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

• 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