Type Theory of Commutative Reductions
| Project/Area Number |
19540156
|
|---|
| 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 | National Institute of Informatics |
|---|
Principal Investigator |
TATSUTA Makoto National Institute of Informatics, 情報学プリンシプル研究系, 教授 (80216994)
|
|---|
| Project Period (FY) |
2007 – 2010
|
| Project Status |
Completed (Fiscal Year 2010)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2008: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2007: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| Keywords | プログラム理論 / 置換簡約 / 型理論 |
|---|
| Research Abstract |
We developed logical systems and type systems extended with commutative reductions and their related notions, and showed their fundamental properties. In particular, we proved characterization of isomorphisms of intersection types, properties of non-commutative first-order sequent calculus, properties of type inference for type systems with multiple-quantifier, properties of an internal decompiler-normalizer for type system F, and characterization of hereditary permutators by type systems.
|
Report
(6 results)
Research Products
(22 results)
