Program derivation in PowerEpsilon
M.-Y. Zhu, C.-W. Wang · 2003
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.>