Symbols

Preface

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

SfLib: Software Foundations Library

Imp: Simple Imperative Programs

ImpParser: Lexing and Parsing in Coq

Equiv: Program Equivalence

ImpList: Imp Extended with Lists

Hoare: Hoare Logic

HoareAsLogic: Hoare Logic as a Logic

Smallstep: Small-step Operational Semantics

Stlc: The Simply Typed Lambda-Calculus

Typechecking

MoreStlc: More on the Simply Typed Lambda-Calculus

Records: Adding Records to STLC

References: Typing Mutable References

Subtyping

Subtyping

RecordSub: Subtyping with Records

Norm: Normalization of STLC

UseTactics: Tactic Library for Coq: a gentle introduction

UseAuto: Theory and Practice of Automation in Coq Proofs

LibTactics: A Collection of Handy General-Purpose Tactics

PE: Partial Evaluation

Postscript


This page has been generated by coqdoc