Technical Report 92-03

TITLE:

Lifting the laws of module algebra to deliverables

DATE:

August 1992

AUTHORS:

Bernhard Reus <reus@informatik.uni-muenchen.de>

Thomas Streicher <streicher@informatik.uni-muenchen.de>

Institut für Informatik

Universität München

Leopoldstr. 11B

D-80802 München (Germany)

KEYWORDS:

Modular Specifications, Type Theory, ECC, Program Verification

ABSTRACT:

This paper presents a comparison between algebraic specifications-in-the-large and a type theoretical formulation of modular specifications, called deliverables. It is shown that the laws of module algebra can be translated into the deliverables approach and can be proved there in the language of type theory. The adequacy of the Extended Calculus of Constructions as a possible implementation of type theory is discussed and it is explained how the reformulation of the laws is influenced by this choice.

Bei Problemen, Vorschlägen schicken Sie bitte eine eMail an wwwmaster@informatik.uni-muenchen.de .

Robert Stabl, 17.01.1994