Normal view MARC view ISBD view

Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers / [electronic resource] : edited by Thorsten Altenkirch, Conor McBride. - Berlin, Heidelberg : Springer Berlin Heidelberg, 2007. - VIII, 272 p. online resource. - Lecture Notes in Computer Science, 4502 0302-9743 ; . - Lecture Notes in Computer Science, 4502 .

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.

ISBN: 9783540744641

Standard No.: 10.1007/978-3-540-74464-1 doi

Subjects--Topical Terms:
Computer science.
Logic design.
Algebra--Data processing.
Artificial intelligence.
Computer Science.
Logics and Meanings of Programs.
Mathematical Logic and Formal Languages.
Programming Languages, Compilers, Interpreters.
Symbolic and Algebraic Manipulation.
Artificial Intelligence (incl. Robotics).

LC Class. No.: QA76.9.L63 QA76.5913 QA76.63

Dewey Class. No.: 005.1015113