| Project/Area Number |
13480082
|
|---|
| 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) |
NAKAZAWA Koji Kyoto University, Graduate School of Informatics, Research Associate, 情報学研究科, 助手 (80362581)
IGARASHI Atsushi Kyoto University, Graduate School of Informatics, Lecturer, 情報学研究科, 講師 (40323456)
竹内 泉 東邦大学, 理学部, 講師 (20264583)
亀山 幸義 筑波大学, 電子・情報工学系, 助教授 (10195000)
|
|---|
| Project Period (FY) |
2001 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥7,300,000 (Direct Cost: ¥7,300,000)
Fiscal Year 2003: ¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 2002: ¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 2001: ¥3,000,000 (Direct Cost: ¥3,000,000)
|
|---|
| Keywords | Object Language / Meta Language / Syntactic Object / Meta Variable / Variable Collision / Context / 環境 / 合流性 / 強正規化性 / 型理論 / 計算体系 |
|---|
| Research Abstract |
The aim of this research project was to construct calculi containing environments and contexts as first-class objects, and to study these calculi from a logical point of view. The main results are summarized as follows.
・Calculi of first-class environments and contexts
We have developed calculus systems of environments and contents. Though environments and contexts are notions outside a formal system, we can handle environments and contexts as first-class objects in these systems. We have constructed the systems as formal type systems, and proved subject reduction, confluence, strong normalizability and conservativity of the systems.
・Calculi of meta-variables
We have developed calculus systems of meta-variables. In these systems, each variable is given a level, which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. By this notion of level, we can treat textual substitution in these systems, and express insertion of programs into holes of contexts, which may generate new variable binding. We have shown that these systems also can express composition of contexts, which the systems above cannot. We have also proved subject reduction, confluence and strong normalizability. of the systems of meta-variables.
|
