Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
Types for Proofs and Programs [[electronic resource] ] : International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers / / edited by Stefano Berardi, Ferruccio Damiani, Ugo de Liguoro
| Types for Proofs and Programs [[electronic resource] ] : International Conference, TYPES 2008 Torino, Italy, March 26-29, 2008 Revised Selected Papers / / edited by Stefano Berardi, Ferruccio Damiani, Ugo de Liguoro |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 |
| Descrizione fisica | 1 online resource (VIII, 323 p.) |
| Disciplina | 005.13122gerDNB |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer programming
Computer science Machine theory Compilers (Computer programs) Computer science—Mathematics Artificial intelligence Programming Techniques Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Compilers and Interpreters Symbolic and Algebraic Manipulation Artificial Intelligence |
| ISBN | 3-642-02444-0 |
| Classificazione |
DAT 373f
DAT 510f DAT 706f SS 4800 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Type Inference by Coinductive Logic Programming -- About the Formalization of Some Results by Chebyshev in Number Theory -- A New Elimination Rule for the Calculus of Inductive Constructions -- A Framework for the Analysis of Access Control Models for Interactive Mobile Devices -- Proving Infinitary Normalization -- First-Class Object Sets -- Monadic Translation of Intuitionistic Sequent Calculus -- Towards a Type Discipline for Answer Set Programming -- Type Inference for a Polynomial Lambda Calculus -- Local Theory Specifications in Isabelle/Isar -- Axiom Directed Focusing -- A Type System for Usage of Software Components -- Merging Procedural and Declarative Proof -- Using Structural Recursion for Corecursion -- Manifest Fields and Module Mechanisms in Intensional Type Theory -- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq -- Coalgebraic Reasoning in Coq: Bisimulation and the ?-Coiteration Scheme -- A Process-Model for Linear Programs -- Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets. |
| Record Nr. | UNISA-996465856203316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for proofs and programs : international conference, TYPES 2008, Torino, Italy, March 26-29, 2008 : revised selected papers / / Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro (eds.)
| Types for proofs and programs : international conference, TYPES 2008, Torino, Italy, March 26-29, 2008 : revised selected papers / / Stefano Berardi, Ferruccio Damiani, Ugo de'Liguoro (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer, c2009 |
| Descrizione fisica | 1 online resource (VIII, 323 p.) |
| Disciplina | 005.13122gerDNB |
| Altri autori (Persone) |
BerardiStefano
DamianiFerruccio De'LiguoroUgo |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer programming |
| ISBN | 3-642-02444-0 |
| Classificazione |
DAT 373f
DAT 510f DAT 706f SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Type Inference by Coinductive Logic Programming -- About the Formalization of Some Results by Chebyshev in Number Theory -- A New Elimination Rule for the Calculus of Inductive Constructions -- A Framework for the Analysis of Access Control Models for Interactive Mobile Devices -- Proving Infinitary Normalization -- First-Class Object Sets -- Monadic Translation of Intuitionistic Sequent Calculus -- Towards a Type Discipline for Answer Set Programming -- Type Inference for a Polynomial Lambda Calculus -- Local Theory Specifications in Isabelle/Isar -- Axiom Directed Focusing -- A Type System for Usage of Software Components -- Merging Procedural and Declarative Proof -- Using Structural Recursion for Corecursion -- Manifest Fields and Module Mechanisms in Intensional Type Theory -- A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq -- Coalgebraic Reasoning in Coq: Bisimulation and the ?-Coiteration Scheme -- A Process-Model for Linear Programs -- Some Complexity and Expressiveness Results on Multimodal and Stratified Proof Nets. |
| Altri titoli varianti | TYPES 2007 |
| Record Nr. | UNINA-9910483948103321 |
| Berlin ; ; Heidelberg, : Springer, c2009 | ||
| Materiale a stampa | ||
| 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
| 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 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Types for Proofs and Programs : International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers / / edited by Stefano Berardi, Mario Coppo, Ferruccio Damiani
| Types for Proofs and Programs : 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 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers / / edited by Stefano Berardi, Mario Coppo
| Types for Proofs and Programs [[electronic resource] ] : International Workshop, TYPES '95, Torino, Italy, June 5 - 8, 1995 Selected Papers / / edited by Stefano Berardi, Mario Coppo |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (X, 298 p.) |
| Disciplina | 511.3/0285 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Mathematical logic
Software engineering Computers Computer logic Programming languages (Electronic computers) Artificial intelligence Mathematical Logic and Formal Languages Software Engineering/Programming and Operating Systems Theory of Computation Logics and Meanings of Programs Programming Languages, Compilers, Interpreters Artificial Intelligence |
| ISBN | 3-540-70722-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Implicit coercions in type systems -- A two-level approach towards lean proof-checking -- The greatest common divisor: A case study for program extraction from classical proofs -- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids -- A constructive proof of the Heine-Borel covering theorem for formal reals -- An application of constructive completeness -- Automating inversion of inductive predicates in Coq -- First order marked types -- Internal type theory -- An application of co-inductive types in Coq: Verification of the alternating bit protocol -- Conservativity of equality reflection over intensional type theory -- A natural deduction approach to dynamic logic -- An algorithm for checking incomplete proof objects in type theory with localization and unification -- Decidability of all minimal models -- Circuits as streams in Coq: Verification of a sequential multiplier -- Context-relative syntactic categories and the formalization of mathematical text -- A simple model construction for the Calculus of Constructions -- Optimized encodings of fragments of type theory in first order logic -- Organization and development of a constructive axiomatization. |
| Record Nr. | UNISA-996465861103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||