Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (X, 412 p.) |
Disciplina | 004/.01/5113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
ISBN |
3-540-24849-8
3-540-22164-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A Modular Hierarchy of Logical Frameworks -- Tailoring Filter Models -- Locales and Locale Expressions in Isabelle/Isar -- to PAF!, a Proof Assistant for ML Programs Verification -- A Constructive Proof of Higman’s Lemma in Isabelle -- A Core Calculus of Higher-Order Mixins and Classes -- Type Inference for Nested Self Types -- Inductive Families Need Not Store Their Indices -- Modules in Coq Are and Will Be Correct -- Rewriting Calculus with Fixpoints: Untyped and First-Order Systems -- First-Order Reasoning in the Calculus of Inductive Constructions -- Higher-Order Linear Ramified Recurrence -- Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus -- Wellfounded Trees and Dependent Polynomial Functors -- Classical Proofs, Typed Processes, and Intersection Types -- “Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models -- Coercions in Hindley-Milner Systems -- Combining Incoherent Coercions for ? -Types -- Induction and Co-induction in Sequent Calculus -- QArith: Coq Formalisation of Lazy Rational Arithmetic -- Mobility Types in Coq -- Some Algebraic Structures in Lambda-Calculus with Inductive Types -- A Concurrent Logical Framework: The Propositional Fragment -- Formal Proof Sketches -- Applied Type System. |
Record Nr. | UNINA-9910144152703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani |
Edizione | [1st ed. 2004.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
Descrizione fisica | 1 online resource (X, 412 p.) |
Disciplina | 004/.01/5113 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Programming languages (Electronic computers)
Computer logic Mathematical logic Artificial intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence |
ISBN |
3-540-24849-8
3-540-22164-6 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A Modular Hierarchy of Logical Frameworks -- Tailoring Filter Models -- Locales and Locale Expressions in Isabelle/Isar -- to PAF!, a Proof Assistant for ML Programs Verification -- A Constructive Proof of Higman’s Lemma in Isabelle -- A Core Calculus of Higher-Order Mixins and Classes -- Type Inference for Nested Self Types -- Inductive Families Need Not Store Their Indices -- Modules in Coq Are and Will Be Correct -- Rewriting Calculus with Fixpoints: Untyped and First-Order Systems -- First-Order Reasoning in the Calculus of Inductive Constructions -- Higher-Order Linear Ramified Recurrence -- Confluence and Strong Normalisation of the Generalised Multiary ?-Calculus -- Wellfounded Trees and Dependent Polynomial Functors -- Classical Proofs, Typed Processes, and Intersection Types -- “Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like Lambda-Models -- Coercions in Hindley-Milner Systems -- Combining Incoherent Coercions for ? -Types -- Induction and Co-induction in Sequent Calculus -- QArith: Coq Formalisation of Lazy Rational Arithmetic -- Mobility Types in Coq -- Some Algebraic Structures in Lambda-Calculus with Inductive Types -- A Concurrent Logical Framework: The Propositional Fragment -- Formal Proof Sketches -- Applied Type System. |
Record Nr. | UNISA-996465431103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|