Bruno Barras: Verification of the Interface of a Small Proof System in Coq. TYPES 1996: 28-45