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 BibTeX

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