© 2008

Types for Proofs and Programs

International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007 Revised Selected Papers

  • Editors
  • Marino Miculan
  • Ivan Scagnetto
  • Furio Honsell
Conference proceedings TYPES 2007

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

Table of contents

  1. Front Matter
  2. João Filipe Belo
    Pages 33-50
  3. Francesco Ciraulo, Giovanni Sambin
    Pages 51-68
  4. J. Espírito Santo, S. Ghilezan, J. Ivetić
    Pages 85-99
  5. Antoine Genitrini, Jakub Kozik, Marek Zaionc
    Pages 100-109
  6. Agnieszka Kozubek, Paweł Urzyczyn
    Pages 110-124
  7. Ralph Matthes, Martin Strecker
    Pages 125-141
  8. Rasmus Ejlers Møgelberg, Alex Simpson
    Pages 142-156
  9. Claudio Sacerdoti Coen, Enrico Tassi
    Pages 157-172
  10. Hongwei Xi
    Pages 188-202
  11. Back Matter

About these proceedings


This book constitutes the thoroughly refereed post-conference proceedings of TYPES 2007, the concluding conference of the Types project, held in Cividale del Friuli, Italy, in May 2007.

The 13 revised full papers presented were carefully reviewed and selected from 22 submissions. The topic of this last annual workshop of the Types Working Group was formal reasoning and computer programming based on type theory. Great importance was attached to languages and computerized tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalization of mathematics and mathematics education.


algorithm algorithms finite sets formal methods formal reasoning formal specification formal verification higher-order logic logic polymorphism program semantics programming programming language programming the verification

Bibliographic information

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