TY  - BOOK
AU  - Altenkirch,Thorsten
AU  - McBride,Conor
ED  - SpringerLink (Online service)
TI  - Types for Proofs and Programs: International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers 
T2  - Lecture Notes in Computer Science,
SN  - 9783540744641
AV  - QA76.9.L63 
U1  - 005.1015113 23
PY  - 2007///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Logic design
KW  - Algebra
KW  - Data processing
KW  - Artificial intelligence
KW  - Computer Science
KW  - Logics and Meanings of Programs
KW  - Mathematical Logic and Formal Languages
KW  - Programming Languages, Compilers, Interpreters
KW  - Symbolic and Algebraic Manipulation
KW  - Artificial Intelligence (incl. Robotics)
N1  - 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
UR  - http://dx.doi.org/10.1007/978-3-540-74464-1
ER  -