Types for Proofs and Programs International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers /
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 .
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.
9783540744641
10.1007/978-3-540-74464-1 doi
Compilers (Computer programs).
Computer science.
Machine theory.
Computer science--Mathematics.
Artificial intelligence.
Compilers and Interpreters.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Symbolic and Algebraic Manipulation.
Artificial Intelligence.
QA76.76.C65
005.45
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.
9783540744641
10.1007/978-3-540-74464-1 doi
Compilers (Computer programs).
Computer science.
Machine theory.
Computer science--Mathematics.
Artificial intelligence.
Compilers and Interpreters.
Computer Science Logic and Foundations of Programming.
Formal Languages and Automata Theory.
Symbolic and Algebraic Manipulation.
Artificial Intelligence.
QA76.76.C65
005.45