Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers

Robin Adams, Zhaohui Luo (auth.), Thorsten Altenkirch, Conor McBride (eds.)3540744630, 9783540744634

The International Workshop of the Types Working Group was held in Nottingham, UK, in April 2006. This workshop attracted leading minds in computing and computer programming who came to share their findings and discuss the latest developments and applications in the field. The workshop took place as part of the Seventh Symposium on Trends in Functional Programming. This book constitutes the refereed post-proceedings of the workshop.

Inside this volume are 17 full papers. Each one of them was carefully reviewed and selected from among 29 submissions.

The papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education.

---

Table of contents :
Front Matter….Pages –
Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory….Pages 1-17
Crafting a Proof Assistant….Pages 18-32
On Constructive Cut Admissibility in Deduction Modulo….Pages 33-47
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond….Pages 48-62
Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq….Pages 63-77
Deciding Equality in the Constructor Theory….Pages 78-92
A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family….Pages 93-109
Truth Values Algebras and Proof Normalization….Pages 110-124
Curry-Style Types for Nominal Terms….Pages 125-139
(In)consistency of Extensions of Higher Order Logic and Type Theory….Pages 140-159
Constructive Type Classes in Isabelle….Pages 160-174
Zermelo’s Well-Ordering Theorem in Type Theory….Pages 175-187
A Finite First-Order Theory of Classes….Pages 188-202
Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers….Pages 203-220
Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs….Pages 221-236
Subset Coercions in Coq ….Pages 237-252
A Certified Distributed Security Logic for Authorizing Code….Pages 253-268
Back Matter….Pages –