研究室発表論文・著書

English version

[ 2019 | 2018 | 2017 | 2016 | 2015 | 2014 | 2013 | 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.

2019

• Atsushi Igarashi, Peter Thiemann, Yuya Tsuda, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. Journal of Functional Programming, 29:e17, 2019. (doi:10.1017/S0956796819000169)
• Hiroaki Inoue and Atsushi Igarashi. A type system for first-class layers with inheritance, subtyping, and swapping. Science of Computer Programming, 179:54–86, June 2019. A revised and extended version of  [InoueIgarashi15APLAS]. (doi:10.1016/j.scico.2019.03.008)
• Akira Kawata and Atsushi Igarashi. A dependently typed multi-stage calculus. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2019), volume 11893 of Lecture Notes in Computer Science, Nusa Dua, Bali, Indonesia, December 2019. Springer-Verlag. (doi:10.1007/978-3-030-34175-6_4)
• Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. Temporal verification of programs via first-order fixpoint logic. In Proceedings of the International Symposium on Static Analysis (SAS 2019), volume 11822 of Lecture Notes in Computer Science, pages 1–24, Porto, Portugal, September 2019. Springer-Verlag. (doi:10.1007/978-3-030-32304-2_20)
• Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. Dynamic type inference for gradual Hindley–Milner typing. Proc. of the ACM on Programming Languages, 3(POPL):18:1–18:29, January 2019. Presented at ACM POPL 2019. (doi:10.1145/3290331)
• Yuki Nishida and Atsushi Igarashi. Manifest contracts with intersection types. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2019), volume 11893 of Lecture Notes in Computer Science, Nusa Dua, Bali, Indonesia, December 2019. Springer-Verlag. (doi:10.1007/978-3-030-34175-6_3)
• Taro Sekiyama and Atsushi Igarashi. Handling polymorphic algebraic effects. In Proceedings of the European Symposium on Programming (ESOP2019), volume 11423 of Lecture Notes in Computer Science, pages 1–28, Prague, Czech, April 2019. Springer-Verlag. (doi:10.1007/978-3-030-17184-1_13)
• 津田優也, 五十嵐淳. 空間効率の良いコアーション計算のためのコアーション渡し形式. In 第21回プログラミングおよびプログラミング言語ワークショップ(PPL2019)論文集, 岩手県花巻市, March 2019.

2018

• Akifumi Imanishi, Kohei Suenaga, and Atsushi Igarashi. A guess-and-assume approach to loop fusion for program verification. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2018), pages 2–14, Los Angeles, CA, January 2018. (doi:10.1145/3162070)
• Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A monadic DSL for compensable and interruptible executions. In Proceedings of the 32nd European Conference on Object-Oriented Programming (ECOOP2018), volume 109 of LIPIcs, pages 2:1–2:33, Amsterdam, Netherlands, July 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. (doi:10.4230/LIPIcs.ECOOP.2018.2)
• Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact). Dagstuhl Artifacts Series, 4(3):4:1–4:2, 2018. Received ECOOP 2018 Distinguished Artifact Award. (doi:10.4230/DARTS.4.3.4)
• Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara, and Atsushi Igarashi. Method safety mechanism for asynchronous layer deactivation. Science of Computer Programming, 156:104–120, March 2018. A revised and extended version of  [KaminaAotaniMasuharaIgarashi15COP]. (doi:10.1016/j.scico.2018.01.006)
• Kensuke Kojima, Akifumi Imanishi, and Atsushi Igarashi. Automated verification of functional correctness of race-free GPU programs. Journal of Automated Reasoning, 60(3):279–298, March 2018. A revised and extended version of  [KojimaImanishiIgarashi16VSTTE]. (doi:10.1007/s10817-017-9428-2)
• Yuki Nishida and Atsushi Igarashi. Nondeterministic manifest contracts. In Proceedings of the 20th ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP2018), pages 16:1–16:13, Frankfurt, Germany, September 2018. (doi:10.1145/3236950.3236964)
• Taro Sekiyama and Atsushi Igarashi. Reasoning about polymorphic manifest contracts, June 2018. Draft. (doi:arXiv:1806.07041)

2017

