Sciweavers

Share
ASIAN
2006
Springer

On Completeness of Logical Relations for Monadic Types

9 years 1 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 to prove it. Whereas pre-logical relations are complete at all types, logical relations are only complete up to firstorder types. We propose a notion of contextual equivalence for Moggi's computational lambda calculus, and define pre-logical and logical relations for this calculus. Monads introduce new difficulties: in particular the usual proofs of completeness up to first-order types do not go through. We prove completeness up to first order for several of Moggi's monads. In the case of the non-determinism monad we obtain, as a corollary, completness of strong bisimulation w.r.t. contextual equivalence in lambda calculus with monadic non-determinism.
Slawomir Lasota, David Nowak, Yu Zhang
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ASIAN
Authors Slawomir Lasota, David Nowak, Yu Zhang
Comments (0)
books