FEEDBACK Smiley face
Normal view MARC view ISBD view

Types for Proofs and Programs [electronic resource] :International Workshop, TYPES’99 Lökeberg, Sweden, June 12–16, 1999 Selected Papers /

Contributor(s): Coquand, Thierry [editor.] | Dybjer, Peter [editor.] | Nordström, Bengt [editor.] | Smith, Jan [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Lecture Notes in Computer Science: 1956Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2000.Description: VIII, 197 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540445579.Subject(s): Computer science | Programming languages (Electronic computers) | Computer logic | Mathematical logic | Artificial intelligence | Computer Science | Programming Languages, Compilers, Interpreters | Logics and Meanings of Programs | Mathematical Logic and Formal Languages | Artificial Intelligence (incl. Robotics) | Mathematical Logic and FoundationsOnline resources: Click here to access online
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.
In: Springer eBooks
Tags from this library: No tags from this library for this title. Add tag(s)
Log in to add tags.
    average rating: 0.0 (0 votes)
No physical items for this record

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.

There are no comments for this item.

Log in to your account to post a comment.

© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in