10
Safety Proof Languages
§
Higher-order logic
§
Temporal Logic
§
Modal Logic
§
Linear Logic
§
Coq Logic
§
Type Systems
Dimension 1: Design
Shipment of proofs
Means formalization of proofs
Uniformity is important, since logic might change.
We do not want to invent a new proof checker for each logic we are trying, we are more interested in one
Trustworthy proof checker.
We have one, the type checker for LF, expressive enough