TYPES 2006: Nottingham, UK

Thorsten Altenkirch, Conor McBride (Eds.): Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers. Lecture Notes in Computer Science 4502 Springer 2007, ISBN 978-3-540-74463-4 BibTeX

Robin Adams, Zhaohui Luo:
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory. 1-17
Electronic Edition (link) BibTeX
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli:
Crafting a Proof Assistant. 18-32
Electronic Edition (link) BibTeX
Richard Bonichon, Olivier Hermant:
On Constructive Cut Admissibility in Deduction Modulo. 33-47
Electronic Edition (link) BibTeX
Frédéric Besson:
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. 48-62
Electronic Edition (link) BibTeX
Venanzio Capretta, Amy P. Felty:
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq. 63-77
Electronic Edition (link) BibTeX
Pierre Corbineau:
Deciding Equality in the Constructor Theory. 78-92
Electronic Edition (link) BibTeX
Nils Anders Danielsson:
A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. 93-109
Electronic Edition (link) BibTeX
Gilles Dowek:
Truth Values Algebras and Proof Normalization. 110-124
Electronic Edition (link) BibTeX
Maribel Fernández, Murdoch Gabbay:
Curry-Style Types for Nominal Terms. 125-139
Electronic Edition (link) BibTeX
Herman Geuvers:
(In)consistency of Extensions of Higher Order Logic and Type Theory. 140-159
Electronic Edition (link) BibTeX
Florian Haftmann, Makarius Wenzel:
Constructive Type Classes in Isabelle. 160-174
Electronic Edition (link) BibTeX
Danko Ilik:
Zermelo's Well-Ordering Theorem in Type Theory. 175-187
Electronic Edition (link) BibTeX
Florent Kirchner:
A Finite First-Order Theory of Classes. 188-202
Electronic Edition (link) BibTeX
Milad Niqui:
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers. 203-220
Electronic Edition (link) BibTeX
Hugo R. Simões, Kevin Hammond, Mário Florido, Pedro B. Vasconcelos:
Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs. 221-236
Electronic Edition (link) BibTeX
Matthieu Sozeau:
Subset Coercions in Coq. 237-252
Electronic Edition (link) BibTeX
Nathan Whitehead:
A Certified Distributed Security Logic for Authorizing Code. 253-268
Electronic Edition (link) BibTeX