*Abstract:*

Pure functional languages are expressive tools for writing modular and reliable code. State in programming languages is a useful tool for programming dynamic systems. However, their combination yields programming languages that are difficult to model and to reason about.

There have been ongoing attempts to find subsets of the whole
languages which have good properties; in particular subsets where
the programs are more modular and the side effects are controlled.
The existing studies are: interference control, typing with
side-effects information, and linear logic based languages. This
thesis presents a new classification for a paradigm called constant
program throughout a computational invariant. A program is called
constant throughout an invariant *R* if its input-output
behaviour is constant over any variations of state that satisfy the
invariant *R*. Hence such a program behaves in an applicative
way when it is executed in a context that satisfies the invariant
*R*.

The language of discussion is a pure ML fragment augmented with
`ref`, `:=`, and `!`. Programs with side
effects are modelled in terms of sets, functions, and the side
effect monad. Computational invariants are modelled in terms of
transition systems. The notion of being constant throughout an
invariant requires the notion of indistinguishability throughout an
invariant and we define the latter using logical relation
technique. We give two definitions of each of them: the first one
can be used for reasoning about programs with at stores adequately.
The second one is more sensitive to the behaviour of ref and gives
a better account of constant programs with dynamic allocations.

Our results are: indistinguishability throughout an invariant
*R* is an equivalence relation over elements that are constant
throughout *R*, and the notion of being constant throughout an
invariant is preserved under function application. On the practical
side we present some substantial ML examples which use references
and side effects but externally behave in a constant way, together
with the proofs that they are classified as being constant. These
are evidences that our notions are useful concepts in the practise
of writing modular programs.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file