Skip to main content
SpringerLink
Log in

Types for Proofs and Programs

International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers

  • Conference proceedings
  • © 1996

Overview

Editors:
  1. Stefano Berardi
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Mario Coppo
    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 1158)

Included in the following conference series:

Conference proceedings info: TYPES 1995.

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

Access this book

Log in via an institution
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 (19 papers)

  1. Front Matter

    Download chapter PDF

  2. Implicit coercions in type systems

    • Gilles Barthe
    Pages 1-15

  3. A two-level approach towards lean proof-checking

    • Gilles Barthe, Mark Ruys, Henk Barendregt
    Pages 16-35

  4. The greatest common divisor: A case study for program extraction from classical proofs

    • U. Berger, H. Schwichtenberg
    Pages 36-46

  5. Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids

    • Ilya Beylin, Peter Dybjer
    Pages 47-61

  6. A constructive proof of the Heine-Borel covering theorem for formal reals

    • Jan Cederquist, Sara Negri
    Pages 62-75

  7. An application of constructive completeness

    • Thierry Coquand, Jan M. Smith
    Pages 76-84

  8. Automating inversion of inductive predicates in Coq

    • Cristina Cornes, Delphine Terrasse
    Pages 85-104

  9. First order marked types

    • Philippe Curmin
    Pages 105-119

  10. Internal type theory

    • Peter Dybjer
    Pages 120-134

  11. An application of co-inductive types in Coq: Verification of the alternating bit protocol

    • Eduardo Giménez
    Pages 135-152

  12. Conservativity of equality reflection over intensional type theory

    • Martin Hofmann
    Pages 153-164

  13. A natural deduction approach to dynamic logic

    • Furio Honsell, Marino Miculan
    Pages 165-182

  14. An algorithm for checking incomplete proof objects in type theory with localization and unification

    • Lena Magnusson
    Pages 183-200

  15. Decidability of all minimal models

    • Vincent Padovani
    Pages 201-215

  16. Circuits as streams in Coq: Verification of a sequential multiplier

    • Christine Paulin-Mohring
    Pages 216-230

  17. Context-relative syntactic categories and the formalization of mathematical text

    • Aarne Ranta
    Pages 231-248

  18. A simple model construction for the Calculus of Constructions

    • M. Stefanova, H. Geuvers
    Pages 249-264

  19. Optimized encodings of fragments of type theory in first order logic

    • Tanel Tammet, Jan M. Smith
    Pages 265-287

  20. Organization and development of a constructive axiomatization

    • Jan von Plato
    Pages 288-296
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

About this book

This volume contains a refereed selection of revised full papers chosen from the contributions presented during the Third Annual Workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs. The workshop took place in Torino, Italy, in June 1995.
Type theory is a formalism in which theorems and proofs, specifications and programs can be represented in a uniform way. The 19 papers included in the book deal with foundations of type theory, logical frameworks, and implementations and applications; all in all they constitute a state-of-the-art survey for the area of type theory.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation