![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
Logical Methods in Computer Science, Volume 8
Volume 8, Number 1, 2012
- Assalé Adjé, Stéphane Gaubert, Eric Goubault:
Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. - Cyril Cohen, Assia Mahboubi:
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. - Denis Cousineau:
On completeness of reducibility candidates as a semantics of strong normalization. - Tomasz Mazur, Gavin Lowe:
A type reduction theory for systems with replicated components. - Mikolaj Bojanczyk, Slawomir Lasota:
An extension of data automata that captures XPath. - Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli
:
Ground interpolation for the theory of equality. - Libor Barto, Marcin Kozik:
Absorbing Subalgebras, Cyclic Terms, and the Constraint Satisfaction Problem. - James Cheney
:
A dependent nominal type theory. - Grigore Rosu, Feng Chen:
Semantics and Algorithms for Parametric Monitoring. - Jean-Louis Krivine:
Realizability algebras II : new models of ZF + DC. - Pablo Arrighi, Alejandro Díaz-Caro
:
Scalar System F for Linear-Algebraic Lambda-Calculus: Towards a Quantum Physical Logic. - Sebastian Rudolph
, Markus Krötzsch
, Pascal Hitzler:
Type-elimination-based reasoning for the description logic SHIQbs using decision diagrams and disjunctive datalog. - Seth Fogarty, Moshe Y. Vardi:
Büchi Complementation and Size-Change Termination. - Jean Goubault-Larrecq:
QRB-Domains and the Probabilistic Powerdomain. - Thomas Schwentick, Thomas Zeume:
Two-Variable Logic with Two Order Relations. - Thomas Braibant, Damien Pous
:
Deciding Kleene Algebras in Coq. - Viviana Bono
, Luca Padovani
:
Typing Copyless Message Passing. - Andrea Asperti
, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi:
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. - Gunnar Wilken
, Andreas Weiermann
:
Derivation Lengths Classification of Gödel's T Extending Howard's Assignment. - Matthias Baaz
, Agata Ciabattoni
, Christian G. Fermüller:
Theorem proving for prenex Gödel logic with Delta: checking validity and unsatisfiability. - Diego Figueira
:
Alternating register automata on finite words and trees. - Paul Potgieter:
The rapid points of a complex oscillation. - Giuseppe Castagna
, Mariangiola Dezani-Ciancaglini
, Luca Padovani
:
On Global Types and Multi-Party Session. - Stephen A. Cook, Lila Fontes:
Formal Theories for Linear Algebra. - Antoine Miné:
Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs. - Stephan Kreutzer:
On the Parameterized Intractability of Monadic Second-Order Logic. - Beniamino Accattoli, Delia Kesner:
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus. - Andreas Abel, Gabriel Scherer:
On Irrelevance and Algorithmic Equality in Predicative Type Theory. - Freek Wiedijk:
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving. - Takahito Aoto, Yoshihito Toyama:
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems. - Isolde Adler, Mark Weyer:
Tree-width for first order formulae.
Volume 8, Number 2, 2012
- Benedikt Ahrens
:
Extended Initiality for Typed Abstract Syntax. - Aquinas Hobor, Cristian Gherghina:
Barriers in Concurrent Separation Logic: Now With Tool Support! - Martin Mundhenk, Felix Weiss:
Intuitionistic implication makes model checking hard. - Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise:
Quantifier-Free Interpolation of a Theory of Arrays. - Thomas P. Jensen, Florent Kirchner, David Pichardie:
Secure the Clones. - Patrick Bahr
:
Modes of Convergence for Term Graph Rewriting. - Matteo Mio:
On the equivalence of game and denotational semantics for the probabilistic mu-calculus. - Alasdair Urquhart:
Width and size of regular resolution proofs. - Robert Atkey
, Patricia Johann, Neil Ghani:
Refining Inductive Types. - Cynthia Kop, Femke van Raamsdonk:
Dynamic Dependency Pairs for Algebraic Functional Systems. - Rémi Bonnet, Alain Finkel, Jérôme Leroux, Marc Zeitoun:
Model Checking Vector Addition Systems with one zero-test. - Neil Ghani, Patricia Johann, Clément Fumex:
Generic Fibrational Induction. - Damien Pous
:
Untyping Typed Algebras and Colouring Cyclic Linear Logic. - Christian Urban, Cezary Kaliszyk
:
General Bindings and Alpha-Equivalence in Nominal Isabelle. - Douglas S. Bridges:
Precompact Apartness Spaces. - Tino Teige, Martin Fränzle
:
Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems with Applications to Probabilistic State Reachability and Region Stability. - Lijun Zhang, David N. Jansen
, Flemming Nielson
, Holger Hermanns
:
Automata-Based CSL Model Checking. - Alessandro Cimatti
, Iman Narasamdya, Marco Roveri
:
Software Model Checking with Explicit Scheduler and Symbolic Threads.
Volume 8, Number 3, 2012
- Matthew J. Parkinson, Alexander J. Summers:
The Relationship Between Separation Logic and Implicit Dynamic Frames. - Clemens Kupke, Alexander Kurz, Yde Venema:
Completeness for the coalgebraic cover modality. - Alberto Griggio
, Thi Thieu Hoa Le, Roberto Sebastiani:
Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic. - Naoki Nishida, Masahiko Sakai
, Toshiki Sakabe:
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity. - Dai Tri Man Le, Stephen A. Cook:
Formalizing Randomized Matching Algorithms. - Peter Selinger
:
Finite dimensional Hilbert spaces are complete for dagger compact closed categories. - Yoriyuki Yamagata
:
Bounded Arithmetic in Free Logic. - Pierre Clairambault:
Isomorphisms of types in the presence of higher-order references (extended version). - Jan Krajícek:
Pseudo-finite hard instances for a student-teacher game with a Nisan-Wigderson generator. - Ben C. Moszkowski:
A Complete Axiom System for Propositional Interval Temporal Logic with Infinite Time. - Manfred Kufleitner
, Pascal Weil:
On logical hierarchies within FO2-definable languages. - Ugo Dal Lago
, Simone Martini
:
On Constructor Rewrite Systems and the Lambda Calculus. - Manuel Bodirsky, Martin Hils
, Barnaby Martin
:
On the Scope of the Universal-Algebraic Approach to Constraint Satisfaction. - Alexander Kurz
, Jirí Rosický:
Strongly Complete Logics for Coalgebras. - Xizhong Zheng, Robert Rettinger:
Point-Separable Classes of Simple Computable Planar Curves. - Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala:
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation. - Jörg Brauer, Andy King:
Transfer Function Synthesis without Quantifier Elimination. - Pawel Parys, Igor Walukiewicz:
Weak Alternating Timed Automata. - Mikolaj Bojanczyk, Howard Straubing, Igor Walukiewicz:
Wreath Products of Forest Algebras, with Applications to Tree Logics. - Mohamed Faouzi Atig:
Model-Checking of Ordered Multi-Pushdown Automata. - Diana Fischer, Lukasz Kaiser:
Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems. - Jacob Thamsborg, Lars Birkedal, Hongseok Yang:
Two for the Price of One: Lifting Separation Logic Assertions. - Alexander Heußner, Jérôme Leroux, Anca Muscholl, Grégoire Sutre:
Reachability Analysis of Communicating Pushdown Systems. - Michael Holtmann, Lukasz Kaiser, Wolfgang Thomas:
Degrees of Lookahead in Regular Infinite Games. - Wonchan Lee, Yungbum Jung, Bow-Yaw Wang, Kwangkeun Yi:
Predicate Generation for Learning-Based Quantifier-Free Loop Invariant Inference. - Mikolaj Bojanczyk, Luc Segoufin, Howard Straubing:
Piecewise testable tree languages. - Harro Wimmel, Karsten Wolf:
Applying CEGAR to the Petri Net State Equation. - Alain Finkel, Jean Goubault-Larrecq:
Forward Analysis for WSTS, Part II: Complete WSTS. - Thomas Martin Gawlitza, David Monniaux:
Invariant Generation through Strategy Iteration in Succinctly Represented Control Flow Graphs. - Predrag Janicic
:
Uniform Reduction to SAT. - Elmar Böhler, Nadia Creignou, Matthias Galota, Steffen Reith, Henning Schnoor, Heribert Vollmer:
Boolean Circuits as a Data Structure for Boolean Functions: Efficient Algorithms and Hard Problems.
Volume 8, Number 4, 2012
- Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, Kristian Støvring:
First steps in synthetic guarded domain theory: step-indexing in the topos of trees. - Jeff Egger, Rasmus Ejlers Møgelberg, Alex Simpson:
Linear-use CPS translations in the Enriched Effect Calculus. - Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, Giulio Manzonetto:
Full Abstraction for the Resource Lambda Calculus with Tests, through Taylor Expansion. - Marc Bezem, Keiko Nakata, Tarmo Uustalu
:
On streams that are finitely red. - Manuel Bodirsky
, Peter Jonsson, Timo von Oertzen:
Essential Convexity and Complexity of Semi-Algebraic Constraints. - Pierre-Malo Deniélou, Nobuko Yoshida
, Andi Bejleri, Raymond Hu
:
Parameterised Multiparty Session Types. - Fritz Müller:
On Berry's conjectures about the stable order in PCF. - Nathalie Bertrand
, Thierry Jéron
, Amélie Stainer, Moez Krichen:
Off-line test selection with test purposes for non-deterministic timed automata. - Philippe Darondeau, Stéphane Demri, Roland Meyer, Christophe Morvan:
Petri Net Reachability Graphs: Decidability Status of First Order Properties. - Lars Kuhtz, Bernd Finkbeiner:
Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds. - Ugo Dal Lago
, Marco Gaboardi:
Linear Dependent Types and Relative Completeness. - Amélie Gheerbrant, Balder ten Cate:
Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees. - Mario Bravetti, Cinzia Di Giusto, Jorge A. Pérez
, Gianluigi Zavattaro:
Adaptable processes. - Bob Coecke, Simon Perdrix:
Environment and classical channels in categorical quantum mechanics. - Robert Rettinger:
On computable approximations of Landau's constant. - André Platzer
:
The Structure of Differential Invariants and Differential Cut Elimination. - André Platzer
:
A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems. - Matteo Mio
:
Probabilistic modal μ-calculus with independent product. - Radu Mardare, Luca Cardelli
, Kim G. Larsen
:
Continuous Markovian Logics - Axiomatization and Quantified Metatheory.
![](https://dblp.dagstuhl.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.