Sciweavers

MSCS
2008
97views more  MSCS 2008»
13 years 4 months ago
Logical relations for monadic types
Abstract. Software security can be ensured by specifying and verifying security properties of software using formal methods with strong theoretical bases. In particular, programs c...
Jean Goubault-Larrecq, Slawomir Lasota, David Nowa...
CONCUR
2008
Springer
13 years 6 months ago
Deriving Structural Labelled Transitions for Mobile Ambients
We present a new labelled transition system (lts) for the ambient calculus on which ordinary bisimilarity coincides with contextual equivalence. The key feature of this lts is that...
Julian Rathke, Pawel Sobocinski
ESOP
2006
Springer
13 years 8 months ago
Bisimulations for Untyped Imperative Objects
We present a sound and complete method for reasoning about contextual equivalence in the untyped, imperative object calculus of Abadi and Cardelli [1]. Our method is based on bisim...
Vasileios Koutavas, Mitchell Wand
ESOP
2006
Springer
13 years 8 months ago
Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types
We present a sound and complete proof technique, based on syntactic logical relations, for showing contextual equivalence of expressions in a -calculus with recursive types and imp...
Amal J. Ahmed
ASIAN
2006
Springer
140views Algorithms» more  ASIAN 2006»
13 years 8 months ago
On Completeness of Logical Relations for Monadic Types
Interesting properties of programs can be expressed using contextual equivalence. The latter is difficult to prove directly, hence (pre-)logical relations are often used as a tool ...
Slawomir Lasota, David Nowak, Yu Zhang
AOSD
2007
ACM
13 years 8 months ago
Open bisimulation for aspects
We define and study bisimulation for proving contextual equivalence in an aspect extension of the untyped lambda-calculus. To our knowledge, this is the first study of coinductive...
Radha Jagadeesan, Corin Pitcher, James Riely
AC
2000
Springer
13 years 8 months ago
Operational Semantics and Program Equivalence
This tutorial paper discusses a particular style of operational semantics that enables one to give a ‘syntax-directed’ inductive definition of termination which is very useful...
Andrew M. Pitts
CSL
2004
Springer
13 years 9 months ago
Complete Lax Logical Relations for Cryptographic Lambda-Calculi
Abstract. Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equiva...
Jean Goubault-Larrecq, Slawomir Lasota, David Nowa...
FOSSACS
2005
Springer
13 years 10 months ago
Third-Order Idealized Algol with Iteration Is Decidable
The problems of contextual equivalence and approximation are studied for the third-order fragment of Idealized Algol with iteration (IA∗ 3). They are approached via a combination...
Andrzej S. Murawski, Igor Walukiewicz
LICS
2009
IEEE
13 years 11 months ago
Trace Semantics is Fully Abstract
mantics Is Fully Abstract∗ Sumit Nain and Moshe Y. Vardi Rice University, Department of Computer Science Houston, TX 77005-1892, USA The discussion in the computer-science liter...
Sumit Nain, Moshe Y. Vardi