Types for Proofs and Programs

Types for Proofs and Programs: International Workshop, TYPES’99 Lökeberg, Sweden, June 12–16, 1999 Selected PapersAuthor: Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan Smith Published by Springer Berlin Heidelberg ISBN: 978-3-540-41517-6 DOI: 10.1007/3-540-44557-9Table of Contents:Specification and Verification of a Formal System for Structurally Recursive Functions
A Predicative Strong Normalisation Proof for a λCalculus with Interleaving Inductive Types
Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-Rule
Computer-Assisted Mathematics at Work
Specification of a Smart Card Operating System
Implementation Techniques for Inductive Types in Plastic
A Co-inductive Approach to Real Numbers
Information Retrieval in a Coq Proof Library Using Type Isomorphisms
Memory Management: An Abstract Formulation of Incremental Tracing
The Three Gap Theorem (Steinhaus Conjecture)
Formalising Formulas-as-Types-as-Objects