TYPES 2003: Torino, Italy

@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
  
• 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 Fri May 25 08:43:38 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page