An axiom-free formalization of category theory in Coq for personal study and practical work

Formal Reasoning About Programs

Mathematical Components

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

PeaCoq is a pretty Coq, isn't it?

Mindless, verified (erasably) coding using dependent types

The Penn Locally Nameless Metatheory Library

A blog about Coq

Old Coq plugin for parametricity [maintainer=@ppedrot]

Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic

Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016

Algebraic Combinatorics in Coq

Robots powered by Constructive Reals

A verified polyhedral scheduling validator in Coq.

A Model of Relationally Parametric System F in Coq

Formal proof in Coq of Banach-Tarski paradox.

Coq code accompanying several articles on semantics of functional programming languages

Initial tinkering with a BPF metalanguage and implementation formally verified in Coq.

A library for Gradual Certified Programming in Coq

Coq development for VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs, MFPS 2015

Automatic transfer of theorems along isomorphisms in Coq

Code from a talk given at YOW! Lambda Jam 2015