TYPES 2003:
Torino, Italy
Stefano Berardi, Mario Coppo, Ferruccio Damiani (Eds.):
Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers.
Lecture Notes in Computer Science 3085 Springer 2004, ISBN 3-540-22164-6 
- Robin Adams:
A Modular Hierarchy of Logical Frameworks.
1-16
- Fabio Alessi, Franco Barbanera, Mariangiola Dezani-Ciancaglini:
Tailoring Filter Models.
17-33
- Clemens Ballarin:
Locales and Locale Expressions in Isabelle/Isar.
34-50
- Sylvain Baro:
Introduction to PAF!, a Proof Assistant for ML Programs Verification.
51-65
- Stefan Berghofer:
A Constructive Proof of Higman's Lemma in Isabelle.
66-82
- Lorenzo Bettini, Viviana Bono, Silvia Likavec:
A Core Calculus of Higher-Order Mixins and Classes.
83-98
- Viviana Bono, Jerzy Tiuryn, Pawel Urzyczyn:
Type Inference for Nested Self Types.
99-114
- Edwin Brady, Conor McBride, James McKinna:
Inductive Families Need Not Store Their Indices.
115-129
- Jacek Chrzaszcz:
Modules in Coq Are and Will Be Correct.
130-146
- Horatiu Cirstea, Luigi Liquori, Benjamin Wack:
Rewriting Calculus with Fixpoints: Untyped and First-Order Systems.
147-161
- Pierre Corbineau:
First-Order Reasoning in the Calculus of Inductive Constructions.
162-177
- Ugo Dal Lago, Simone Martini, Luca Roversi:
Higher-Order Linear Ramified Recurrence.
178-193
- José Espírito Santo, Luis Pinto:
Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus.
194-209
- Nicola Gambino, Martin Hyland:
Wellfounded Trees and Dependent Polynomial Functors.
210-225
- Silvia Ghilezan, Pierre Lescanne:
Classical Proofs, Typed Processes, and Intersection Types: Extended Abstract.
226-241
- Furio Honsell, Marina Lenisa:
"Wave-Style" Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models.
242-258
- Robert Kießling, Zhaohui Luo:
Coercions in Hindley-Milner Systems.
259-275
- Yong Luo, Zhaohui Luo:
Combining Incoherent Coercions for Sigma-Types.
276-292
- Alberto Momigliano, Alwen Fernanto Tiu:
Induction and Co-induction in Sequent Calculus.
293-308
- Milad Niqui, Yves Bertot:
QArith: Coq Formalisation of Lazy Rational Arithmetic.
309-323
- Furio Honsell, Ivan Scagnetto:
Mobility Types in Coq.
324-337
- Sergei Soloviev, David Chemouil:
Some Algebraic Structures in Lambda-Calculus with Inductive Types.
338-354
- Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker:
A Concurrent Logical Framework: The Propositional Fragment.
355-377
- Freek Wiedijk:
Formal Proof Sketches.
378-393
- Hongwei Xi:
Applied Type System: Extended Abstract.
394-408
Last update Tue May 21 01:00:12 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
