Sciweavers

CSL
2008
Springer
13 years 11 months 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
13 years 11 months 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
13 years 11 months 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
13 years 11 months 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
13 years 11 months 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
13 years 11 months ago
Recursion Schemata for NCk
Abstract. We give a recursion-theoretic characterization of the complexity classes NCk
Guillaume Bonfante, Reinhard Kahle, Jean-Yves Mari...
CSL
2008
Springer
13 years 11 months ago
Proving Infinitude of Prime Numbers Using Binomial Coefficients
We study the problem of proving in weak theories of Bounded Arithmetic the theorem that there are arbitrarily large prime numbers. We show that the theorem can be proved by some &...
Phuong Nguyen
CSL
2008
Springer
13 years 11 months ago
Molecules as Automata
Luca Cardelli
CSL
2008
Springer
13 years 11 months ago
Quantified Positive Temporal Constraints
Abstract. A positive temporal template (or a positive temporal constraint language) is a relational structure whose relations can be defined over countable dense linear order witho...
Witold Charatonik, Michal Wrona
CSL
2008
Springer
13 years 11 months ago
Quantitative Languages
Quantitative generalizations of classical languages, which assign to each word a real number instead of a boolean value, have applications in modeling resource-constrained computat...
Krishnendu Chatterjee, Laurent Doyen, Thomas A. He...