Creative Commons
| 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 | ||