Skip to main content
SpringerLink
Log in
Book cover

Types for Proofs and Programs

Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers

  • Conference proceedings
  • © 2003

Overview

Editors:
  1. Herman Geuvers

    1. Department of Computer Science, University of Nijmegen, Nijmegen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Freek Wiedijk

    1. Department of Computer Science, University of Nijmegen, Nijmegen, The Netherlands

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2646)

Included in the following conference series:

Conference proceedings info: TYPES 2002.

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (18 papers)

  1. Front Matter

    Pages I-VIII
    Download chapter PDF

  2. (Co-)Iteration for Higher-Order Nested Datatypes

    • Andreas Abel, Ralph Matthes
    Pages 1-20

  3. Program Extraction in Simply-Typed Higher Order Logic

    • Stefan Berghofer
    Pages 21-38

  4. General Recursion in Type Theory

    • Ana Bove
    Pages 39-58

  5. Using Theory Morphisms for Implementing Formal Methods Tools

    • Achim D. Brucker, Burkhart Wolff
    Pages 59-77

  6. Subsets, Quotients and Partial Functions in Martin-Löf’s Type Theory

    • Jesper Carlström
    Pages 78-94

  7. Mathematical Quotients and Quotient Types in Coq

    • Laurent Chicli, Loïc Pottier, Carlos Simpson
    Pages 95-107

  8. A Constructive Formalization of the Fundamental Theorem of Calculus

    • Luís Cruz-Filipe
    Pages 108-126

  9. Two Behavioural Lambda Models

    • Mariangiola Dezani-Ciancaglini, Silvia Ghilezan
    Pages 127-147

  10. A Unifying Approach to Recursive and Co-recursive Definitions

    • Pietro Di Gianantonio, Marino Miculan
    Pages 148-161

  11. Holes with Binding Power

    • Georgi I. Jojgov
    Pages 162-181

  12. Typing with Conditions and Guarantees for Functional In-place Update

    • Michal Konečný
    Pages 182-199

  13. A New Extraction for Coq

    • Pierre Letouzey
    Pages 200-219

  14. Weak Transitivity in Coercive Subtyping

    • Yong Luo, Zhaohui Luo, Sergei Soloviev
    Pages 220-239

  15. The Not So Simple Proof-Irrelevant Model of CC

    • Alexandre Miquel, Benjamin Werner
    Pages 240-258

  16. Structured Proofs in Isar/HOL

    • Tobias Nipkow
    Pages 259-278

  17. Java as a Functional Programming Language

    • Anton Setzer
    Pages 279-298

  18. Monad Translating Inductive and Coinductive Types

    • Tarmo Uustalu
    Pages 299-315

  19. A Finite First-Order Presentation of Set Theory

    • Stéphane Vaillant
    Pages 316-330

  20. Back Matter

    Pages 331-331
    Download chapter PDF
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

About this book

These proceedings contain a refereed selection of papers presented at the Second Annual Workshop of the Types Working Group (Computer-Assisted Reasoning based on Type Theory, EUIST project 29001), which was held April 24–28, 2002 in Hotel Erica, Berg en Dal (close to Nijmegen), The Netherlands. The workshop was attended by about 90 researchers. On April 27, there was a special afternoon celebrating the 60th birthday of Per Martin-L¨of, one of the founding fathers of the Types community. The afternoon consisted of the following three invited talks: “Constructive Validity Revisited” by Dana Scott, “From the Rules of Logic to the Logic of Rules” by Jean-Yves Girard, and “The Varieties of Type Theories” by Peter Aczel. The contents of these contributions were not laid down in these proceedings, but the videos of the talks and the slides used by the speakers are available at http://www. cs. kun. nl/fnds/MartinLoefDay/LoefTalks. htm The previous workshop of the Types Working Group under EUIST project 29001 was held in 2000 in Durham, UK. The workshops Types 2000 and Types 2002 followed a series of meetings organized in the period 1993 – 1999 whithin previous Types projects (ESPRIT BRA 6435 and ESPRIT Working Group 21900). The proceedings of these earlier Types workshops were also published in the LNCS series, as volumes 806, 996, 1158, 1512, 1657, 1956 and 2277. ESPRIT BRA 6453 was a continuation of ESPRIT Action 3245, Logical Frameworks: - sign, Implementation and Experiments.

Editors and Affiliations

  • Department of Computer Science, University of Nijmegen, Nijmegen, The Netherlands

    Herman Geuvers, Freek Wiedijk

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation