Types for Proofs and Programs: International Workshop, TYPES'99 Lökeberg, Sweden, June 12-16, 1999 Selected Papers (Lecture Notes in Computer Science, 1956, Band 1956) - Softcover

 
9783540415176: Types for Proofs and Programs: International Workshop, TYPES'99 Lökeberg, Sweden, June 12-16, 1999 Selected Papers (Lecture Notes in Computer Science, 1956, Band 1956)
Softcover
ISBN 10: 3540415173 ISBN 13: 9783540415176
Verlag: Springer, 2009

Inhaltsangabe

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.

Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.

Verlag
Springer
Erscheinungsdatum
2009
Sprache
Englisch
ISBN 10 
3540415173
ISBN 13 
9783540415176
Einband
Taschenbuch
Anzahl der Seiten
208
Herausgeber
Coquand Thierry
Kontakt zum Hersteller
Springer Nature Customer Service Center GmbH
ProductSafety@springernature.com

Europaplatz 3
Heidelberg
69115
Deutschland