applicative bisimulation

Jawahar writes:
> I have been looking at applicative bisimulation recently. I was
> wondering if anyone has used it for justifying program transformations
> of interest to compiler writers. 

My recent Cambridge PhD thesis may be of interest.  In it I define a small
functional language and on it a typed form of applicative bisimulation.  I use
Howe's method from LICS'89 to show that applicative bisimulation is a
congruence, and then prove the validity of a collection of equational
properties of applicative bisimulation.  These equational properties could be
used to justify program transformations used in a compiler, say.

  author="Andrew D. Gordon",
  title="Functional Programming and Input/Output",
  school="University of Cambridge Computer Laboratory", month=Feb, year=1993,
  note="Available as Technical Report 285"}

I append the abstract at the end of this message.  I have a limited number of
copies of my thesis I can post out on request.  It's also available by
emailing tech-reports@cl.cam.ac.uk and asking for report 285.

Andrew Gordon.


A common attraction to functional programming is the ease with which proofs
can be given of program properties.  A common disappointment with functional
programming is the difficulty of expressing input/output (I/O) while at the
same time being able to verify programs.  In this dissertation we show how a
theory of functional programming can be smoothly extended to admit both an
operational semantics for functional I/O and verification of programs engaged
in I/O.

The first half develops the operational theory of a semantic metalanguage used
in the second half.  The metalanguage mu-nu-ML is a simply-typed
lambda-calculus with product, sum, function, lifted and recursive types.  We
study two senses of operational equivalence, one of which is a form of
Abramsky's applicative bisimulation, and show them to be congruences.  We
prove equational laws that are analogous to the axiomatic domain theory of LCF
and derive a co-induction principle.

The second half defines a small functional language, H, and shows how the
semantics of H can be extended to accommodate I/O.  H is a non-trivial
fragment of Haskell.  We give both operational and denotational semantics for
H.  The denotational semantics uses mu-nu-ML in a case study of Moggi's
proposal to use monads to parameterise semantic descriptions.  We define
operational and denotational equalities on H and show that denotational
implies operational equality.  We develop a theory of H based on equational
laws and a co-induction principle.

We study simplified forms of four widely-implemented I/O mechanisms: 
side-effecting, Landin-stream, synchronised-stream and continuation-passing 
I/O.  We give reasons why side-effecting I/O is unsuitable for lazy 
languages.  We extend the semantics of H to include the other three 
mechanisms and prove that the three are equivalent to each other in 
expressive power.

We investigate {\em monadic I/O}, a high-level model for functional I/O 
based on Wadler's suggestion that monads can express interaction with state 
in a functional language.  We show how a class of {\em monadic transition 
systems} can formalise the semantics of monadic I/O.  We rework 
strong and weak bisimulation from CCS, and hence verify a program 
transformation arising from an application of monadic I/O in medical