Implementation of Constructive Programming Based on Classical Logic

点击翻译按钮获取中文摘要

For the purpose of developing constructive programming based on classical logic, this research extended the functional programming language PAィイD2ctィエD2, which has catch/throw mechanism as exception processing, and made the following results.The head investigator Sato studied the notion of binding variables, which is the important notion for predicate logic and functional programming language. As the result of this study, he proposed a calculus which do not have renaming of bind variables. This result was presented in the 4th international conference on Typed Lambda Calculi and Application in 1999, at L'Aquia, Italy.The investigator Kameyama studied exception processing and partial contiunation in functional programming languages based on classical logic, and classified typical calculi with exception processing and partial continuation. He solved the problems of confluency and termination of such calculi. This results are to be published in 'Theoretical Computer Science'.The investigator Takeuti studied the relation between parametric polymorphism and mathematical induction. Mathematical induction is an important method to prove theorems in systems of constructive programming. He showed that system of parametricity derives various forms of mathematical induction. This result was published in 'Fundamenta Informaticae'.