Types for Proofs and Programs

International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers

  • Stefano Berardi
  • Mario Coppo
  • Ferruccio Damiani
Conference proceedings TYPES 2003

Part of the Lecture Notes in Computer Science book series (LNCS, volume 3085)

Table of contents

  1. Front Matter
  2. Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini
    Pages 17-33
  3. Lorenzo Bettini, Viviana Bono, Silvia Likavec
    Pages 83-98
  4. Viviana Bono, Jerzy Tiuryn, Paweł Urzyczyn
    Pages 99-114
  5. Edwin Brady, Conor McBride, James McKinna
    Pages 115-129
  6. Jacek Chrza̧szcz
    Pages 130-146
  7. Horatiu Cirstea, Luigi Liquori, Benjamin Wack
    Pages 147-161
  8. Ugo Dal Lago, Simone Martini, Luca Roversi
    Pages 178-193
  9. José Espírito Santo, Luís Pinto
    Pages 194-209
  10. Nicola Gambino, Martin Hyland
    Pages 210-225
  11. Silvia Ghilezan, Pierre Lescanne
    Pages 226-241
  12. Robert Kießling, Zhaohui Luo
    Pages 259-275
  13. Yong Luo, Zhaohui Luo
    Pages 276-292
  14. Alberto Momigliano, Alwen Tiu
    Pages 293-308
  15. Milad Niqui, Yves Bertot
    Pages 309-323
  16. Furio Honsell, Ivan Scagnetto
    Pages 324-337
  17. Sergej Soloviev, David Chemouil
    Pages 338-354
  18. Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker
    Pages 355-377
  19. Freek Wiedijk
    Pages 378-393
  20. Hongwei Xi
    Pages 394-408
  21. Back Matter

About these proceedings


These proceedings contain a selection of refereed papers presented at or related to the 3rd Annual Workshop of the Types Working Group (Computer-Assisted Reasoning Based on Type Theory, EU IST project 29001), which was held d- ing April 30 to May 4, 2003, in Villa Gualino, Turin, Italy. The workshop was attended by about 100 researchers. Out of 37 submitted papers, 25 were selected after a refereeing process. The ?nal choices were made by the editors. Two previous workshops of the Types Working Group under EU IST project 29001 were held in 2000 in Durham, UK, and in 2002 in Berg en Dal (close to Nijmegen), The Netherlands. These workshops followed a series of meetings organized in the period 1993–2002 within previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these e- lier workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 2277, and 2646. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: Design, Implementation and Ex- riments. Proceedings for annual meetings under that action were published by Cambridge University Press in the books “Logical Frameworks”, and “Logical Environments”, edited by G. Huet and G. Plotkin. We are very grateful to the members of the research group “Semantics and Logics of Computation” of the Computer Science Department of the University of Turin, who helped organize the Types 2003 meeting in Torino.


Applied Type System Coq Isabelle ML Self formal methods formal proof inductive types lambda calculus proof theory rewriting systems subtyping type systems types verification

Editors and affiliations

  • Stefano Berardi
    • 1
  • Mario Coppo
    • 2
  • Ferruccio Damiani
    • 3
  1. 1.Dipartimento di InformaticaUniversità di TorinoTorinoItaly
  2. 2.Dipartimento di InformaticaUniversità di Torino 
  3. 3.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 2004
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-22164-7
  • Online ISBN 978-3-540-24849-1
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Finance, Business & Banking
IT & Software
Consumer Packaged Goods
Oil, Gas & Geosciences