[Prev][Next][Index][Thread]
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.
@PhDThesis{gordon93a,
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
electronics.