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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Coquand, Thierry (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Dybjer, Peter (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Nordström, Bengt (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Smith, Jan (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2000.
• Έκδοση: 1st ed. 2000.
• Σειρά: Lecture Notes in Computer Science, 1956
• Θέματα: 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.

Πίνακας περιεχομένων:

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