Types for Proofs and Programs -

Types for Proofs and Programs

International Workshop, TYPES'99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers
Buch | Softcover
X, 202 Seiten
2000 | 2000
Springer Berlin (Verlag)
978-3-540-41517-6 (ISBN)
53,49 inkl. MwSt
This book contains a selection of papers presented at the third annual workshop of the Esprit Working Group 21900 Types, which was held 12 - 16 June 1999 at L okeberg in the rural area north of G oteborg and close to Marstrand. It was attended by 77 researchers. The two previous workshops of the working group were held in Aussois, France, in December 1996 and in Irsee, Germany, in March 1998. The proc- dings of those workshops appear as LNCS Vol. 1512 (edited by Christine Paulin- Mohring and Eduardo Gimenez) and LNCS Vol. 1657 (edited by Thorsten - tenkirch, Wolfgang Naraschewski, and Bernhard Reus). These workshops are, in turn, a continuation of the meetings organized in 1993, 1994, and 1995 under the auspices of the Esprit Basic Research Action 6453 Types for Proofs and Programs. Those proceedings were also published in the LNCS series, edited by Henk Barendregt and Tobias Nipkow (Vol. 806, 1993), by Peter Dybjer, Bengt Nordstr om, and Jan Smith (Vol. 996, 1994) and by Stefano Berardi and Mario Coppo (Vol. 1158, 1995). The Esprit BRA 6453 was a continuation of the former Esprit Action 3245 Logical Frameworks: - sign, Implementation and Experiments. The articles from the annual workshops organized under that Action were edited by Gerard Huet and Gordon Plotkin in the books Logical Frameworks and Logical Environments, both published by Cambridge University Press.

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.

Erscheint lt. Verlag 13.12.2000
Reihe/Serie Lecture Notes in Computer Science
Zusatzinfo X, 202 p.
Verlagsort Berlin
Sprache englisch
Maße 155 x 235 mm
Gewicht 299 g
Themenwelt Mathematik / Informatik Informatik Programmiersprachen / -werkzeuge
Informatik Theorie / Studium Compilerbau
Schlagworte Beweis (Math.) • Coq • Formalismus (Logik) • formal methods • formal specification • Formal Verification • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Inductive Types • Lambda Calculus • programming • Programming Logics • Programming Theory • Program Semantics • Proof theory • Rewriting Systems • Types • Type Systems • verification
ISBN-10 3-540-41517-3 / 3540415173
ISBN-13 978-3-540-41517-6 / 9783540415176
Zustand Neuware
Haben Sie eine Frage zum Produkt?
Mehr entdecken
aus dem Bereich
Grundlagen und Anwendungen

von Hanspeter Mössenböck

Buch | Softcover (2024)
dpunkt (Verlag)
29,90