Skip to main content
SpringerLink
Log in
Book cover

Types for Proofs and Programs

International Workshop TYPES '94, Bastad, Sweden, June 6-10, 1994. Selected Papers

  • Conference proceedings
  • © 1995

Overview

Editors:
  1. Peter Dybjer
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Bengt Nordström
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Jan Smith
    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 996)

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 (10 papers)

  1. Front Matter

    Download chapter PDF

  2. Communicating contexts: A pragmatic approach to information exchange

    • René Ahn
    Pages 1-13

  3. A short and flexible proof of strong normalization for the calculus of constructions

    • Herman Geuvers
    Pages 14-38

  4. Codifying guarded definitions with recursive schemes

    • Eduarde Giménez
    Pages 39-59

  5. The metatheory of UTT

    • Healfdene Goguen
    Pages 60-82

  6. A user's friendly syntax to define recursive functions as typed λ-terms

    • Pascal Manoury
    Pages 83-100

  7. I/O automata in Isabelle/HOL

    • Tobias Nipkow, Konrad Slind
    Pages 101-119

  8. A concrete final coalgebra theorem for ZF set theory

    • Lawrence C. Paulson
    Pages 120-139

  9. On extensibility of proof checkers

    • Robert Pollack
    Pages 140-161

  10. Syntactic categories in the language of mathematics

    • Aarne Ranta
    Pages 162-182

  11. Formalization of a λ-calculus with explicit substitutions in Coq

    • Amokrane Saïbi
    Pages 183-202

  12. Back Matter

    Download chapter PDF
Back to top

Keywords

About this book

This book presents a strictly refereed collection of revised full papers selected from the papers accepted for the TYPES '94 Workshop, held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Bastad, Sweden, in June 1994.
The 10 papers included address various aspects of developing computer-assisted proofs and programs using a logical framework. Type theory and three logical frameworks based on it are dealt with: ALF, Coq, and LEGO; other topics covered are metatheory, the Isabelle system, 2-calculus, proof checkers, and ZF set theory.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation