  MiniJava is a subset of the object-oriented programming language Java.
Standard ML is the canonical representative of the ML family of functional
programming languages, which includes F# and OCaml. Different program analysis
and verification tools and techniques have been developed for both Java-like
and ML-like languages. Naturally, the tools developed for a particular language
emphasise accurate treatment of language features commonly used in that
language. In Java, this means objects with mutable properties and dynamic
method dispatch. In ML, this means higher order functions and algebraic
datatypes with pattern matching.
  We propose to translate programs from one language into the other and use the
target language's tools for analysis and verification. By doing so, we hope to
identify areas for improvement in the target language's tools and suggest
techniques, perhaps as used in the source language's tools, that may guide
their improvement. More generally, we hope to develop tools for reasoning about
programs that are more resilient to changes in the style of code and
representation of data. We begin our programme by outlining a translation from
MiniJava to ML that uses only the core features of ML; in particular, it avoids
the use of ML's mutable references.
