SPECIAL ISSUE:
Special Issue: Types for Proofs and Programs, 2010
Warsaw, Poland, 2010



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



DOI: 10.2168/LMCS-TYPES:2010

Creative Commons