Types for Proofs and Programs International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers /

• Corporate Author: SpringerLink (Online service)
• Other Authors: Coquand, Thierry (Editor, http://id.loc.gov/vocabulary/relators/edt), Dybjer, Peter (Editor, http://id.loc.gov/vocabulary/relators/edt), Nordström, Bengt (Editor, http://id.loc.gov/vocabulary/relators/edt), Smith, Jan (Editor, http://id.loc.gov/vocabulary/relators/edt)
• Format: Electronic eBook
• Language: English
• Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2000.
• Edition: 1st ed. 2000.
• Series: Lecture Notes in Computer Science, 1956
• Subjects: Programming languages (Electronic computers).; Computer logic.; Mathematical logic.; Artificial intelligence.; Programming Languages, Compilers, Interpreters.; Logics and Meanings of Programs.; Mathematical Logic and Formal Languages.; Artificial Intelligence.; Mathematical Logic and Foundations.

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