Types for Proofs and Programs
Subtitle: International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers (Lecture Notes in Computer Science)
Contributors: Thierry Coquand (Editor); Peter Dybjer (Editor); Bengt Nordström (Editor); Jan Smith (Editor)
Edition: 1 edition
Publisher: Springer
Published: February 8, 2001
Language: eng
Format: Paperback
Number of pages: 195
ISBN-13: 9783540415176
Subjects: Programming languages; Congresses; Computer Logic; Programming - General; Automata; Computers; Computers - Languages / Programming; Computer Books: Languages; Computer Science; Logic Design; Programming Languages - General; Computers / Logic Design; Formal Methods; Formal Specification; Formal Verification; Inductive Types; Lambda Calculus; Program Semantics; Programming Logics; Automatic theorem proving; Type theory; Computer programming
First sentence: In lambda calculi with inductive types the standard means to construct a function over an inductive type is the recursor.
Description: Types for Proofs and Programs: International Workshop, TYPES’99 Lökeberg, Sweden, June 12–16, 1999 Selected Papers<br />Author: Thierry Coquand, Peter Dybjer, Bengt Nordström, Jan Smith<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-41517-6<br /> DOI: 10.1007/3-540-44557-9<br /><br />Table of Contents:<p></p><ul><li>Specification and Verification of a Formal System for Structurally Recursive Functions
</li><li>A Predicative Strong Normalisation Proof for a λCalculus with Interleaving Inductive Types
</li><li>Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-Rule
</li><li>Computer-Assisted Mathematics at Work
</li><li>Specification of a Smart Card Operating System
</li><li>Implementation Techniques for Inductive Types in Plastic
</li><li>A Co-inductive Approach to Real Numbers
</li><li>Information Retrieval in a Coq Proof Library Using Type Isomorphisms
</li><li>Memory Management: An Abstract Formulation of Incremental Tracing
</li><li>The Three Gap Theorem (Steinhaus Conjecture)
</li><li>Formalising Formulas-as-Types-as-Objects</li></ul>