2003 Fiscal Year Final Research Report Summary
Calculus and Logic of Delimited Continuations
| Project/Area Number |
13680411
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | University of Tsukuba |
|---|
Principal Investigator |
KAMEYAMA Yukiyoshi University of Tsukuba, Institute of Information Sciences and Electronics, Associate Professor, 電子・情報工学系, 助教授 (10195000)
|
|---|
| Project Period (FY) |
2001 – 2003
|
| Keywords | Control Operators / Software Verification / Delimited Continuations / Axiomatization / Functional Programming / Meta-variables / Contexts |
|---|
| Research Abstract |
The main purpose of this three-year project is to study the control operators in functional programming from 'the viewpoint of type theory and logic, and then develop a theory on the control operators which enables one to write correct programs with control operators. In this project we focus on the control operators for so called delimited continuations. Our research results can be summarized as follows. (1) We have succesfully given a sound and complete axiomatization for "shift" and "reset", the most well known, and widely used control operators for delimited continuations, (2) We have shown that the axioms for shift and reset are a conservative extension over those for callcc, and that the added axioms are not redundant with one exception. These two results enable one to reason about shift and reset, thus we can verify the correctness of programs with shift and reset. (3) We have also extended the above results to the higher-level shift and reset, by which we can combine various uses of shift and reset. The resulting axioms are surprisingly simple and thus can be used to software verification, too
Since control operators manipulate mete-level control structures of programs, we }lave also study the calculi and logic of mete-variables and computational contexts, and obtained a sufficiently simple, but powerful calculi based on the simply typed lambda calculi. A characteristic feature of our calculus is that it has the textual substitution as well as the ordinary capture-avoiding substitution
|
