Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
LICS
2008
IEEE
11 years 11 months ago
On the Axiomatizability of Impossible Futures: Preorder versus Equivalence
We investigate the (in)equational theory of impossible futures semantics over the process algebra BCCSP. We prove that no finite, sound axiomatization for BCCSP modulo impossible...
Taolue Chen, Wan Fokkink
LICS
2008
IEEE
11 years 11 months ago
Caterpillar Duality for Constraint Satisfaction Problems
The study of constraint satisfaction problems definable in various fragments of Datalog has recently gained considerable importance. We consider constraint satisfaction problems ...
Catarina Carvalho, Víctor Dalmau, Andrei A....
LICS
2008
IEEE
11 years 11 months ago
Typed Normal Form Bisimulation for Parametric Polymorphism
This paper presents a new bisimulation theory for parametric polymorphism which enables straightforward coinductive proofs of program equivalences involving existential types. The...
Søren B. Lassen, Paul Blain Levy
LICS
2008
IEEE
11 years 11 months ago
Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule
Separation logic involves two dual forms of modularity: local reasoning makes part of the store invisible within a static scope, whereas hiding local state makes part of the store...
François Pottier
LICS
2008
IEEE
11 years 11 months ago
Cut Elimination for Monomial MALL Proof Nets
We present a syntax for MALL (multiplicative additive linear logic without units) proof nets which refines Girard’s one. It is also based on the use of monomial weights for ide...
Olivier Laurent, Roberto Maieli
LICS
2008
IEEE
11 years 11 months ago
Winning Regions of Higher-Order Pushdown Games
In this paper we consider parity games defined by higher-order pushdown automata. These automata generalise pushdown automata by the use of higher-order stacks, which are nested ...
Arnaud Carayol, Matthew Hague, Antoine Meyer, C.-H...
LICS
2008
IEEE
11 years 11 months ago
Mechanizing the Metatheory of LF
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as p...
Christian Urban, James Cheney, Stefan Berghofer
LICS
2008
IEEE
11 years 11 months ago
Correctness of Multiplicative Additive Proof Structures is NL-Complete
We revisit the correctness criterion for the multiplicative additive fragment of linear logic. We prove that deciding the correctness of corresponding proof structures is NLcomple...
Paulin Jacobé de Naurois, Virgile Mogbil
books