Program Equivalence    (Equiv)

Hoare Logic, Part I    (Hoare)

Hoare Logic, Part II    (Hoare2)

Hoare Logic as a Logic    (HoareAsLogic)

Small-step Operational Semantics    (Smallstep)

Type Systems    (Types)

The Simply Typed Lambda-Calculus    (Stlc)

Properties of STLC    (StlcProp)

More on the Simply Typed Lambda-Calculus    (MoreStlc)

Subtyping    (Sub)

A Typechecker for STLC    (Typechecking)

Adding Records to STLC    (Records)

Typing Mutable References    (References)

Subtyping with Records    (RecordSub)

Normalization of STLC    (Norm)

Partial Evaluation    (PE)


Bibliography    (Bib)

A Collection of Handy General-Purpose Tactics    (LibTactics)

Tactic Library for Coq: A Gentle Introduction    (UseTactics)

Theory and Practice of Automation in Coq Proofs    (UseAuto)