Types for Proofs and Programs International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers /
Types for Proofs and Programs International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers / [electronic resource] :
edited by Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan Smith.
- 1st ed. 2000.
- VIII, 197 p. online resource.
- Lecture Notes in Computer Science, 1956 1611-3349 ; .
- Lecture Notes in Computer Science, 1956 .
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.
9783540445579
10.1007/3-540-44557-9 doi
Compilers (Computer programs).
Computer science.
Machine theory.
Artificial intelligence.
Mathematical logic.
Compilers and Interpreters.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Artificial Intelligence.
Mathematical Logic and Foundations.
QA76.76.C65
005.45
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.
9783540445579
10.1007/3-540-44557-9 doi
Compilers (Computer programs).
Computer science.
Machine theory.
Artificial intelligence.
Mathematical logic.
Compilers and Interpreters.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Artificial Intelligence.
Mathematical Logic and Foundations.
QA76.76.C65
005.45