Skip to main content
  • Conference proceedings
  • © 1994

Types for Proofs and Programs

International Workshop TYPES '93, Nijmegen, The Netherlands, May 24 - 28, 1993. Selected Papers

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

Buy it now

Buying options

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

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

Table of contents (17 papers)

  1. Front Matter

  2. Introduction

    Pages 1-2
  3. Checking algorithms for Pure Type Systems

    • L. S. van Benthem Jutting, J. McKinna, R. Pollack
    Pages 19-61
  4. Infinite objects in type theory

    • Thierry Coquand
    Pages 62-78
  5. Logic of refinement types

    • Susumu Hayashi
    Pages 108-126
  6. Proof-checking a data link protocol

    • L. Helmink, M. P. A. Sellink, F. W. Vaandrager
    Pages 127-165
  7. Programming with streams in Coq a case study: The Sieve of Eratosthenes

    • François Leclerc, Christine Paulin-Mohring
    Pages 191-212
  8. The Alf proof editor and its proof engine

    • Lena Magnusson, Bengt Nordström
    Pages 213-237
  9. Encoding Z-style Schemas in type theory

    • Savi Maharaj
    Pages 238-262
  10. Closure under alpha-conversion

    • Randy Pollack
    Pages 313-332
  11. Machine Deduction

    • Christophe Raffalli
    Pages 333-351
  12. Semantics for abstract clauses

    • D. A. Wolfram
    Pages 366-383
  13. Back Matter

About this book

This volume contains thoroughly refereed and revised full papers selected from the presentations at the first workshop held under the auspices of the ESPRIT Basic Research Action 6453 Types for Proofs and Programs in Nijmegen, The Netherlands, in May 1993.
As the whole ESPRIT BRA 6453, this volume is devoted to the theoretical foundations, design and applications of systems for theory development. Such systems help in designing mathematical axiomatisation, performing computer-aided logical reasoning, and managing databases of mathematical facts; they are also known as proof assistants or proof checkers.

Bibliographic Information

Buy it now

Buying options

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