Types for proofs and programs

the long version

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