Sciweavers

Share
CSL
2008
Springer
10 years 5 days ago
Type-Based Termination with Sized Products
Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursiv...
Gilles Barthe, Benjamin Grégoire, Colin Rib...
CSL
2008
Springer
10 years 5 days ago
Pure Pointer Programs with Iteration
not use pointer arithmetic. Such "pure pointer algorithms" thus are a useful abstraction for studying the nature of logspace-computation. In this paper we introduce a for...
Martin Hofmann, Ulrich Schöpp
CSL
2008
Springer
10 years 5 days ago
On Counting Generalized Colorings
Abstract. The notion of graph polynomials definable in Monadic Second Order Logic, MSOL, was introduced in [Mak04]. It was shown that the Tutte polynomial and its generalization, a...
Tomer Kotek, Johann A. Makowsky, Boris Zilber
CSL
2008
Springer
10 years 5 days ago
A Tight Karp-Lipton Collapse Result in Bounded Arithmetic
Olaf Beyersdorff, Sebastian Müller
CSL
2008
Springer
10 years 5 days ago
Syntactic Metatheory of Higher-Order Subtyping
Abstract. We present a new proof of decidability of higher-order subtyping in the presence of bounded quantification. The algorithm is formulated as a judgement which operates on b...
Andreas Abel, Dulma Rodriguez
CSL
2008
Springer
10 years 5 days ago
On the Almighty Wand
We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL) and its fragments. SL can specify pr...
Rémi Brochenin, Stéphane Demri, &Eac...
CSL
2008
Springer
10 years 5 days ago
An Infinite Automaton Characterization of Double Exponential Time
Infinite-state automata are a new invention: they are automata that have an infinite number of states represented by words, transitions defined using rewriting, and with sets of in...
Salvatore La Torre, P. Madhusudan, Gennaro Parlato
CSL
2008
Springer
10 years 5 days ago
A Characterization of Hypercoherent Semantic Correctness in Multiplicative Additive Linear Logic
We give a graph theoretical criterion on multiplicative additive linear logic (MALL) cut-free proof structures that exactly characterizes those whose interpretation is a hypercliqu...
Paolo Tranquilli
CSL
2008
Springer
10 years 5 days ago
Fractional Collections with Cardinality Bounds, and Mixed Linear Arithmetic with Stars
Abstract. We present decision procedures for logical constraints involving collections such as sets, multisets, and fuzzy sets. Element membership in our collections is given by ch...
Ruzica Piskac, Viktor Kuncak
CSL
2008
Springer
10 years 5 days ago
Recursion Schemata for NCk
Abstract. We give a recursion-theoretic characterization of the complexity classes NCk
Guillaume Bonfante, Reinhard Kahle, Jean-Yves Mari...
books