List of Publications

Japanese version

[ 2012 | 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 and before ]

Notice: The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

2012

2011

• João Filipe Belo, Michael Greenberg, Atsushi Igarashi, and Benjamin C. Pierce. Polymorphic contracts. In Proceedings of the European Symposium on Programming (ESOP2011), volume 6602 of Lecture Notes in Computer Science, pages 18–37, Saarbrücken, Germany, March 2011. Springer-Verlag.
• Ryota Fukuda, Kohei Suenaga, and Atsushi Igarashi. Type-based analysis of safe resource deallocation for shared-memory concurrency. Poster session at APLAS2011, December 2011.
• Robert Hirschfeld, Atsushi Igarashi, and Hidehiko Masuhara. ContextFJ: A minimal core calculus for context-oriented programming. In Proceedings of the International Workshop on Foundations of Aspect-Oriented Languages (FOAL2011), Pernambuco, Brazil, March 2011. (PDF)
• Atsushi Igarashi. A featherweight approach to FOOL. In Proceedings of the 25th European Conference on Object-Oriented Programming (ECOOP2011), volume 6813 of Lecture Notes in Computer Science, page 433, Lancaster, UK, June 2011. Springer-Verlag. Keynote talk abstract.
• Lintaro Ina and Atsushi Igarashi. Gradual typing for generics. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2011), pages 609–624, Portland, OR, October 2011. (PDF)
• Naoki Kobayashi and Atsushi Igarashi. Model checking Featherweight Java, December 2011. Submitted for publication.
• Kensuke Kojima and Atsushi Igarashi. Constructive linear-time temporal logic: Proof systems and Kripke semantics. Information and Computation, 209(12):1491–1503, 2011. A preliminary version appeared in Proceedings of the Intutionistic Modal Logics and Applications Workshop (IMLA'08). (PDF)
• Chieri Saito and Atsushi Igarashi. Matching MyType with subtyping. Science of Computer Programming, 2011. Accepted for publication. A preliminary version under the title ``Matching ThisType with Subtyping'' appeared in Proceedings of the 24th Annual ACM Symposium on Applied Computing (SAC2009), pages 1851-1858, March 2009. (PDF)
• Kohei Suenaga and Atsushi Igarashi. Type-based safe resource deallocation for shared-memory concurrency, 2011. Submitted for publication.
• ¸Þ½½Íò ½ß. ¥×¥í¥°¥é¥ß¥ó¥°¸À¸ì¤Î´ðÁóµÇ°. Number 24 in ¥é¥¤¥Ö¥é¥ê¾ðÊó³Ø¥³¥¢¡¦¥Æ¥­¥¹¥È. ¥µ¥¤¥¨¥ó¥¹¼Ò, July 2011.
• ÂçΤ ÍÛ°ì, ¸Þ½½Íò ½ß, Ãæß· ¹ª¼¤. Îã³°µ¡¹½¤ò»ý¤Ä·¿ÉÕ¥é¥à¥À·×»»¤Ë¤ª¤±¤ë¥Ñ¥é¥á¥È¥ê¥·¥Æ¥£, January 2011. Submitted for publication.

2010

• Shigeru Chiba, Atsushi Igarashi, and Salikh Zakirov. Mostly modular composition of crosscutting structures by contextual predicate dispatch. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2010), pages 539–554, Reno/Tahoe, NV, October 2010. (PDF)
• Lintaro Ina and Atsushi Igarashi. Gradual typing for generics. Poster session at APLAS2010, December 2010.
• Yuki Kato and Koji Nakazawa. Type checking and inference are equivalent in lambda calculi with existential types. In Santiago Escobar, editor, 18th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2009), Revised Selected Papers, Brasilia, Brazil, volume 5979 of Lecture Notes in Computer Science, pages 96–110. Springer-Verlag, April 2010. (PDF)
• Hidehiko Masuhara, Atsushi Igarashi, and Manabu Toyama. Type relaxed weaving. In Proceedings of the 9th International Conference on Aspect-Oriented Software Development (AOSD'10), pages 121–132, Rennes and Saint Malo, France, March 2010. (PDF)
• Hidehiko Masuhara, Atsushi Igarashi, and Manabu Toyama. Type relaxed weaving, August 2010. A revied and extended version of [Masuhara et al., 2010a].
• Koji Nakazawa and Makoto Tatsuta. Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems. Chicago Journal of Theoretical Computer Science, Special Issue: Selected papers from 2009 Computing: The Australasian Theory Symposium (CATS 2009), Article 7, 2010. (Jounal version of the precedent conference paper: Type Checking and Inference for Polymorphic and Existential Types, CATS 2009, Wellington, New Zealand, January, 2009.). (PDF)
• Takeshi Tsukada and Atsushi Igarashi. A logical foundation for environment classifiers. Logical Methods in Computer Science, 6(4:8):1–43, December 2010. A preliminary version appeared in Proceedings of the 9th International Conference on Typed Lambda-Calculi and Applications (TLCA'09), volume 5608 of Springer LNCS, pages 341-355, June, 2009. (PDF) (doi:10.2168/LMCS-6(4:8)2010)

2009

• Lintaro Ina and Atsushi Igarashi. Towards gradual typing for generics. In Proceedings of the 1st International Workshop on Script to Program Evolution (STOP2009), Genova, Italy, July 2009. Available also in the ACM Digital Library. (PDF)
• Chieri Saito and Atsushi Igarashi. Matching ThisType to subtyping. In Proceedings of the 24th Annual ACM Symposium on Applied Computing (SAC2009), pages 1851–1858, Honolulu, HI, March 2009. (PDF)
• Chieri Saito and Atsushi Igarashi. Self type constructors. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA2009), pages 263–282, Orlando, FL, October 2009. (PDF)
• Takeshi Tsukada and Atsushi Igarashi. A logical foundation for environment classifiers. In Pierre-Louis Curien, editor, Proceedings of the 9th International Conference on Typed Lambda-Calculi and Applications (TLCA'09), volume 5608 of Lecture Notes in Computer Science, pages 341–355, Brasília, Brazil, July 2009. Springer-Verlag. (PDF)

2008

• Elvira Albert, Anindya Banerjee, Sophia Drossopoulou, Marieke Huisman, Atsushi Igarashi, Gary T. Leavens, Peter Müller, and Tobias Wrigstad. Formal techniques for Java-like languages. In ECOOP Workshops, volume 5475 of Lecture Notes in Computer Science, pages 70–76, Paphos, Cyprus, July 2008. Springer-Verlag.
• Kensuke Kojima and Atsushi Igarashi. On constructive linear-time temporal logic. In Proceedings of the Intutionistic Modal Logics and Applications Workshop (IMLA'08), Pittsburgh, PA, June 2008. (PDF)
• Koji Nakazawa and Makoto Tatsuta. Strong normalization of classical natural deduction with disjunctions. Annals of Pure and Applied Logic, 153:21–37, April 2008. (PDF)
• Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, and Hiroshi Nakano. Undecidability of type-checking in domain-free typed lambda-calculi with existence. In Michael Kaminski and Simone Martini, editors, Computer Science Logic (CSL 2008), volume 5213 of Lecture Notes in Computer Science, pages 478–492. Springer-Verlag, 2008. (PDF)
• Chieri Saito and Atsushi Igarashi. The essence of lightweight family polymorphism. Journal of Object Technology, 7(5):67–99, June 2008. Special Issue: Workshop on FTfJP 2007. (PDF)
• Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Lightweight family polymorphism. Journal of Functional Programming, 18(3):285–331, 2008. A preliminary summary appeared in Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS 2005), Springer LNCS vol. 3780, pages 161–177, November, 2005. (PDF) (doi:10.1017/S0956796807006405)
• Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, and Atsushi Igarashi. Calculi of meta-variables. Frontiers of Computer Science in China, 2(1):12–21, 2008. Special issue on foundations of software.
• Naokata Shikuma and Atsushi Igarashi. Proving noninterference by a fully complete translation to the simply typed λ-calculus. Logical Methods in Computer Science, 4(3:10):1–31, September 2008. An extended abstract appeared in Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), volume 4435 of Springer LNCS, pages 302-316, December, 2006. (PDF) (doi:10.2168/LMCS-4(3:10)2008)

2007

• Atsushi Igarashi and Masashi Iwaki. Deriving compilers and virtual machines for a multi-level language. In Zhong Shao, editor, Proceedings of the 5th Asian Symposium on Programming Languages and Systems (APLAS 2007), volume 4807 of Lecture Notes in Computer Science, pages 206–221, Singapore, November/December 2007. Springer-Verlag. (PDF)
• Atsushi Igarashi and Hideshi Nagira. Union types for object-oriented programming. Journal of Object Technology, 6(2):47–68, February 2007. Special Issue OOPS track at SAC 2006. Available through http://www.jot.fm/issues/issue_2007_02/article3. (PDF)
• Atsushi Igarashi and Mirko Viroli. Variant path types for scalable extensibility. In Proceedings of the International Workshop on Foundations and Developments of Object-Oriented Languages (FOOL/WOOD 2007), pages 38–49, Nice, France, January 2007. Available through http://www.cs.hmc.edu/~stone/FOOL/FOOLWOOD07/.
• Atsushi Igarashi and Mirko Viroli. Variant path types for scalable extensibility. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2007), pages 113–132, Montreal, QC, October 2007. (PDF)
• Koji Nakazawa. An isomorphism between cut-elimination procedure and proof reduction. In Simona Ronchi Della Rocca, editor, Typed Lambda Calculi and Applications (TLCA2007), volume 4583 of Lecture Notes in Computer Science, pages 336–350. Springer-Verlag, 2007. (PDF)
• Chieri Saito and Atsushi Igarashi. The essence of lightweight family polymorphism. In Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), pages 27–41, Berlin, Germany, July 2007. Available through http://cs.nju.edu.cn/boyland/ftjp/. (PDF)

