Output details
11 - Computer Science and Informatics
University of Edinburgh
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
<11> Originality: Implementations of theorem proving systems typically involve many details not treated in the official theory of their underlying proofs. This paper presents a general framework for (interactive) proof search in a general class of type theories, logically equivalent to their standard typed lambda calculus presentation, bringing together many techniques previously developed for individual systems.
Significance: The calculus gives a uniform treatment of Huet's higher-order unification algorithm, Dowek's type inhabitant enumeration, and forms the basis for Spiwack's reimplementation of the Coq theorem-proving kernel.
Rigour: The paper contains detailed proofs, which have been fully formalised in Coq in Siles' PhD.
