This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
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...
The study of constraint satisfaction problems definable in various fragments of Datalog has recently gained considerable importance. We consider constraint satisfaction problems ...
This paper presents a new bisimulation theory for parametric polymorphism which enables straightforward coinductive proofs of program equivalences involving existential types. The...
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...
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...
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...
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...
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...