TYPES 2002: Berg en Dal, The Netherlands

@proceedings{DBLP:conf/types/2002,
  editor    = {Herman Geuvers and
               Freek Wiedijk},
  title     = {Types for Proofs and Programs, Second International Workshop,
               TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002,
               Selected Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2646},
  year      = {2003},
  isbn      = {3-540-14031-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

• Andreas Abel, Ralph Matthes:
  (Co-)Iteration for Higher-Order Nested Datatypes. 1-20
  Electronic Edition (Springer LINK) BibTeX
• Stefan Berghofer:
  Program Extraction in Simply-Typed Higher Order Logic. 21-38
  Electronic Edition (Springer LINK) BibTeX
• Ana Bove:
  General Recursion in Type Theory. 39-58
  Electronic Edition (Springer LINK) BibTeX
• Achim D. Brucker, Burkhart Wolff:
  Using Theory Morphisms for Implementing Formal Methods Tools. 59-77
  Electronic Edition (Springer LINK) BibTeX
• Jesper Carlström:
  Subsets, Quotients and Partial Functions in Martin-Löf's Type Theory. 78-94
  Electronic Edition (Springer LINK) BibTeX
• Laurent Chicli, Loic Pottier, Carlos Simpson:
  Mathematical Quotients and Quotient Types in Coq. 95-107
  Electronic Edition (Springer LINK) BibTeX
• Luís Cruz-Filipe:
  A Constructive Formalization of the Fundamental Theorem of Calculus. 108-126
  Electronic Edition (Springer LINK) BibTeX
• Mariangiola Dezani-Ciancaglini, Silvia Ghilezan:
  Two Behavioural Lambda Models. 127-147
  Electronic Edition (Springer LINK) BibTeX
• Pietro Di Gianantonio, Marino Miculan:
  A Unifying Approach to Recursive and Co-recursive Definitions. 148-161
  Electronic Edition (Springer LINK) BibTeX
• Gueorgui I. Jojgov:
  Holes with Binding Power. 162-181
  Electronic Edition (Springer LINK) BibTeX
• Michal Konecný:
  Typing with Conditions and Guarantees for Functional In-place Update. 182-199
  Electronic Edition (Springer LINK) BibTeX
• Pierre Letouzey:
  A New Extraction for Coq. 200-219
  Electronic Edition (Springer LINK) BibTeX
• Yong Luo, Zhaohui Luo, Sergei Soloviev:
  Weak Transitivity in Coercive Subtyping. 220-239
  Electronic Edition (Springer LINK) BibTeX
• Alexandre Miquel, Benjamin Werner:
  The Not So Simple Proof-Irrelevant Model of CC. 240-258
  Electronic Edition (Springer LINK) BibTeX
• Tobias Nipkow:
  Structured Proofs in Isar/HOL. 259-278
  Electronic Edition (Springer LINK) BibTeX
• Anton Setzer:
  Java as a Functional Programming Language. 279-298
  Electronic Edition (Springer LINK) BibTeX
• Tarmo Uustalu:
  Monad Translating Inductive and Coinductive Types. 299-315
  Electronic Edition (Springer LINK) BibTeX
• Stéphane Vaillant:
  A Finite First-Order Presentation of Set Theory. 316-330
  Electronic Edition (Springer LINK) BibTeX