• Atsushi Igarashi, Peter Thiemann, Vasco T. Vasconcelos, and Philip Wadler. Gradual session types. Proc. of the ACM on Programming Languages, 1(ICFP), September 2017. Presented at ACM ICFP 2017. (doi:10.1145/3110282)
• Yuu Igarashi, Taro Sekiyama, and Atsushi Igarashi. On polymorphic gradual typing. Proc. of the ACM on Programming Languages, 1(ICFP), September 2017. Presented at ACM ICFP 2017. (doi:10.1145/3110284)
• Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. A DSL for compensable and interruptible executions. In Proceedings of the 4th Workshop on Reactive and Event-based Languages & Systems (REBLS), pages 8–14, Vancouver, Canada, October 2017. (doi:10.1145/3141858.3141860)
• Kensuke Kojima and Atsushi Igarashi. A Hoare logic for GPU kernels. ACM Transactions on Computational Logic, 18(1):3:1–3:43, February 2017. A preliminary version appeared in Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2013) under the title ``A Hoare Logic for SIMT Programs''. (doi:10.1145/3001834)
• Yusuke Miyazaki and Atsushi Igarashi. A type reconstruction algorithm for gradually typed delimited continuations. In 第19回プログラミングおよびプログラミング言語ワークショップ(PPL2017)論文集, 山梨県笛吹市, March 2017.
• Hirofumi Nakamura, Kensuke Kojima, Kohei Suenaga, and Atsushi Igarashi. A nonstandard functional programming language. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2017), volume 10695 of Lecture Notes in Computer Science, pages 514–533, Suzhou, China, November 2017. (doi:10.1007/978-3-319-71237-6_25)
• Taro Sekiyama and Atsushi Igarashi. Stateful manifest contracts. In Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL2017), pages 530–544, Paris, France, January 2017. (doi:10.1145/3009837.3009875)
• Taro Sekiyama, Atsushi Igarashi, and Michael Greenberg. Polymorphic manifest contracts, revised and resolved. ACM Transactions on Programming Languages and Systems, 39(1):3:1–3:36, January 2017. (doi:10.1145/2994594)
• Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, and Atsushi Igarashi. Verification of code generators via higher-order model checking. In Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM2017), pages 59–70, Paris, France, January 2017. (doi:10.1145/3018882.3018886)
• 矢杉 和義, 五十嵐 淳. C言語における無効なスタック領域へのポインタを検出する静的解析. In 日本ソフトウェア科学会第34回大会論文集, 横浜市港北区, September 2017.

2016

• Hiroaki Inoue and Atsushi Igarashi. A library-based approach to context-dependent computation with reactive values. In Proceedings of the Constrained and Reactive Objects Workshop (CROW 2016), Málaga, Spain, March 2016. (doi:10.1145/2892664.2892669)
• Kensuke Kojima, Akifumi Imanishi, and Atsushi Igarashi. Automated verification of functional correctness of race-free GPU programs. In Proceedings of the 8th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2016), volume 9971 of Lecture Notes in Computer Science, pages 90–106. Springer-Verlag, November 2016. (doi:10.1007/978-3-319-48869-1_7)
• Yusuke Miyazaki, Taro Sekiyama, and Atsushi Igarashi. Gradual typing for delimited continuations. In Proceedings of the International Workshop on Scripts to Programs, Rome, Italy, July 2016.
• Qi Tan, Kohei Suenaga, and Atsushi Igarashi. An extended behavioral type system for memory-leak freedom. In 日本ソフトウェア科学会第33回大会論文集, 仙台市青葉区, September 2016.
• 奥村 健太郎, 小島 健介, 五十嵐 淳. SIMT のための Hoare 論理の Coq を用いた形式化と 並列 prefix-sum アルゴリズムの検証. In 第18回プログラミングおよびプログラミング言語ワークショップ(PPL2016)論文集, 岡山県玉野市, March 2016. 日本ソフトウェア科学会.
• 馬谷 誠二, 藤原 康史, 五十嵐 淳. 階層的グループ化に基づきAndroidアプリの安全性を向上するバイトコード書換えツール. In 日本ソフトウェア科学会第33回大会論文集, 仙台市青葉区, September 2016.

2015