2006

• Davide Ancona, Sophia Drossopoulou, Atsushi Igarashi, Gary T. Leavens, Arnd Poetzsch-Heffter, and Elena Zucca. Formal techniques for Java-like languages. In ECOOP Workshops, volume 4379 of Lecture Notes in Computer Science, pages 53–58, Nantes, France, July 2006. Springer-Verlag.
• Atsushi Igarashi and Hideshi Nagira. Union types for object-oriented programming. In Proceedings of the 21st Annual ACM Symposium on Applied Computing (SAC2006), pages 1435–1441, Dijon, France, April 2006.
• Atsushi Igarashi and Mirko Viroli. Variant parametric types: A flexible subtyping scheme for generics. ACM Transactions on Programming Languages and Systems, 28(5):795–847, September 2006. A preliminary version appeared under the title ``On Variance-Based Subtyping for Parametric Types'' in Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP2002), Springer LNCS vol. 2374, pages 441–469, June 2002. (PDF)
• Satoshi Ikeda and Koji Nakazawa. Strong normalization proofs by CPS-translations. Information Processing Letters, 99(4):163–170, August 2006. (PDF)
• Futoshi Iwama, Atsushi Igarashi, and Naoki Kobayashi. Resource usage analysis for a functional language with exceptions. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'06), pages 38–47, Charleston, SC, January 2006. (PDF)
• Naokata Shikuma and Atsushi Igarashi. Proving noninterference by a fully complete translation to the simply typed λ-calculus. In Proceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), volume 4435 of Lecture Notes in Computer Science, pages 302–316, Tokyo, Japan, December 2006. Springer-Verlag. (PDF)
• Yoshihiro Yuse and Atsushi Igarashi. A modal type system for multi-level generating extensions with persistent code. In Proceedings of the 8th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'06), pages 201–212, Venice, Italy, July 2006. (PDF)

