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.
Theoretical Computer Science [[electronic resource] ] : 9th Italian Conference, ICTCS 2005, Siena, Italy, October 12-14, 2005, Proceedings / / edited by Mario Coppo, Elena Lodi, G. Michele Pinna
| Theoretical Computer Science [[electronic resource] ] : 9th Italian Conference, ICTCS 2005, Siena, Italy, October 12-14, 2005, Proceedings / / edited by Mario Coppo, Elena Lodi, G. Michele Pinna |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XI, 411 p.) |
| Disciplina | 004 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Artificial intelligence—Data processing Algorithms Machine theory Theory of Computation Data Science Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory |
| ISBN |
3-540-32024-5
3-540-29106-7 |
| Classificazione | 54.10 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Semantic Subtyping: Challenges, Perspectives, and Open Problems -- Biological Systems as Reactive Systems -- Mobile Agents Computing: Security Issues and Algorithmic Solutions -- Technical Contributions -- Efficient Algorithms for Detecting Regular Point Configurations -- Pickup and Delivery for Moving Objects on Broken Lines -- A Static Analysis of PKI-Based Systems -- Subtyping Object and Recursive Types Logically -- The Language ?: Circuits, Computations and Classical Logic -- Checking Risky Events Is Enough for Local Policies -- The Graph Rewriting Calculus: Confluence and Expressiveness -- Safe Object Composition in the Presence of Subtyping -- Reachability Analysis in Boxed Ambients -- Error Mining for Regular Expression Patterns -- Reconstructing an Alternate Periodical Binary Matrix from Its Orthogonal Projections -- Inapproximability Results for the Lateral Gene Transfer Problem -- Faster Deterministic Wakeup in Multiple Access Channels -- Weighted Coloring: Further Complexity and Approximability Results -- Quantum Algorithms for a Set of Group Theoretic Problems -- On the Computational Complexity of the L (2,1)-Labeling Problem for Regular Graphs -- A Polymerase Based Algorithm for SAT -- Laxity Helps in Broadcast Scheduling -- Enforcing and Defying Associativity, Commutativity, Totality, and Strong Noninvertibility for One-Way Functions in Complexity Theory -- Synthesis from Temporal Specifications Using Preferred Answer Set Programming -- Model Checking Strategic Abilities of Agents Under Incomplete Information -- Improved Algorithms for Polynomial-Time Decay and Time-Decay with Additive Error -- A Theoretical Analysis of Alignment and Edit Problems for Trees -- A Complete Formulation of Generalized Affine Equivalence -- A New Combinatorial Approach to Sequence Comparison -- A Typed Assembly Language for Non-interference -- Improved Exact Exponential Algorithms for Vertex Bipartization and Other Problems -- A Typed Semantics of Higher-Order Store and Subtyping -- Two Variables Are Not Enough. |
| Record Nr. | UNISA-996465861903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 | ||
| ||