• Robert Hirschfeld, Hidehiko Masuhara, Atsushi Igarashi, and Tim Felgentreff. Visibility of context-oriented behavior and state in L. コンピュータソフトウェア (Computer Software), 32(3):149–158, August 2015. (doi:10.11309/jssst.32.3_149)
• Hiroaki Inoue and Atsushi Igarashi. A sound type system for layer subtyping and dynamically activated first-class layers. In Xinyu Feng and Sungwoo Park, editors, Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2015), volume 9458 of Lecture Notes in Computer Science, pages 445–464, Pohang, Korea, November 2015. Springer-Verlag. (doi:10.1007/978-3-319-26529-2_24)
• Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara, and Atsushi Igarashi. Method safety mechanism for asynchronous layer deactivation. In Proceedings of the International Workshop on Context-Oriented Programming (COP'15), Prague, Czech, July 2015. (doi:10.1145/2786545.2786550)
• Taro Sekiyama, Yuki Nishida, and Atsushi Igarashi. Manifest contracts for datatypes. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL2015), pages 195–207, January 2015. (doi:10.1145/2676726.2676996)
• Taro Sekiyama, Soichiro Ueda, and Atsushi Igarashi. Shifting the blame: A blame calculus with static delimited control. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2015), volume 9458 of Lecture Notes in Computer Science, pages 189–207, Pohang, Korea, November 2015. Springer-Verlag. (doi:10.1007/978-3-319-26529-2_11)
• Qi Tan, Kohei Suenaga, and Atsushi Igarashi. A behavioral type system for memory-leak freedom. In 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)論文集, 愛媛県松山市, March 2015. 日本ソフトウェア科学会.
• 小林 恵, 五十嵐 淳. 参照を備えた多段階計算のための多相的型システム. In 日本ソフトウェア科学会第32回大会論文集, 東京都新宿区, September 2015.
• 五十嵐 淳. 日本ソフトウェア科学会第31回大会報告. コンピュータソフトウェア, February 2015.
• 村井 涼, 五十嵐 淳, 中澤 巧爾. 高階契約を持つプログラミング言語に対するトレース意味論. In 第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)論文集, 愛媛県松山市, March 2015. 日本ソフトウェア科学会.

2014

• Gul Agha, Atsushi Igarashi, Naoki Kobayashi, Hidehiko Masuhara, Satoshi Matsuoka, Etsuya Shibayama, and Kenjiro Taura, editors. Concurrent Objects and Beyond: Papers dedicated to Akinori Yonezawa on the Occasion of His 65th Birthday, volume 8665 of Lecture Notes in Computer Science. Springer-Verlag, 2014. (doi:10.1007/978-3-662-44471-9)
• Yuichiro Hanada and Atsushi Igarashi. On cross-stage persistence in multi-stage programming. In M. Codish and E. Sumii, editors, Proceedings of the International Symposium on Functional and Logic Programming (FLOPS2014), volume 8475 of Lecture Notes in Computer Science, pages 103–118, Kanazawa, Japan, June 2014. Springer-Verlag. (doi:10.1007/978-3-319-07151-0_7)
• Robert Hirschfeld, Hidehiko Masuhara, Atsushi Igarashi, and Tim Felgentreff. Visibility of context-oriented behavior and state in L. In Proceedings of the 31st Annual Conference of Japan Society of Software Science and Technology, Nagoya, Japan, 2014.
• Hiroaki Inoue, Atsushi Igarashi, Malte Appeltauer, and Robert Hirschfeld. Towards type-safe JCop: A type system for layer inheritance and first-class layers. In Tomoyuki Aotani, editor, Proceedings of the International Workshop on Context-Oriented Programming (COP'14), Uppsala, Sweden, July 2014. (doi:10.1145/2637066.2637073)
• Tetsuo Kamina, Tomoyuki Aotani, and Atsushi Igarashi. On-demand layer activation for type-safe deactivation. In Tomoyuki Aotani, editor, Proceedings of the International Workshop on Context-Oriented Programming (COP'14), Uppsala, Sweden, July 2014. (doi:10.1145/2637066.2637070)
• Minoru Kinoshita, Kohei Suenaga, and Atsushi Igarashi. Automatic synthesis of combiners in the MapReduce framework: An approach with right inverse. In Informal Proceedings of the 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR2014), Cantabury, UK, September 2014.
• Taro Sekiyama, Yuki Nishida, and Atsushi Igarashi. Manifest contracts for datatypes, March 2014. Submitted for publication.
• Tatsuya Sonobe, Kohei Suenaga, and Atsushi Igarashi. Automatic memory management based on program transformation using ownerships. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2014), volume 8858 of Lecture Notes in Computer Science, pages 58–77. Springer-Verlag, November 2014. (doi:10.1007/978-3-319-12736-1_4)
• 五十嵐 淳, Jacques Garrigue, 古瀬 淳. 今熱い! 快進撃のOCaml. ソフトウェアデザイン2月号, January 2014.
• 関山 太朗, 西田 雄気, 五十嵐 淳. 顕在的契約計算における代数的データ型. In 第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集, 熊本県阿蘇市, March 2014. 日本ソフトウェア科学会.

2013

