Skip to main content
SpringerLink
Log in

Types for Proofs and Programs

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

  • Conference proceedings
  • © 1994

Overview

Editors:
  1. Henk Barendregt
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Tobias Nipkow
    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 806)

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

  1. Front Matter

    Download chapter PDF

  2. Introduction

    Pages 1-2

  3. Proving strong normalization of CC by modifying realizability semantics

    • Thorsten Altenkirch
    Pages 3-18

  4. Checking algorithms for Pure Type Systems

    • L. S. van Benthem Jutting, J. McKinna, R. Pollack
    Pages 19-61

  5. Infinite objects in type theory

    • Thierry Coquand
    Pages 62-78

  6. Conservativity between logics and typed λ calculi

    • Herman Geuvers
    Pages 79-107

  7. Logic of refinement types

    • Susumu Hayashi
    Pages 108-126

  8. Proof-checking a data link protocol

    • L. Helmink, M. P. A. Sellink, F. W. Vaandrager
    Pages 127-165

  9. Elimination of extensionality in Martin-Löf type theory

    • Martin Hofmann
    Pages 166-190

  10. Programming with streams in Coq a case study: The Sieve of Eratosthenes

    • François Leclerc, Christine Paulin-Mohring
    Pages 191-212

  11. The Alf proof editor and its proof engine

    • Lena Magnusson, Bengt Nordström
    Pages 213-237

  12. Encoding Z-style Schemas in type theory

    • Savi Maharaj
    Pages 238-262

  13. The expressive power of Structural Operational Semantics with explicit assumptions

    • Marino Miculan
    Pages 263-290

  14. Developing certified programs in the system Coq the program tactic

    • C. Parent
    Pages 291-312

  15. Closure under alpha-conversion

    • Randy Pollack
    Pages 313-332

  16. Machine Deduction

    • Christophe Raffalli
    Pages 333-351

  17. Type theory and the informal language of mathematics

    • Aarne Ranta
    Pages 352-365

  18. Semantics for abstract clauses

    • D. A. Wolfram
    Pages 366-383

  19. Back Matter

    Download chapter PDF
Back to top

Keywords

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

Publish with us

Policies and ethics

Back to top

Search

Navigation