Produktbild: Types for Proofs and Programs
Band 4502

Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers

49,99 €

inkl. gesetzl. MwSt., Versandkostenfrei


Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

01.10.2007

Abbildungen

VIII, 272 p.

Herausgeber

Thorsten Altenkirch + weitere

Verlag

Springer Berlin

Seitenzahl

272

Maße (B/H)

15,5/23,5 cm

Gewicht

408 g

Sprache

Englisch

ISBN

978-3-540-74463-4

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

01.10.2007

Abbildungen

VIII, 272 p.

Herausgeber

Verlag

Springer Berlin

Seitenzahl

272

Maße (B/H)

15,5/23,5 cm

Gewicht

408 g

Sprache

Englisch

ISBN

978-3-540-74463-4

Herstelleradresse

Springer-Verlag GmbH
Heidelberger Platz 3
14197 Berlin
Deutschland
Email: sdc-bookservice@springer.com
Url: www.springer.com
Telephone: +49 6221 3454301
Fax: +49 30 8214091

Noch keine Bewertungen vorhanden

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kundinnen und Kunden durch Ihre Meinung.

Kundinnen und Kunden meinen

Bewertungen (0)

  • Produktbild: Types for Proofs and Programs
  • 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.