Handbook of Automated Reasoning

Chapter 18

Proof-Assistants Using Dependent Type Systems

Henk Barendregt; Herman Geuvers

Contents

1.  Proof checking    1151

2.  Type-theoretic notions for proof checking    1153

2.1.  Proof checking mathematical statements    1153

2.2.  Propositions as types    1156

2.3.  Examples of proofs as terms    1157

2.4.  Intermezzo: Logical frameworks    1160

2.5.  Functions: algorithms versus graphs    1164

2.6.  Subject Reduction    1166

2.7.  Conversion and Computation    1166

2.8.  Equality    1168

2.9.  Connection between logic and type theory    1175

3.  Type systems for proof checking    1180

3.1.  Higher order predicate logic    1181

3.2.  Higher order typed λ-calculus    1185

3.3.  Pure Type Systems    1196

3.4.