Formal Reasoning about Communication Systems I: Embedding ML into Type Theory.
Christoph Kreitz.
Technical Report TR 97-1637, Cornell University, Ithaca, NY, June 1997.
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.

			Back to overview of papers
Bibtex Entry
	@TechReport{tr:Kreitz97a, author = "Christoph Kreitz", title = "Formal Reasoning about Communication Systems {I}: Embedding {ML} into Type Theory", institution = "Cornell University. Department of Computer Science", year = 1997, number = "TR97-1637", month = "June" }