| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910483766003321 |
|
|
Titolo |
Types for Proofs and Programs : International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers / / edited by Thorsten Altenkirch, Conor McBride |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2007.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (VIII, 272 p.) |
|
|
|
|
|
|
Collana |
|
Theoretical Computer Science and General Issues, , 2512-2029 ; ; 4502 |
|
|
|
|
|
|
Altri autori (Persone) |
|
AltenkirchThorsten <1962-> |
McBrideConor |
|
|
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
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 |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
|
Sommario/riassunto |
|
The refereed post-proceedings of the International Workshop of the Types Working Group are presented in this volume. The 17 papers address all current issues in formal reasoning and computer programming based on type theory, including languages and computerized tools for reasoning; applications in several domains, such as analysis of programming languages; certified software; formalization of mathematics; and mathematics education. |
|
|
|
|
|
|
|
| |