Program derivation in PowerEpsilon

Author

Zhu, Ming-Yuan ; Wang, Cheng-Wei

Author_Institution

Beijing Inst. of Syst. Eng., China

fYear

1992

fDate

21-25 Sep 1992

Firstpage

206

Lastpage

211

Abstract

The authors present a proof development system called PowerEpsilon, based on a constructive type theory which can be used as a formal program development system for deriving a program from a specification. PowerEpsilon is a polymorphic language based on Martin-Lof´s type theory and the calculus of constructions. In PowerEpsilon, the concept of limit of type universe hierarchies and a scheme for inductive define types are introduced. The system can be used as both a programming language with a very rich set of data structures and a metalanguage for formalizing constructive mathematics. The system has been implemented. A programming exercise is given to show how the system works

Keywords

data structures; program verification; theorem proving; type theory; Martin-Lof´s type theory; PowerEpsilon; calculus of constructions; constructive type theory; data structures; formal program development system; inductive define types; metalanguage; polymorphic language; proof development system; type universe hierarchies; Calculus; Computer languages; Data structures; Logic programming; Mathematical programming; Mathematics; Power engineering and energy; Read only memory; Systems engineering and theory; Writing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Software and Applications Conference, 1992. COMPSAC '92. Proceedings., Sixteenth Annual International

Conference_Location

Chicago, IL

Print_ISBN

0-8186-3000-0

Type

conf

DOI

10.1109/CMPSAC.1992.217567

Filename

217567