2005

• Atsushi Igarashi and Naoki Kobayashi. Resource usage analysis. ACM Transactions on Programming Languages and Systems, 27(2):264–313, March 2005. An extended abstract appeared in Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL2002), ACM SIGPLAN Notices, volume 37, number 1, pages 331–342, January 2002. (PDF)
• Atsushi Igarashi, Chieri Saito, and Mirko Viroli. Lightweight family polymorphism. In Kwangkeun Yi, editor, Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS2005), volume 3780 of Lecture Notes in Computer Science, pages 161–177, Tsukuba, Japan, November 2005. Springer-Verlag. (PDF)

2004

• Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. Theoretical Computer Science, 311(1-3):121–163, January 2004. An extended abstract appeared in Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL2001), ACM SIGPLAN Notices, volume 36, number 3, pages 128–141, January 2001. (PDF)
• Kenji Miyamoto and Atsushi Igarashi. A modal foundation for secure information flow. In Andrei Sabelfeld, editor, Proceedings of the Workshop on Foundations of Computer Security (FCS'04), number 31 in Turku Centre for Computer Science General Publication, pages 187–203, Turku, Finland, July 2004. (PDF)
• Masahiko Sato. A simple theory of expressions, judgments and derivations. In Proceedings of the 9th Asian Computing Science Conference (ASIAN'04), volume 3321 of Lecture Notes in Computer Science, pages 437–451, Chiang Mai, Thailand, December 2004. Springer-Verlag.

2003

• Koji Nakazawa and Makoto Tatsuta. Strong normalization proof with CPS-translation for second order classical natural deduction. The Journal of Symbolic Logic, 68(3):851–859, September 2003. (PDF) Corrigendum of this article is available in, The Journal of Symbolic Logic, 68(4):1415–1416, December 2003. (PDF).
• Koji Nakazawa. Confluency and strong normalizability of call-by-value λμ-calculus. Theoretical Computer Science, 290:429–463, January 2003. (PDF)
• Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama, and Atsushi Igarashi. Calculi of metavariables. In Matthias Baaz and Johann M. Makowsky, editors, Proceedings of the the Annual Computer Science Logic (CSL'03) and 8th Kurt Gödel Colloquium, volume 2803 of Lecture Notes in Computer Science, pages 484–497, Vienna, Austria, August 2003. Springer-Verlag.

2002

• Atsushi Igarashi and Naoki Kobayashi. Resource usage analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'02), pages 331–342, Portland, OR, January 2002. (PDF)
• Atsushi Igarashi and Benjamin C. Pierce. Foundations for virtual types. Information and Computation, 175(1):34–49, May 2002. A special issue with papers from the 6th International Workshop on Foundations of Object-Oriented Languages (FOOL6). An earlier version appeared in emph bgroup Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99) egroup , Springer LNCS 1628, pages 161–185, June, 1999.
• Atsushi Igarashi and Benjamin C. Pierce. On inner classes. Information and Computation, 177(1):56–89, August 2002. A special issue with papers from the 7th International Workshop on Foundations of Object-Oriented Languages (FOOL7). An earlier version appeared in emph bgroup Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000) egroup , Springer LNCS 1850, pages 129–153, June, 2000. (PDF)
• Atsushi Igarashi and Mirko Viroli. On variance-based subtyping for parametric types. In Boris Magnusson, editor, Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP2002), volume 2374 of Lecture Notes in Computer Science, pages 441–469, Málaga, Spain, June 2002. Springer-Verlag.
• Yukiyoshi Kameyama and Masahiko Sato. Strong normalizability of the non-deterministic catch/throw calculi. Theoretical Computer Science, 272(1–2):223–245, 2002.
• Masahiko Sato, Yukiyoshi Kameyama, and Takeuti Izumi. CAL: A computer assisted learning system for computation and logic. In Proceedings of the 8th International Workshop on Computer Aided Systems Theory (EUROCAST 2001), volume 2178 of Lecture Notes in Computer Science, pages 509–524. Springer-Verlag, 2002.
• Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama. A simply typed context calculus with first-class environments. Journal of Functional and Logic Programming, 2002(4):1–41, 2002.
• Azza A. Taha, Masahiko Sato, and Yukiyoshi Kameyama. A second order context calculus. Journal of Information Processing Society of Japan, 19(3):158–175, 2002.

