A Type-Theoretic Approach to Program Development

A paradigm of program development using type theories is given after analyzing some typical exam- ples.In order to carry this approach forward,a language ALT is designed.It is a linguistic description of a generalized higher order typed lambda calculus with Π,∑ types and Π,∑ kinds (supertypes). Four examples are given to show how ALT can be used to implement many concepts of software engi- neering and artificial intelligence.They are intuitionistic logic,Peano arithmetic,approximate reasoning and program tr…