Blick ins Buch

Types for Proofs and Programs

International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers

Thorsten Altenkirch, Conor McBride (Herausgeber)

Buch | Softcover

VIII, 272 Seiten

2007 | 2007
Springer Berlin (Verlag)
978-3-540-74463-4 (ISBN)

Lese- und Medienproben

Blick ins Buch (midvox)

Artikel merken

lt;p>The refereed post-proceedings of the International Workshop of the Types Working Group are presented in this volume. The 17 papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education.

Weyl's Predicative Classical Mathematics as a Logic-Enriched Type Theory.- Crafting a Proof Assistant.- On Constructive Cut Admissibility in Deduction Modulo.- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond.- Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq.- Deciding Equality in the Constructor Theory.- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family.- Truth Values Algebras and Proof Normalization.- Curry-Style Types for Nominal Terms.- (In)consistency of Extensions of Higher Order Logic and Type Theory.- Constructive Type Classes in Isabelle.- Zermelo's Well-Ordering Theorem in Type Theory.- A Finite First-Order Theory of Classes.- Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers.- Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs.- Subset Coercions in Coq.- A Certified Distributed Security Logic for Authorizing Code.

Erscheint lt. Verlag	1.10.2007
Reihe/Serie	Lecture Notes in Computer Science
Reihe/Serie	Theoretical Computer Science and General Issues
Zusatzinfo	VIII, 272 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	408 g
Themenwelt	Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
Themenwelt	Informatik ► Theorie / Studium ► Compilerbau
Schlagworte	algorithms • formal methods • Formal Reasoning • formal specification • Formal Verification • Functional Programming • Hardcover, Softcover / Informatik, EDV/Informatik • HC/Informatik, EDV/Informatik • Higher Order Logic • Isabell • Isabelle • Logic • Polymorphism • programming • Programming language • Programming Logic • Programming Theory • Program Semantics • Proof theory • Rewriting Systems • subtyping • theorem proving • type inference • Types • Type Systems • verification
ISBN-10	3-540-74463-0 / 3540744630
ISBN-13	978-3-540-74463-4 / 9783540744634
Zustand	Neuware