1999 Fiscal Year Final Research Report Summary
Implementation of Constructive Programming Based on Classical Logic
| Project/Area Number |
10480061
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | KYOTO UNIVERSITY |
|---|
Principal Investigator |
SATO Masahiko Kyoto University, Graduate School of Informatics, Professor, 情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
TAKEUTI Izumi Kyoto University, Graduate School of Informatics, Research Associate, 情報学研究科, 助手 (20264583)
KAMEYAMA Yukiyoshi Kyoto University, Graduate School of Informatics, Associate Professor, 情報学研究科, 助教授 (10195000)
|
|---|
| Project Period (FY) |
1998 – 1999
|
| Keywords | Classical Logic / Constructive Programming / Type Theory |
|---|
| Research Abstract |
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'.
|
