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 
- Robin Adams, Zhaohui Luo:
Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory.
1-17
- Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli:
Crafting a Proof Assistant.
18-32
- Richard Bonichon, Olivier Hermant:
On Constructive Cut Admissibility in Deduction Modulo.
33-47
- Frédéric Besson:
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.
48-62
- Venanzio Capretta, Amy P. Felty:
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.
63-77
- Pierre Corbineau:
Deciding Equality in the Constructor Theory.
78-92
- Nils Anders Danielsson:
A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.
93-109
- Gilles Dowek:
Truth Values Algebras and Proof Normalization.
110-124
- Maribel Fernández, Murdoch Gabbay:
Curry-Style Types for Nominal Terms.
125-139
- Herman Geuvers:
(In)consistency of Extensions of Higher Order Logic and Type Theory.
140-159
- Florian Haftmann, Makarius Wenzel:
Constructive Type Classes in Isabelle.
160-174
- Danko Ilik:
Zermelo's Well-Ordering Theorem in Type Theory.
175-187
- Florent Kirchner:
A Finite First-Order Theory of Classes.
188-202
- Milad Niqui:
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers.
203-220
- 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
- Matthieu Sozeau:
Subset Coercions in Coq.
237-252
- Nathan Whitehead:
A Certified Distributed Security Logic for Authorizing Code.
253-268
Last update Tue Feb 14 04:12:02 2012
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
