LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
We present an extension of the πI-calculus with formal sums of terms. The study of the properties of this sum reveals that its neutral element can be used to make assumptions abo...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
Tait’s method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed λ-calculi. Histo...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
In higher-order process calculi the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators nec...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addi...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
This paper is an investigation of the matching problem for term equations s = t where s contains context variables, and both terms s and t are given using some kind of compressed ...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
We present a logic for algebraic effects, based on the algebraic representation of computational effects by operations and equations. We begin with the a-calculus, a minimal calcu...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
We show that reachability and termination for lossy channel systems is exactly at level Fωω in the Fast-Growing Hierarchy of recursive functions, the first level that dominates...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE
We investigate the notions of may- and mustapproximation in Erratic Idealized Algol (a nondeterministic extension of Idealized Algol), and give explicit characterizations of both ...
LICS
2008
IEEE
14 years 7 months ago
2008
IEEE