Types for Proofs and Programs

Coercion synthesis in computer implementations of type-theoretic frameworks.- Verification of the interface of a small proof system in coq.- An implementation of the Heine-Borel covering theorem in type theory.- Detecting and removing dead-code using rank 2 intersection.- A type-free formalization of mathematics where proofs are objects.- Higman's lemma in type theory.- A proof of weak termination of typed ??-calculi.- Proof style.- Some algorithmic and proof-theoretical aspects of coercive subtyping.- Semantical BNF.- The internal type theory of a Heyting pretopos.- Inverting inductively defined relations in LEGO.- A generic normalisation proof for pure type systems.- Proving a real time algorithm for ATM in Coq.- Dependent types with explicit substitutions: A meta-theoretical development.- Type inference verified: Algorithm W in Isabelle/HOL.- Continuous lattices in formal topology.- Abstract insertion sort in an extension of type theory with record types and subtyping.