Title :
Program derivation in PowerEpsilon
Author :
Zhu, Ming-Yuan ; Wang, Cheng-Wei
Author_Institution :
Beijing Inst. of Syst. Eng., China
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;
Conference_Titel :
Computer Software and Applications Conference, 1992. COMPSAC '92. Proceedings., Sixteenth Annual International
Conference_Location :
Chicago, IL
Print_ISBN :
0-8186-3000-0
DOI :
10.1109/CMPSAC.1992.217567
