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. 
 - 1st ed. 2007. 
 - VIII, 272 p.  online resource. 
 - Theoretical Computer Science and General Issues,  4502  2512-2029 ; .
 - Theoretical Computer Science and General Issues,  4502 .
<br/><br/>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. 
<br/><br/><label>ISBN: </label>9783540744641 
<br/><br/><label>Standard No.: </label>10.1007/978-3-540-74464-1  doi 
<br/><br/><label>Subjects--Topical Terms: </label><br/>Compilers (Computer programs).<br/>Computer science.<br/>Machine theory.<br/>Computer science--Mathematics.<br/>Artificial intelligence.<br/>Compilers and Interpreters.<br/>Computer Science Logic and Foundations of Programming.<br/>Formal Languages and Automata Theory.<br/>Symbolic and Algebraic Manipulation.<br/>Artificial Intelligence.
<br/><br/><label>LC Class. No.: </label>QA76.76.C65 
<br/><br/><label>Dewey Class. No.: </label>005.45