Technical Report

TITLE:

Verifying Properties of Module Construction in Type Theory

DATE:

August 1993

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:

type theory, program verification, specification-in-the-large

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 to laws about deliverables which can be proved correct in 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, 03.01.1994