FEEDBACK Smiley face
Normal view MARC view ISBD view

Types for Proofs and Programs [electronic resource] :International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers /

Contributor(s): Altenkirch, Thorsten [editor.] | McBride, Conor [editor.] | SpringerLink (Online service).
Material type: materialTypeLabelBookSeries: Lecture Notes in Computer Science: 4502Publisher: Berlin, Heidelberg : Springer Berlin Heidelberg, 2007.Description: VIII, 272 p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9783540744641.Subject(s): Computer science | Programming languages (Electronic computers) | Computer logic | Mathematical logic | Computer science -- Mathematics | Artificial intelligence | Computer Science | Programming Languages, Compilers, Interpreters | Logics and Meanings of Programs | Mathematical Logic and Formal Languages | Symbolic and Algebraic Manipulation | Artificial Intelligence (incl. Robotics)Online 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 eBooks
Tags from this library: No tags from this library for this title. Add tag(s)
Log in to add tags.
    average rating: 0.0 (0 votes)
No physical items for this 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.

There are no comments for this item.

Log in to your account to post a comment.

© IIIT-Delhi, 2013 | Phone: +91-11-26907510| FAX +91-11-26907405 | E-mail: library@iiitd.ac.in