2001

• Masahiko Sato, Takafumi Sakurai, and Rod Burstall. Explicit environments. Fundamenta Informaticae, 45(1–2):79–115, 2001. Errata is available at http://www.sato.kuis.kyoto-u.ac.jp/~masahiko/papers/expenv-errata.dvi.
• Masahiko Sato, Takafumi Sakurai, and Yukiyoshi Kameyama. A simply typed context calculus with first-class environments. In Proceedings of the Fifth International Symposium on Functional and Logic Programming (FLOPS 2001), volume 2024 of Lecture Notes in Computer Science, pages 359–374, Tokyo, Japan, 2001. Springer-Verlag.
• Masahiko Sato. Theory of judgments and derivations. In S. Arikawa and A. Shinohara, editors, Progres in Discovery Science, Lecture Notes in Artificial Intelligence, State-of-the-Art Surveys. Springer-Verlag, 2001.
• Azza A. Taha, Masahiko Sato, and Yukiyoshi Kameyama. A second order context calculus. In Proceedings of the 3rd Workshop on Programming and Programming Languages (PPL2001), pages 71–82, Kameoka, Japan, March 2001.
• Azza A. Taha, Masahiko Sato, and Yukiyoshi Kameyama. A type-free context calculus. Journal of Information Processing Society of Japan, 42(1), 2001.

