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...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 transformations.ALT is described formally,using a structural operational approach.展开更多
文摘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 transformations.ALT is described formally,using a structural operational approach.
