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