Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers
by
Altenkirch, Thorsten. editor.
Title
:
Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers
Author
:
Altenkirch, Thorsten. editor.
ISBN
:
9783540744641
Physical Description
:
VIII, 272 p. online resource.
Series
:
Lecture Notes in Computer Science, 4502
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.
Subject Term
:
Computer science.
Logic design.
Algebra -- Data processing.
Artificial intelligence.
Logics and Meanings of Programs.
Mathematical Logic and Formal Languages.
Programming Languages, Compilers, Interpreters.
Symbolic and Algebraic Manipulation.
Artificial Intelligence (incl. Robotics).
Added Author
:
Altenkirch, Thorsten.
McBride, Conor.
Added Corporate Author
:
SpringerLink (Online service)
Electronic Access
:
Library | Material Type | Item Barcode | Shelf Number | Status |
---|
IYTE Library | E-Book | 512794-1001 | QA76.9 .L63 | Online Springer |