IST Austria Library

Types for proofs and programs : international workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006 : revised selected papers / Thorsten Altenkirch, Conor McBride (eds.).

By: TYPES 2006 (2006 : Nottingham, England)
Contributor(s): Altenkirch, Thorsten, 1962- | McBride, Conor
Material type: TextTextSeries: SerienbezeichnungLecture notes in computer science: 4502.; LNCS sublibrary: Publisher: Berlin ; New York : Springer, ©2007Description: 1 online resource (viii, 268 pages) : illustrationsContent type: text Media type: computer Carrier type: online resourceISBN: 9783540744641; 3540744649; 9783540744634; 3540744630Other title: TYPES 2006Subject(s): Automatic theorem proving -- Congresses | Computer programming -- Congresses | Informatique | Automatic theorem proving | Computer programming | wiskunde | mathematics | computerwetenschappen | computer sciences | kunstmatige intelligentie | artificial intelligence | logica | logic | programmeertalen | programming languages | algebra | Information and Communication Technology (General) | Informatie- en communicatietechnologie (algemeen)Genre/Form: Electronic books. | Conference papers and proceedings. Additional physical formats: Print version:: Types for proofs and programs.DDC classification: 511.3 LOC classification: QA76.9.A96 | T96 2006ebOnline resources: Click here to access online
Contents:
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.
In: Springer e-booksSummary: This book constitutes the thoroughly refereed post-proceedings of the annual International Workshop of the Types Working Group, TYPES 2006, held in Nottingham, UK in April 2006 - co-located with the Seventh Symposium on Trends in Functional Programming, TFP 2006. The 17 revised full papers presented were carefully reviewed and selected from 29 submissions. All current issues of formal reasoning and computer programming based on type theory are addressed; in particular languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.
Tags from this library: No tags from this library for this title. Log in to add tags.
    Average rating: 0.0 (0 votes)
Item type Current location Collection Call number Status Date due Barcode Item holds
eBook eBook e-Library

Electronic Book@IST

 EBook Available
Total holds: 0

Includes bibliographical references and index.

Print version record.

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.

This book constitutes the thoroughly refereed post-proceedings of the annual International Workshop of the Types Working Group, TYPES 2006, held in Nottingham, UK in April 2006 - co-located with the Seventh Symposium on Trends in Functional Programming, TFP 2006. The 17 revised full papers presented were carefully reviewed and selected from 29 submissions. All current issues of formal reasoning and computer programming based on type theory are addressed; in particular languages and computerised tools for reasoning, and applications in several domains such as analysis of programming languages, certified software, formalisation of mathematics and mathematics education.

Remote access restricted to users with a valid UTM ID via VPN.

There are no comments for this item.

to post a comment.

Powered by Koha