Preface Natarajan Shankar | ||
Canonical calculi with (n,k)-ary quantifiers | ||
Arnon Avron and Anna Zamansky | ||
Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics | ||
Robert L. Constable and Wojciech Moczydlowski | ||
Consistency and Completeness of Rewriting in the Calculus of Constructions | ||
Daria Walukiewicz-Chrząszcz and Jacek Chrząszcz | ||
On the strength of proof-irrelevant type theories | ||
Benjamin Werner | ||
Interpolation in local theory extensions | ||
Viorica Sofronie-Stokkermans | ||
Cut-Simulation and Impredicativity | ||
Christoph E. Benzmueller, Chad E. Brown and Michael Kohlhase | ||