• Robert Hirschfeld, Atsushi Igarashi, and Hidehiko Masuhara. Layer refinement in L. In 並列/分散/協調処理に関するサマー・ワークショップ (SWoPP), 北九州市, August 2013.
• Robert Hirschfeld, Hidehiko Masuhara, and Atsushi Igarashi. L: Context-oriented programming only with layers. In Proceedings of the International Workshop on Context-Oriented Programming (COP'13), Montpellier, France, July 2013. (doi:10.1145/2489793.2489797)
• Tetsuo Kamina, Tomoyuki Aotani, Hidehiko Masuhara, Robert Hirschfeld, and Atsushi Igarashi. Towards supporting COP layers to introduce new fields, July 2013. Submitted for publication.
• Naoki Kobayashi and Atsushi Igarashi. Model checking higher-order programs with recursive types. In Proceedings of the European Symposium on Programming (ESOP2013), volume 7792 of Lecture Notes in Computer Science, pages 431–450, Rome, Italy, March 2013. Springer-Verlag. (PDF) (doi:10.1007/978-3-642-37036-6_24)
• Kensuke Kojima and Atsushi Igarashi. A Hoare logic for SIMT programs. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS2013), volume 8301 of Lecture Notes in Computer Science, pages 58–73, Melbourne, Australia, December 2013. Springer-Verlag. (PDF) (doi:10.1007/978-3-319-03542-0_5)
• Chieri Saito and Atsushi Igarashi. Matching MyType with subtyping. Science of Computer Programming, 78(7):933–952, 2013. 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) (doi:10.1016/j.scico.2012.12.010)
• 花田 裕一朗, 五十嵐 淳. 多段階計算 λ ^rhd のための越段階埋込. In 日本ソフトウェア科学会第30回大会論文集, 東京都文京区, September 2013. 高橋奨励賞受賞.

2012

• Atsushi Igarashi, Robert Hirschfeld, and Hidehiko Masuhara. A type system for dynamic layer composition. In Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL2012), Tucson, AZ, October 2012. (PDF)
• Kohei Suenaga, Ryota Fukuda, and Atsushi Igarashi. Type-based safe resource deallocation for shared-memory concurrency. In Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA2012), pages 1–20, Tucson, AZ, October 2012. (doi:10.1145/2384616.2384618)
• 関山 太朗, 五十嵐 淳. 顕在的契約計算におけるアップキャスト除去. 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. (PDF) (doi:10.1007/978-3-642-19718-5_2)
• 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), pages 19–23, Pernambuco, Brazil, March 2011. (PDF) (doi:10.1145/1960510.1960515)
• 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. (doi:10.1007/978-3-642-22655-7_20)
• 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) (doi:10.1145/2048066.2048114)
• 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) (doi:10.1016/j.ic.2010.09.008)
• 小山内 幸一, 五十嵐 淳. 低水準コード生成を行う λ° 仮想機械の融合変換を使った系統的導出. In 日本ソフトウェア科学会第28回大会論文集, 沖縄県那覇市, September 2011. (PDF)
• 五十嵐 淳. プログラミング言語の基礎概念. Number 24 in ライブラリ情報学コア・テキスト. サイエンス社, 2011. 192 頁．ISBN: 978-4-7819-1285-1.
• 大里 陽一, 五十嵐 淳, 中澤 巧爾. 例外機構を持つ型付ラムダ計算におけるパラメトリシティ, 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) (doi:10.1145/1869459.1869503)
• 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) (doi:10.1145/1739230.1739245)
• 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. (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), pages 17–26, Genova, Italy, July 2009. Available also in the ACM Digital Library. (PDF) (doi:10.1145/1570506.1570509)
• 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) (doi:10.1145/1529282.1529699)
• 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) (doi:10.1145/1640089.1640109)
• 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) (doi:10.1007/978-3-642-02273-9_25)
• 伊奈 林太郎, 五十嵐 淳. Featherweight Java のための漸進的型付け. コンピュータソフトウェア, 26(2):18–40, May 2009. PPL2008特集号. (doi:10.11309/jssst.26.2_18)

2008

