|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/7292
| Title: | Formal Reasoning about Communication Systems I: Embedding ML into TypeTheory. |
| Authors: | Kreitz, Christoph |
| Keywords: | computer science
technical report |
| Issue Date: | Jul-1997 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR97-1637 |
| 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. |
| URI: | http://hdl.handle.net/1813/7292 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
