Title: Types for proofs and programs
Description: 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>
Subjects: Type theory, Congresses, Computer programming, Automatic theorem proving