Computation-Theoretic Approach to Types and Proofs
| Project/Area Number |
09640248
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
General mathematics (including Probability theory/Statistical mathematics)
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
TAKAHASHI-HORAI Masako Tokyo Institute of Technology, Mathematical and Computing Sciences, Professor, 大学院・情報理工学研究科, 教授 (00015588)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
寶来 正子 東京工業大学, 大学院・情報理工学研究科, 教授 (00015588)
|
|---|
| Project Period (FY) |
1997 – 1999
|
| Project Status |
Completed (Fiscal Year 1999)
|
| Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 1999: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1998: ¥500,000 (Direct Cost: ¥500,000)
Fiscal Year 1997: ¥700,000 (Direct Cost: ¥700,000)
|
|---|
| Keywords | computability / higher-order types / intuitionistic higher-order logic / Curry-Howard isomorphism / λ-calculus / term algebra / 単純型つきラムダ計算 / 自由代数 / 項代数 / 語に対する帰納的関数 / 型理論 / 証明論 / 高階理論 / 原始帰納法 / 単純型理論 / 単一化問題 / マッチング問題 / 帰納的関数 |
|---|
| Research Abstract |
It is shown that the Curry-Howard isomorphism between higher-order intuitionistic logic and Calculus of Constructions can be better formulated when a modified version of higher-order type theory λPREDω is introduced. Also studied are the lambda-representability of functions over free structures with respect to the simple type system, as well as the notion of recursive functions over free-structures.
|
Report
(4 results)
Research Products
(20 results)
-
-
-
-
-
-
-
-
-
-
-
[Publications] M. Dezani-Ciancaglini, E. Giovannetti, and U. de'Liguoro: "Intesection types,λ-models, and Bo hm treees"Theories of Types and Proofs, (Masako Takahashi, M.Dezani-Ciancaglini, and M. Okada, eds.), MSJ-Memoirs, Vol. 2, pp 45-97 (Mathematical Society of Japan). (1998)
Description
「研究成果報告書概要(欧文)」より
Related Report
-
-
-
-
-
-
-
-
-
