Formal Reasoning about Communication Systems I: Embedding ML into TypeTheory.

Abstract

We present a semantically correct embedding of a subset of the Ocaml programming language into the type theory of NuPRL. The subset is that needed to build the Ensemble group communication system. We describe the essential methodologies for representing language constructs by type-theoretical expressions. Tactics representing derived inference rules and a programming logic for these constructs will be discussed as well as algorithms for translating an Ocaml-program into NuPRL-objects and vice versa. The formal representations and the translation algorithms will serve as the foundation for the development of automated reasoning tools for the verification and optimization of a group communication systems.