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: ¥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.

Research Products

• [Journal Article] Static Analysis for Multi-Staged Programs via Unstaging Translation (2011)
  • Author(s): Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta
  • Journal Title: Proceedings of 38th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2011) 81--92. Volume: 全1巻 Pages: 81-92
  • Peer Reviewed
• [Journal Article] Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems (2010)
  • Author(s): Koji Nakazawa, Makoto Tatsuta
  • Journal Title: Chicago Journal of Theoretical Computer Science Article 7
  • Peer Reviewed
• [Journal Article] Inhabitation of Polymorphic and Existential Types (2010)
  • Author(s): Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
  • Journal Title: Annals of Pure and Applied Logic 161(11) Pages: 1390-1399
  • Peer Reviewed
• [Journal Article] On Isomorphisms of Intersection Types (2010)
  • Author(s): Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta
  • Journal Title: ACM Transactions on Computational Logic 11(4) Article No 25
  • Peer Reviewed
• [Journal Article] Internal Normalization, Compilation and Decompilation for System F (2010)
  • Author(s): Stefano Berardi, Makoto Tatsuta
  • Journal Title: Lecture Notes in Computer Science(In : Proceedings of Tenth International Symposium on Functional and Logic Programming (FLOPS 2010)) 6009 Pages: 207-223
  • Peer Reviewed
• [Journal Article] Type Checking and Inference for Polymorphic and Existential Types in Multiple-Quantifier and Type-Free Systems (2010)
  • Author(s): Koji Nakazawa, Makoto Tatsuta
  • Journal Title: Chicago Journal of Theoretical Computer Science Volume: (Article 7)
  • Peer Reviewed
• [Journal Article] Internal Normalization, Compilation and Decompilation for System F (2010)
  • Author(s): Stefano Berardi, Makoto Tatsuta
  • Journal Title: Lecture Notes in Computer Science Volume: 6009 Pages: 207-223
  • Peer Reviewed
• [Journal Article] On Isomorphisms of Intersection Types (2010)
  • Author(s): Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makto Tatsut
  • Journal Title: ACM Transactions on Computational Logic (to appear)
  • Peer Reviewed
• [Journal Article] Inhabitation of Polymorphic and Existential Types (2010)
  • Author(s): Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
  • Journal Title: \em Annals of Pure and Applied Logic (to appear)
  • Peer Reviewed
• [Journal Article] On Isomorphisms of Intersection Types (2010)
  • Author(s): M.Dezani-Ciancaglini, R.Di Cosmo, E.Giovannetti, M.Tatsuta
  • Journal Title: ACM Transactions on Computational Logic (出版確定)
  • Peer Reviewed
• [Journal Article] Inhabitation of Polymorphic and Existential Types (2010)
  • Author(s): Makoto Tatsuta, Ken-etsu Fujita, Ryu Hasegawa, Hiroshi Nakano
  • Journal Title: Annals of Pure and Applied Logic (出版確定)
  • Peer Reviewed
• [Journal Article] Non-Commutative First-Order Sequent Calculus (2009)
  • Author(s): Makoto Tatsuta
  • Journal Title: Lecture Notes in Computer Science(In : Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009)) 5771 Pages: 470-484
  • Peer Reviewed
• [Journal Article] Proceedings of 18th EACSL Annual Conference on Computer Science Logic (CSL2009) (2009)
  • Author(s): Makoto Tatsuta, Non-Commutative First-Order Sequent Calculus
  • Journal Title: Lecture Notes in Computer Science 5771 Pages: 470-484
  • Peer Reviewed
• [Journal Article] Non-Commutative First-Order Sequent Calculus (2009)
  • Author(s): Makoto Tatsuta
  • Journal Title: Lecture Notes in Computer Science 5771 Pages: 470-484
  • Peer Reviewed
• [Journal Article] Strong normalization of classical natural deduction with disjunctions (2008)
  • Author(s): Koji Nakazawa, Makoto Tatsuta
  • Journal Title: Annals of Pure and Applied Logic 153(1-3) Pages: 21-37
  • Peer Reviewed
• [Journal Article] Types for Hereditary Permutators (2008)
  • Author(s): Makoto Tatsuta
  • Journal Title: In : Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS2008) Pages: 83-92
  • Peer Reviewed
• [Journal Article] Types for Hereditary Permutators (2008)
  • Author(s): Makoto Tatsuta
  • Journal Title: Proceedings of Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008) Pages: 83-92
  • Peer Reviewed
• [Journal Article] On Isomorphisms of Intersection Types (2008)
  • Author(s): M. Dezani-Ciancaglini, R. Di Cosmo, E. Giovannetti., M. Tatsuta
  • Journal Title: Leeture Notes in Computer Science 5213 Pages: 461-477
  • Peer Reviewed
• [Journal Article] Simple saturated sets for disjunction and second-order existential quantification (2007)
  • Author(s): M.Tatsuta
  • Journal Title: Lecture Notes in Computer Science(In : Proceedings of 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007)) 4583 Pages: 366-380
  • Peer Reviewed
• [Journal Article] Simple saturated sets for disjunction and second-order existential quantification (2007)
  • Author(s): M. Tatsuta
  • Journal Title: Lecture Notes in Computer Science 4583 Pages: 366-380
  • Peer Reviewed
• [Journal Article] The maximum length of mu-reduction in lambda mu-alculus (2007)
  • Author(s): Makoto Tatsuta
  • Journal Title: Lecture Notes in Computer Science 4533 Pages: 359-373
  • Peer Reviewed
• [Presentation] 遺伝的置換子の型とTLCA未解決問題20番 (2008)
  • Author(s): 龍田真
  • Organizer: 日本ソフトウェア科学会第25回大会(査読無)