Skip to main content
SpringerLink
Log in

Types for Proofs and Programs

International Workshop TYPES'96, Aussois, France, December 15-19, 1996 Selected Papers

  • Conference proceedings
  • © 1998

Overview

Editors:
  1. Eduardo Giménez
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Christine Paulin-Mohring
    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 1512)

Included in the following conference series:

Conference proceedings info: TYPES 1996.

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. Introduction

    Pages 1-8

  3. Coercion synthesis in computer implementations of type-theoretic frameworks

    • Anthony Bailey
    Pages 9-27

  4. Verification of the interface of a small proof system in coq

    • Bruno Barras
    Pages 28-45

  5. An implementation of the Heine-Borel covering theorem in type theory

    • Jan Cederquist
    Pages 46-65

  6. Detecting and removing dead-code using rank 2 intersection

    • Ferruccio Damiani, Frédéric Prost
    Pages 66-87

  7. A type-free formalization of mathematics where proofs are objects

    • Gilles Dowek
    Pages 88-111

  8. Higman's lemma in type theory

    • Daniel Fridlender
    Pages 112-133

  9. A proof of weak termination of typed λσ-calculi

    • Jean Goubault-Larrecq
    Pages 134-153

  10. Proof style

    • John Harrison
    Pages 154-172

  11. Some algorithmic and proof-theoretical aspects of coercive subtyping

    • Alex Jones, Zhaohui Luo, Sergei Soloviev
    Pages 173-195

  12. Semantical BNF

    • Petri Mäenpää
    Pages 196-215

  13. The internal type theory of a Heyting pretopos

    • Maria Emilia Maietti
    Pages 216-235

  14. Inverting inductively defined relations in LEGO

    • Conor McBride
    Pages 236-253

  15. A generic normalisation proof for pure type systems

    • Paul-André Melliès, Benjamin Werner
    Pages 254-276

  16. Proving a real time algorithm for ATM in Coq

    • Jean-François Monin
    Pages 277-293

  17. Dependent types with explicit substitutions: A meta-theoretical development

    • César Muñoz
    Pages 294-316

  18. Type inference verified: Algorithm W in Isabelle/HOL

    • Wolfgang Naraschewski, Tobias Nipkow
    Pages 317-332

  19. Continuous lattices in formal topology

    • Sara Negri
    Pages 333-353

  20. Abstract insertion sort in an extension of type theory with record types and subtyping

    • Alvaro Tasistro
    Pages 354-372
Back to top

Other volumes

  1. Types for Proofs and Programs

Keywords

About this book

This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996.
The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL.

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation