


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.

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.