研究室発表論文・著書

English version

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

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

• 関山 太朗, 五十嵐 淳. 顕在的契約計算におけるアップキャスト除去. In 第14回プログラミングおよびプログラミング言語ワークショップ(PPL2012)オンライン論文集, 和歌山県南紀白浜, March 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.
• 小山内 幸一, 五十嵐 淳. 低水準コード生成を行う λ° 仮想機械の融合変換を使った系統的導出. In 日本ソフトウェア科学会第28回大会論文集, 沖縄県那覇市, September 2011. (PDF)
• 五十嵐 淳. プログラミング言語の基礎概念. 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)
• 伊奈 林太郎, 五十嵐 淳. Featherweight Java のための漸進的型付け. コンピュータソフトウェア, 26(2):18–40, May 2009. PPL2008特集号.

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)
• 仲井間 達也, 五十嵐 淳, 小林 直樹. 文脈依存資源使用解析のための型システム. In 第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)オンライン論文集, pages 184–198, 仙台市太白区, March 2008. 日本ソフトウェア科学会. http://www.nue.riec.tohoku.ac.jp/ppl2008/. (PDF)
• 伊奈 林太郎, 五十嵐 淳. Featherweight Java のための漸進的型付け. In 第10回プログラミングおよびプログラミング言語ワークショップ(PPL2008)オンライン論文集, pages 17–31, 仙台市太白区, March 2008. 日本ソフトウェア科学会. http://www.nue.riec.tohoku.ac.jp/ppl2008/. (PDF)

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)
• 五十嵐 淳. プログラミング in OCaml〜関数型プログラミングの基礎からGUIプログラミングまで. 技術評論社, 2007. ISBN: 978-4-7741-3264-8.
• 岩間 太, 五十嵐 淳, 小林 直樹. 計算資源使用法検証における計算資源の仕様と実際の使用法との適合性検証アルゴリズム. 情報処理学会論文誌: プログラミング, 48(SIG 4(PRO32)):48–61, March 2007.

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)
• 佐藤 雅彦. 計算と論理のための自然枠組 NF/CAL. コンピュータソフトウェア, 23(3):3–13, July 2006.
• 中澤 巧爾, 龍田 真. 選言を含む自然演繹古典論理の強正規化性. In 第8回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2006), March 2006. (PDF)
• 四熊 尚方, 五十嵐 淳. 様相型に基づく情報流解析における非干渉性の論理関係による一般化とその証明. In 第8回プログラミングおよびプログラミング言語ワークショップ(PPL2006)オンライン論文集, pages 134–149, 滋賀県大津市, March 2006. 日本ソフトウェア科学会. http://ppl2006.agusa.i.is.nagoya-u.ac.jp/. (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)
• 佐藤 雅彦. フレーゲの計算機科学への影響. 科学哲学, 38(2):21–33, 2005.
• 池田 聡, 中澤 巧爾. コントロールオペレータをもつ計算体系の強正規化可能性のCPS変換を用いた証明. In 第7回プログラミングおよびプログラミング言語ワークショップ論文集 (PPL2005), pages 171–186, March 2005. (PDF)
• 岩間 太, 五十嵐 淳, 小林 直樹. 例外機構を備えた言語のための資源使用法解析. In 第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)オンライン論文集, pages 154–170, 利根郡水上町, March 2005. 日本ソフトウェア科学会. http://www.graco.c.u-tokyo.ac.jp/ppl2005/. (PDF)
• 湯瀬 芳洋, 五十嵐 淳. メタプログラミングのための時相論理に基づく型付λ計算. In 第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)オンライン論文集, pages 57–73, 利根郡水上町, March 2005. 日本ソフトウェア科学会. http://www.graco.c.u-tokyo.ac.jp/ppl2005/. (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.
• 柳楽 秀士, 五十嵐 淳. Generics・union 型を導入したオブジェクト指向計算体系. In 第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)オンライン論文集, pages 34–51, 蒲郡市, March 2004. 日本ソフトウェア科学会. http://www.is.titech.ac.jp/ppl2004/. (PDF)
• 五十嵐 淳. Generic Java: 多相的型付けによる安全かつ再利用性の高いオブジェクト指向プログラミング. 情報処理45巻6号, June 2004.

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.
• 柳楽 秀士, 五十嵐 淳. Union 型を導入したオブジェクト指向計算体系. In 日本ソフトウェア科学会第20回大会論文集, 名古屋市, September 2003. (PDF)
• 山本 和樹, 岡本 暁広, 五十嵐 淳, 佐藤 雅彦. 擬似引用を持つ型付計算体系λ q. In 第5回プログラミングおよびプログラミング言語ワークショップ(PPL2003)論文集, pages 87–102, 富士市, March 2003. 日本ソフトウェア科学会. http://wwwfun.kurims.kyoto-u.ac.jp/~nisimura/ppl2003/. (PDF)

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.
• 五十嵐 淳, 住井 英二郎. 会議レポート TACS 2001 および Manfred Paul 賞授賞式. 情報処理43巻2号, February 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.
• 中澤 巧爾. 値呼びラムダ・ミュー計算の合流性と強正規化性. In 日本ソフトウェア科学会第17回大会講演論文集 (CD-ROM), September 2000. (PDF)

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.
• 山中 淳彦, 佐藤 雅彦. 参照透明な代入をもつ純関数型言語. コンピュータソフトウェア, 14(4):56–69, 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.
• 佐藤 雅彦, 桜井 貴文. プログラムの基礎理論, volume 13 of 岩波ソフトウェア科学. 岩波書店, 1991.
• 亀山 幸義, 佐藤 雅彦. 自己反映的証明体系RPTの理論と実現. コンピュータソフトウェア, 12(2):32–51, 1995.
• 山中 淳彦, 亀山 幸義, 佐藤 雅彦. Assignment を持つ純関数型言語λの実現について. In 関数プログラミングワークショップ, pages 201–216. 近代科学社, 1994.