Table of contents

  1. Front Matter
  2. Pages 1-2
  3. L. S. van Benthem Jutting, J. McKinna, R. Pollack
    Pages 19-61
  4. Thierry Coquand
    Pages 62-78
  5. Susumu Hayashi
    Pages 108-126
  6. L. Helmink, M. P. A. Sellink, F. W. Vaandrager
    Pages 127-165
  7. François Leclerc, Christine Paulin-Mohring
    Pages 191-212
  8. Lena Magnusson, Bengt Nordström
    Pages 213-237
  9. Savi Maharaj
    Pages 238-262
  10. Randy Pollack
    Pages 313-332
  11. Christophe Raffalli
    Pages 333-351
  12. D. A. Wolfram
    Pages 366-383
  13. Back Matter

About these proceedings


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.


Lambda-Calculus Machine Deduction Maschinelles Schließen Proof Checking Theorem Proving Typentheorie Types databases linear optimization logical reasoning

Bibliographic information

  • DOI
  • Copyright Information Springer-Verlag Berlin Heidelberg 1994
  • Publisher Name Springer, Berlin, Heidelberg
  • eBook Packages Springer Book Archive
  • Print ISBN 978-3-540-58085-0
  • Online ISBN 978-3-540-48440-0
  • Series Print ISSN 0302-9743
  • Series Online ISSN 1611-3349
  • Buy this book on publisher's site
Industry Sectors
Finance, Business & Banking
IT & Software
Consumer Packaged Goods