2000

• Yukiyoshi Kameyama. A type system for delimited continuations. In Proceedings of the 2nd Workshop on Programming and Programming Languages (PPL2000), pages 4–11, Kanzanji, Japan, 2000.
• Yukiyoshi Kameyama. A type-theoretic study on partial continuations. In Proceedings of the IFIP International Conference on Theoretical Computer Science (IFIP TCS2000), Lecture Notes in Computer Science, Sendai, Japan, August 2000. Springer-Verlag.
• Izumi Takeuti. Pruning for principal type assignment. In D. A. Wolfram, editor, Proceedings of the CATS 2000, Computing: The Australian Theory Symposium, volume 31 of Electronic Notes in Theoretical Computer Science, 2000.

1999

• Masahiko Sato, Takafumi Sakurai, and Rod Burstall. Explicit environments. In Proceedings of the International Conference on Typed Lambda-Calculi and Applications (TLCA'99), volume 1581 of Lecture Notes in Computer Science, pages 340–354. Springer-Verlag, 1999.

1998

• Yukiyoshi Kameyama and Masahiko Sato. A classical catch/throw calculus with tag abstractions and its strong normalizability. In Proceedings of the CATS'98, volume 20 of Australian Computer Science Communications, pages 183–197. Springer-Verlag, 1998.
• Izumi Takeuti. An axiomatic system of parametricity. Fundamenta Informaticae, 33:397–432, 1998.
• Izumi Takeuti. A type theory for cyclic structure. In Proceedings of the 3rd Fuji International Symposium on Functional and Logic Programming, pages 207–226. World Scientific, 1998.

1997

• Yukiyoshi Kameyama. A new formulation of the catch/throw mechanism. In Proceedings of the Second Fuji International Workshop on Functional and Logic Programming, pages 106–122. World-Scientific, 1997.
• Masahiko Sato. Classical Brouwer-Heyting-Kolmogorov interpretation. In M. Li and A. Maruoka, editors, Proceedings of the Algorithmic Learning Theory, volume 1316 of Lecture Notes in Artificial Intelligence, pages 176–196, Sendai, Japan, 1997. Springer-Verlag.
• Masahiko Sato. Intuitionistic and classical natural deduction systems with the catch and the throw rules. Theoretical Computer Science, 175(1):75–92, 1997.
• Izumi Takeuti. An axiomatic system of parametricity. In P. de Groote and J. R. Hindley, editors, Proceedings of the International Conference on Typed Lambda-Calculi and Applications (TLCA'97), volume 1210, pages 354–372. Springer-Verlag, 1997.

1996

• Yukiyoshi Kameyama. A type-free theory of half-monotone inductive definitions. International Journal of Foundations of Computer Science, 6(3):203–234, 1995.
• Yukiyoshi Kameyama. A new formulation of the catch/throw mechanism. In Proceedings of the Second Fuji International Workshop on Functional and Logic Programming. World-Scientific, November 1996.
• Masahiko Sato and Yukiyoshi Kameyama. Conservativeness of lambda over lambda-sigma-calculus. In Neil D. Jones, Masami Hagiya, and Masahiko Sato, editors, Logic, Language and Computation: Festschrift in Honor of Satoru Takasu, volume 792 of Lecture Notes in Computer Science, pages 73–94, 1994.
• Masahiko Sato. A purely functional language with encapsulated assignment. In Proceedings of the Theoretical Aspects of Computer Software (TACS'94), volume 789 of Lecture Notes in Computer Science, pages 179–202, Sendai, Japan, April 1994.
• Masahiko Sato. A natural deduction system with catch and throw rules. In Proceedings of the Second Workshop on Non-Standard Logic and Logical Aspects of Computer Science, Irkutsk, Russia, June 1995.