• 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. (doi:10.5381/jot.2008.7.5.a3)
• 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. (doi:10.1007/s11704-008-0011-1)
• 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) (doi:10.1007/978-3-540-76637-7_14)
• 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) (doi:10.5381/jot.2007.6.2.a3)
• 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) (doi:10.1145/1297027.1297037)
• 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. 384頁．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. (doi:10.1007/978-3-540-71774-4_6)
• 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. (doi:10.1145/1141277.1141610)
• 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) (doi:10.1145/1152650)
• 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) (doi:10.1145/1111542.1111550)
• 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. (doi:10.1007/978-3-540-77505-8_24)
• 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) (doi:10.1145/1140335.1140360)
• 佐藤 雅彦. 計算と論理のための自然枠組 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) (doi:10.1145/1057387.1057390)
• 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) (doi:10.1007/11575467_12)
• 佐藤 雅彦. フレーゲの計算機科学への影響. 科学哲学, 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) (doi:10.1016/S0304-3975(03)00325-6)
• 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. (PDF) (doi:10.1007/978-3-540-45220-1_39)
• 柳楽 秀士, 五十嵐 淳. 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) (doi:10.1145/565816.503303)
• 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. (PDF) (doi:10.1006/inco.2001.2942)
• 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) (doi:10.1006/inco.2002.3092)
• 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. (doi:10.1007/3-540-47993-7_19)
• 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

• Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01), ACM SIGPLAN Notices, volume 36, number 3, pages 128–141, London, England, January 2001. (PDF) (doi:10.1145/373243.360215)
• Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396–450, May 2001. A preliminary summary appeared in Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), ACM SIGPLAN Notices, volume 34, number 10, pages 132–146, October 1999. (PDF) (doi:10.1145/503502.503505)
• Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. A recipe for raw types. In Informal Proceedings of the 8th International Workshop on Foundations of Object-Oriented Languages (FOOL8), pages 65–82, London, England, January 2001. Available through http://www.cmu.edu/~aldrich/FOOL/. (PDF)
• 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

• Atsushi Igarashi and Naoki Kobayashi. Garbage collection based on a linear type system. In Preliminary Proceedings of the 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC2000), Montreal, Canada, September 2000. Published as Technical Report CMU-CS-00-161, Carnegie Mellon University, Pittsburgh, PA. (PDF)
• Atsushi Igarashi and Naoki Kobayashi. Type reconstruction for linear π-calculus with I/O subtyping. Information and Computation, 161(1):1–44, August 2000. A preliminary summary was presented in Proceedings of SAS'97 under the title ``Type-based Analysis of Communication for Concurrent Programming Languages,'' Springer LNCS 1302, pages 187–201, September 1997. (PDF) (doi:10.1006/inco.2000.2872)
• Atsushi Igarashi and Benjamin C. Pierce. On inner classes. In Proceedings of the 7th International Workshop on Foundations of Object-Oriented Languages (FOOL7), Boston, MA, January 2000. Available through http://www.cmu.edu/~aldrich/FOOL/.
• Atsushi Igarashi and Benjamin C. Pierce. On inner classes. In Elisa Bertino, editor, Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000), volume 1850 of Lecture Notes in Computer Science, pages 129–153, Cannes, France, June 2000. Springer-Verlag. (PDF) (doi:10.1007/3-540-45102-1_7)
• Atsushi Igarashi. Formalizing Advanced Class Mechanisms. PhD thesis, University of Tokyo, Tokyo, Japan, March 2000. (PDF)
• 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

• Atsushi Igarashi and Benjamin C. Pierce. Foundations for virtual types. In Proceedings of the 6th International Workshop on Foundations of Object-Oriented Languages (FOOL6), pages 1–15, San Antonio, TX, January 1999. Available through http://www.cmu.edu/~aldrich/FOOL/.
• Atsushi Igarashi and Benjamin C. Pierce. Foundations for virtual types. In Rachid Guerraoui, editor, Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99), volume 1628 of Lecture Notes in Computer Science, pages 161–185, Lisbon, Portugal, June 1999. Springer-Verlag. (doi:10.1007/3-540-48743-3_8)
• Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweighty Java: A minimal core calculus for Java and GJ. In Linda M. Northrop, editor, Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'99), ACM SIGPLAN Notices, volume 34, number 10, pages 132–146, Denver, CO, October 1999. ACM Press. (PDF) (doi:10.1145/320385.320395)
• 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

• Atsushi Igarashi and Naoki Kobayashi. Type-based analysis of communication for concurrent programming languages. In Pascal Van Hentenryck, editor, Proceedings of the Fourth International Symposium on Static Analysis (SAS'97), volume 1302 of Lecture Notes in Computer Science, pages 187–201, Paris, France, September 1997. Springer-Verlag. (PDF) (doi:10.1007/BFb0032742)
• Atsushi Igarashi. Type-based analysis of usage of values for concurrent programming languages. Master's thesis, University of Tokyo, Tokyo, Japan, February 1997. (PDF)
• 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

• Atsushi Igarashi. Study on mechanisms for multi-object synchronization and their implementation. Senior's thesis, University of Tokyo, Tokyo, Japan, February 1995.
• 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.