Basics: Functional programming and reasoning about programs

Lists: Products, Lists and Options

Poly: Polymorphism and Higher-Order Functions

Ind: Propositions and Evidence

Logic: Logic in Coq

Rel: Properties of Relations

Template: Patterns for Inductive Proofs

SfLib: Software Foundations Library

Imp: Simple Imperative Programs

ImpParser: Lexing and Parsing in Coq

Equiv: Program Equivalence

Hoare: Hoare Logic

MoreHoare: Hoare Logic with Lists; Formalizing Decorated Programs

Smallstep: Small-step Operational Semantics

Stlc: The Simply Typed Lambda-Calculus

MoreStlc: More on the Simply Typed Lambda-Calculus

References: Typing Mutable References

Subtyping: Subtyping


This page has been generated by coqdoc