论文部分内容阅读
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 descriptionof 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 reasoningand 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 to 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.