2010 Fiscal Year Final Research Report
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
|
| 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.
|
