Computer Science Logic [[electronic resource] ] : 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings / / edited by Zoltán Ésik
| Computer Science Logic [[electronic resource] ] : 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings / / edited by Zoltán Ésik |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (XII, 627 p.) |
| Disciplina | 005.1/015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Machine theory Artificial intelligence Mathematical logic Compilers and Interpreters Theory of Computation Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Mathematical Logic and Foundations |
| ISBN | 3-540-45459-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Presentations -- Functorial Boxes in String Diagrams -- Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract) -- Automata and Logics for Words and Trees over an Infinite Alphabet -- Nonmonotonic Logics and Their Algebraic Foundations -- Contributions -- Semi-continuous Sized Types and Termination -- Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation -- A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata -- The Power of Linear Functions -- Logical Omniscience Via Proof Complexity -- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic -- MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay -- Abstracting Allocation -- Collapsibility in Infinite-Domain Quantified Constraint Satisfaction -- Towards an Implicit Characterization of NC k -- On Rational Trees -- Reasoning About States of Probabilistic Sequential Programs -- Concurrent Games with Tail Objectives -- Nash Equilibrium for Upward-Closed Objectives -- Algorithms for Omega-Regular Games with Imperfect Information -- Relating Two Standard Notions of Secrecy -- Jump from Parallel to Sequential Proofs: Multiplicatives -- First-Order Queries over One Unary Function -- Infinite State Model-Checking of Propositional Dynamic Logics -- Weak Bisimulation Approximants -- Complete Problems for Higher Order Logics -- Solving Games Without Determinization -- Game Quantification on Automatic Structures and Hierarchical Model Checking Games -- An Algebraic Point of View on the Crane Beach Property -- A Sequent Calculus for Type Theory -- Universality Results for Models in Locally Boolean Domains -- Universal Structures and the Logic of Forbidden Patterns -- On the Expressive Power of Graph Logic -- Hoare Logic in the Abstract -- Normalization of IZF with Replacement -- Acyclicity and Coherence in Multiplicative Exponential Linear Logic -- Church Synthesis Problem with Parameters -- Decidable Theories of the Ordering of Natural Numbers with Unary Predicates -- Separation Logic for Higher-Order Store -- Satisfiability and Finite Model Property for the Alternating-Time ?-Calculus -- Space-Efficient Computation by Interaction -- The Ackermann Award 2006. |
| Record Nr. | UNISA-996465977603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Science Logic : 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings / / edited by Zoltán Ésik
| Computer Science Logic : 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings / / edited by Zoltán Ésik |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 |
| Descrizione fisica | 1 online resource (XII, 627 p.) |
| Disciplina | 005.1/015113 |
| Altri autori (Persone) | ÉsikZoltán <1951-> |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Machine theory Artificial intelligence Logic, Symbolic and mathematical Compilers and Interpreters Theory of Computation Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Mathematical Logic and Foundations |
| ISBN | 3-540-45459-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Presentations -- Functorial Boxes in String Diagrams -- Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract) -- Automata and Logics for Words and Trees over an Infinite Alphabet -- Nonmonotonic Logics and Their Algebraic Foundations -- Contributions -- Semi-continuous Sized Types and Termination -- Visibly Pushdown Automata: From Language Equivalence to Simulation and Bisimulation -- A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata -- The Power of Linear Functions -- Logical Omniscience Via Proof Complexity -- Verification of Ptime Reducibility for System F Terms Via Dual Light Affine Logic -- MSO Queries on Tree Decomposable Structures Are Computable with Linear Delay -- Abstracting Allocation -- Collapsibility in Infinite-Domain Quantified Constraint Satisfaction -- Towards an Implicit Characterization of NC k -- On Rational Trees -- Reasoning About States of Probabilistic Sequential Programs -- Concurrent Games with Tail Objectives -- Nash Equilibrium for Upward-Closed Objectives -- Algorithms for Omega-Regular Games with Imperfect Information -- Relating Two Standard Notions of Secrecy -- Jump from Parallel to Sequential Proofs: Multiplicatives -- First-Order Queries over One Unary Function -- Infinite State Model-Checking of Propositional Dynamic Logics -- Weak Bisimulation Approximants -- Complete Problems for Higher Order Logics -- Solving Games Without Determinization -- Game Quantification on Automatic Structures and Hierarchical Model Checking Games -- An Algebraic Point of View on the Crane Beach Property -- A Sequent Calculus for Type Theory -- Universality Results for Models in Locally Boolean Domains -- Universal Structures and the Logic of Forbidden Patterns -- On the Expressive Power ofGraph Logic -- Hoare Logic in the Abstract -- Normalization of IZF with Replacement -- Acyclicity and Coherence in Multiplicative Exponential Linear Logic -- Church Synthesis Problem with Parameters -- Decidable Theories of the Ordering of Natural Numbers with Unary Predicates -- Separation Logic for Higher-Order Store -- Satisfiability and Finite Model Property for the Alternating-Time ?-Calculus -- Space-Efficient Computation by Interaction -- The Ackermann Award 2006. |
| Record Nr. | UNINA-9910483865403321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2006 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Computer Science Logic [[electronic resource] ] : 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings / / edited by Luke Ong
| Computer Science Logic [[electronic resource] ] : 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings / / edited by Luke Ong |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XI, 567 p.) |
| Disciplina | 005.1/015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Machine theory Artificial intelligence Mathematical logic Compilers and Interpreters Theory of Computation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Artificial Intelligence Mathematical Logic and Foundations |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Lectures -- XML Navigation and Tarski’s Relation Algebras -- Verification in Predicate Logic with Time: Algorithmic Questions -- Note on Formal Analogical Reasoning in the Juridical Context -- An Abstract Strong Normalization Theorem -- Semantics and Logics -- On Bunched Polymorphism -- Distributed Control Flow with Classical Modal Logic -- A Logic of Coequations -- A Semantic Formulation of ???-Lifting and Logical Predicates for Computational Metalanguage -- Type Theory and Lambda Calculus -- Order Structures on Böhm-Like Models -- Higher-Order Matching and Games -- Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations -- On the Role of Type Decorations in the Calculus of Inductive Constructions -- Linear Logic and Ludics -- L-Nets, Strategies and Proof-Nets -- Permutative Logic -- Focusing the Inverse Method for Linear Logic -- Towards a Typed Geometry of Interaction -- Constraints -- From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction -- An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints -- Finite Models, Decidability and Complexity -- Coprimality in Finite Models -- Towards a Characterization of Order-Invariant Queries over Tame Structures -- Decidability of Term Algebras Extending Partial Algebras -- Results on the Guarded Fragment with Equivalence or Transitive Relations -- The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic -- On the Complexity of Hybrid Logics with Binders -- The Complexity of Independence-Friendly Fixpoint Logic -- Closure Properties of Weak Systems of Bounded Arithmetic -- Verification and Model Checking -- Transfinite Extension of the Mu-Calculus -- Bounded Model Checking of Pointer Programs -- PDL with Intersection and Converse Is Decidable -- On Deciding Topological Classes of Deterministic Tree Languages -- Constructive Reasoning and Computational Mathematics -- Complexity and Intensionality in a Type-1 Framework for Computable Analysis -- Computing with Sequences, Weak Topologies and the Axiom of Choice -- Light Functional Interpretation -- Feasible Proofs of Matrix Properties with Csanky’s Algorithm -- Implicit Computational Complexity and Rewriting -- A Propositional Proof System for Log Space -- Identifying Polynomial-Time Recursive Functions -- Confluence of Shallow Right-Linear Rewrite Systems -- Appendices -- The Ackermann Award 2005 -- Clemens Lautemann: 1951-2005 An Obituary. |
| Record Nr. | UNISA-996465924403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Computer Science Logic : 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings / / edited by Luke Ong
| Computer Science Logic : 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings / / edited by Luke Ong |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XI, 567 p.) |
| Disciplina | 005.1/015113 |
| Altri autori (Persone) | OngLuke |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Computer science Machine theory Artificial intelligence Logic, Symbolic and mathematical Compilers and Interpreters Theory of Computation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Artificial Intelligence Mathematical Logic and Foundations |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Lectures -- XML Navigation and Tarski’s Relation Algebras -- Verification in Predicate Logic with Time: Algorithmic Questions -- Note on Formal Analogical Reasoning in the Juridical Context -- An Abstract Strong Normalization Theorem -- Semantics and Logics -- On Bunched Polymorphism -- Distributed Control Flow with Classical Modal Logic -- A Logic of Coequations -- A Semantic Formulation of ???-Lifting and Logical Predicates for Computational Metalanguage -- Type Theory and Lambda Calculus -- Order Structures on Böhm-Like Models -- Higher-Order Matching and Games -- Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations -- On the Role of Type Decorations in the Calculus of Inductive Constructions -- Linear Logic and Ludics -- L-Nets, Strategies and Proof-Nets -- Permutative Logic -- Focusing the Inverse Method for Linear Logic -- Towards a Typed Geometry of Interaction -- Constraints -- From Pebble Games to Tractability: An Ambidextrous Consistency Algorithm for Quantified Constraint Satisfaction -- An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints -- Finite Models, Decidability and Complexity -- Coprimality in Finite Models -- Towards a Characterization of Order-Invariant Queries over Tame Structures -- Decidability of Term Algebras Extending Partial Algebras -- Results on the Guarded Fragment with Equivalence or Transitive Relations -- The Modular Decomposition of Countable Graphs: Constructions in Monadic Second-Order Logic -- On the Complexity of Hybrid Logics with Binders -- The Complexity of Independence-Friendly Fixpoint Logic -- Closure Properties of Weak Systems of Bounded Arithmetic -- Verification and Model Checking -- Transfinite Extension of the Mu-Calculus -- Bounded Model Checking of Pointer Programs -- PDLwith Intersection and Converse Is Decidable -- On Deciding Topological Classes of Deterministic Tree Languages -- Constructive Reasoning and Computational Mathematics -- Complexity and Intensionality in a Type-1 Framework for Computable Analysis -- Computing with Sequences, Weak Topologies and the Axiom of Choice -- Light Functional Interpretation -- Feasible Proofs of Matrix Properties with Csanky’s Algorithm -- Implicit Computational Complexity and Rewriting -- A Propositional Proof System for Log Space -- Identifying Polynomial-Time Recursive Functions -- Confluence of Shallow Right-Linear Rewrite Systems -- Appendices -- The Ackermann Award 2005 -- Clemens Lautemann: 1951-2005 An Obituary. |
| Record Nr. | UNINA-9910484744203321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Lo trovi qui: Univ. Federico II | ||
| ||