Preface Henk Barendregt and Pawel Urzyczyn | ||
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination | ||
Assia Mahboubi and Cyril Cohen | ||
On completeness of reducibility candidates as a semantics of strong normalization | ||
Denis Cousineau | ||
A dependent nominal type theory | ||
James Cheney | ||
A System F accounting for scalars | ||
Pablo Arrighi and Alejandro Díaz-Caro | ||
Deciding Kleene Algebras in Coq | ||
Thomas Braibant and Damien Pous | ||
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions | ||
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen and Enrico Tassi | ||
On Irrelevance and Algorithmic Equality in Predicative Type Theory | ||
Andreas Abel and Gabriel Scherer | ||
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving | ||
Freek Wiedijk | ||
On streams that are finitely red | ||
Marc Bezem, Keiko Nakata and Tarmo Uustalu | ||