TYPES 2007: Cividale des Friuli, Italy

Marino Miculan, Ivan Scagnetto, Furio Honsell (Eds.): Types for Proofs and Programs, International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised Selected Papers. Lecture Notes in Computer Science 4941 Springer 2008, ISBN 978-3-540-68084-0

Lisa Allali:
Algorithmic Equality in Heyting Arithmetic Modulo. 1-17
Robert Atkey:
CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types. 18-32
João Filipe Belo:
Dependently Sorted Logic. 33-50
Francesco Ciraulo, Giovanni Sambin:
Finiteness in a Minimalist Foundation. 51-68
Pierre Corbineau:
A Declarative Language for the Coq Proof Assistant. 69-84
José Espírito Santo, Silvia Ghilezan, J. Ivetic:
Characterising Strongly Normalising Intuitionistic Sequent Terms. 85-99
Antoine Genitrini, Jakub Kozik, Marek Zaionc:
Intuitionistic vs. Classical Tautologies, Quantitative Comparison. 100-109
Agnieszka Kozubek, Pawel Urzyczyn:
In the Search of a Naive Type Theory. 110-124
Ralph Matthes, Martin Strecker:
Verification of the Redecoration Algorithm for Triangular Matrices. 125-141
Rasmus Ejlers Møgelberg, Alex Simpson:
A Logic for Parametric Polymorphism with Effects. 142-156
Claudio Sacerdoti Coen, Enrico Tassi:
Working with Mathematical Structures in Type Theory. 157-172
Jan Schwinghammer:
On Normalization by Evaluation for Object Calculi. 173-187
Hongwei Xi:
Attributive Types for Proof Erasure. 188-202