Types for Proofs and Programs

International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers

208 Seiten, Taschenbuch

Kurzbeschreibung des Verlags

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.

• Reihe: Lecture Notes in Computer Science
• Themen: Informatik und Informationstechnologie Informatik Künstliche Intelligenz (KI)
• ISBN: 9783540415176
• Sprache: Englisch
• Erscheinungsdatum: 13.12.2000
• Größe: 235 x 155 mm
• Verlag: Springer
• Herausgegeben von: Bengt Nordström, Thierry Coquand, Jan Smith, Peter Dybjer