© 2009

Types for Proofs and Programs

International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers

  • Stefano Berardi
  • Ferruccio Damiani
  • Ugo de’Liguoro
Conference proceedings TYPES 2008

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

Table of contents

  1. Front Matter
  2. Davide Ancona, Giovanni Lagorio, Elena Zucca
    Pages 1-18
  3. Andrea Asperti, Wilmer Ricciotti
    Pages 19-31
  4. Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini
    Pages 32-48
  5. Juan Manuel Crespo, Gustavo Betarte, Carlos Luna
    Pages 49-63
  6. Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks, Jan Willem Klop, Roel de Vrijer
    Pages 64-82
  7. Erik Ernst
    Pages 83-99
  8. José Espírito Santo, Ralph Matthes, Luís Pinto
    Pages 100-116
  9. Camillo Fiorentini, Alberto Momigliano, Mario Ornaghi
    Pages 117-135
  10. Marco Gaboardi, Simona Ronchi Della Rocca
    Pages 136-152
  11. Florian Haftmann, Makarius Wenzel
    Pages 153-168
  12. Clément Houtmann
    Pages 169-185
  13. Cezary Kaliszyk, Freek Wiedijk
    Pages 203-219
  14. Yves Bertot, Ekaterina Komendantskaya
    Pages 220-236
  15. Eelis van der Weegen, James McKinna
    Pages 256-271
  16. Luca Paolini, Mauro Piccolo
    Pages 289-305

About these proceedings


This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2008, the last of a series of meetings of the TYPES working group funded by the European Union between 1993 and 2008; the workshop has been held in Torino, Italy, in March 2008.

The 19 revised full papers presented were carefully reviewed and selected from 27 submissions. The topic of the workshop was formal reasoning and computer programming based on type theory: languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, mobile code, formalization of mathematics, mathematics education.


Coq Quicksort Scheme Simulation abstract mathematics answer set programming complexity formal proofs formal semantics formal specification formal verification logic programming programming language proving recursion

Editors and affiliations

  • Stefano Berardi
    • 1
  • Ferruccio Damiani
    • 2
  • Ugo de’Liguoro
    • 1
  1. 1.Dipartimento di InformaticaUniversità di TorinoTorinoItaly
  2. 2.Dipartimento di InformaticaUniversità di TorinoTorinoItaly

Bibliographic information

Industry Sectors
IT & Software
Finance, Business & Banking
Energy, Utilities & Environment