1999 Fiscal Year Final Research Report Summary
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
|
| 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.
|
Research Products
(15 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
「研究成果報告書概要(欧文)」より
-
-
-
-
