Type-Based Analysis of Communication for Concurrent Programming Languages. - Atsushi Igarashi; Naoki Kobayashi 001 (SAS, 1997)

Featherwieght Java: A Minimal Core Calculus for Java and GJ. - Atsushi Igarashi; Benjamin C. Pierce; Philip Wadler (OOPSLA, 1999)

Type Reconstruction for Linear -Calculus with I/O Subtyping. - Atsushi Igarashi; Naoki Kobayashi 001 (Inf. Comput., 2000)

Featherweight Java: a minimal core calculus for Java and GJ. - Atsushi Igarashi; Benjamin C. Pierce; Philip Wadler (ACM Trans. Program. Lang. Syst., 2001)

On Variance-Based Subtyping for Parametric Types. - Atsushi Igarashi; Mirko Viroli (ECOOP, 2002)

Foundations for Virtual Types. - Atsushi Igarashi; Benjamin C. Pierce (Inf. Comput., 2002)

On Inner Classes. - Atsushi Igarashi; Benjamin C. Pierce (Inf. Comput., 2002)

A generic type system for the Pi-calculus. - Atsushi Igarashi; Naoki Kobayashi 001 (Theor. Comput. Sci., 2004)

Resource usage analysis. - Atsushi Igarashi; Naoki Kobayashi 001 (ACM Trans. Program. Lang. Syst., 2005)

Formal Techniques for Java-Like Programs. - Davide Ancona; Sophia Drossopoulou; Atsushi Igarashi; Gary T. Leavens; Arnd Poetzsch-Heffter; Elena Zucca (ECOOP Workshops, 2006)

Resource usage analysis for a functional language with exceptions. - Futoshi Iwama; Atsushi Igarashi; Naoki Kobayashi 001 (PEPM, 2006)

A modal type system for multi-level generating extensions with persistent code. - Yosihiro Yuse; Atsushi Igarashi (PPDP, 2006)

Variant parametric types: A flexible subtyping scheme for generics. - Atsushi Igarashi; Mirko Viroli (ACM Trans. Program. Lang. Syst., 2006)

Deriving Compilers and Virtual Machines for a Multi-level Language. - Atsushi Igarashi; Masashi Iwaki (APLAS, 2007)

Variant path types for scalable extensibility. - Atsushi Igarashi; Mirko Viroli (OOPSLA, 2007)

Union Types for Object-Oriented Programming. - Atsushi Igarashi; Hideshi Nagira (J. Object Technol., 2007)

Formal Techniques for Java-Like Programs. - Elvira Albert; Anindya Banerjee 001; Sophia Drossopoulou; Marieke Huisman; Atsushi Igarashi; Gary T. Leavens; Peter Müller 001; Tobias Wrigstad (ECOOP Workshops, 2008)

Calculi of meta-variables. - Masahiko Sato 001; Takafumi Sakurai; Yukiyoshi Kameyama; Atsushi Igarashi (Frontiers Comput. Sci. China, 2008)

Lightweight family polymorphism. - Chieri Saito; Atsushi Igarashi; Mirko Viroli (J. Funct. Program., 2008)

The Essence of Lightweight Family Polymorphism. - Chieri Saito; Atsushi Igarashi (J. Object Technol., 2008)

Proving Noninterference by a Fully Complete Translation to the Simply Typed Lambda-Calculus. - Naokata Shikuma; Atsushi Igarashi (Log. Methods Comput. Sci., 2008)

Towards gradual typing for generics. - Lintaro Ina; Atsushi Igarashi (STOP@ECOOP, 2009)

Self type constructors. - Chieri Saito; Atsushi Igarashi (OOPSLA, 2009)

Matching ThisType to subtyping. - Chieri Saito; Atsushi Igarashi (SAC, 2009)

Type relaxed weaving. - Hidehiko Masuhara; Atsushi Igarashi; Manabu Toyama (AOSD, 2010)

Mostly modular compilation of crosscutting concerns by contextual predicate dispatch. - Shigeru Chiba; Atsushi Igarashi; Salikh Zakirov (OOPSLA, 2010)

A Logical Foundation for Environment Classifiers - Takeshi Tsukada; Atsushi Igarashi (Log. Methods Comput. Sci., 2010)

A Featherweight Approach to FOOL. - Atsushi Igarashi (ECOOP, 2011)

Polymorphic Contracts. - João Filipe Belo; Michael Greenberg 002; Atsushi Igarashi; Benjamin C. Pierce (ESOP, 2011)

ContextFJ: a minimal core calculus for context-oriented programming. - Robert Hirschfeld; Atsushi Igarashi; Hidehiko Masuhara (FOAL, 2011)

Gradual typing for generics. - Lintaro Ina; Atsushi Igarashi (OOPSLA, 2011)

Constructive linear-time temporal logic: Proof systems and Kripke semantics. - Kensuke Kojima; Atsushi Igarashi (Inf. Comput., 2011)

Type-based safe resource deallocation for shared-memory concurrency. - Kohei Suenaga; Ryota Fukuda; Atsushi Igarashi (OOPSLA, 2012)

A Hoare Logic for SIMT Programs. - Kensuke Kojima; Atsushi Igarashi (APLAS, 2013)

L: context-oriented programming with only layers. - Robert Hirschfeld; Hidehiko Masuhara; Atsushi Igarashi (COP@ECOOP, 2013)

Model-Checking Higher-Order Programs with Recursive Types. - Naoki Kobayashi 001; Atsushi Igarashi (ESOP, 2013)

Matching MyType to subtyping. - Chieri Saito; Atsushi Igarashi (Sci. Comput. Program., 2013)

Automatic Memory Management Based on Program Transformation Using Ownership. - Tatsuya Sonobe; Kohei Suenaga; Atsushi Igarashi (APLAS, 2014)

Towards Type-Safe JCop: A type system for layer inheritance and first-class layers. - Hiroaki Inoue; Atsushi Igarashi; Malte Appeltauer; Robert Hirschfeld (COP@ECOOP, 2014)

On-Demand Layer Activation for Type-Safe Deactivation. - Tetsuo Kamina; Tomoyuki Aotani; Atsushi Igarashi (COP@ECOOP, 2014)

On Cross-Stage Persistence in Multi-Stage Programming. - Yuichiro Hanada; Atsushi Igarashi (FLOPS, 2014)

Software Contracts for Communication, Monitoring, and Security (NII Shonan Meeting 2014-6). - Atsushi Igarashi; Peter Thiemann 001; Philip Wadler (NII Shonan Meet. Rep., 2014)

A Sound Type System for Layer Subtyping and Dynamically Activated First-Class Layers. - Hiroaki Inoue; Atsushi Igarashi (APLAS, 2015)

Shifting the Blame - A Blame Calculus with Delimited Control. - Taro Sekiyama; Soichiro Ueda; Atsushi Igarashi (APLAS, 2015)

Manifest Contracts for Datatypes. - Taro Sekiyama; Yuki Nishida 001; Atsushi Igarashi (POPL, 2015)

Semantics and Verification of Object-Oriented Languages (NII Shonan Meeting 2015-13). - Atsushi Igarashi; Andrzej S. Murawski; Nikos Tzevelekos (NII Shonan Meet. Rep., 2015)

A library-based approach to context-dependent computation with reactive values: suppressing reactions of context-dependent functions using dynamic binding. - Hiroaki Inoue; Atsushi Igarashi (MODULARITY (Companion), 2016)

Visibility of Context-oriented Behavior and State in L. - Robert Hirschfeld; Hidehiko Masuhara; Atsushi Igarashi; Tim Felgentreff (Inf. Media Technol., 2016)

A Nonstandard Functional Programming Language. - Hirofumi Nakamura; Kensuke Kojima; Kohei Suenaga; Atsushi Igarashi (APLAS, 2017)

A DSL for compensable and interruptible executions. - Hiroaki Inoue; Tomoyuki Aotani; Atsushi Igarashi (REBLS@SPLASH, 2017)

Verification of code generators via higher-order model checking. - Takashi Suwa; Takeshi Tsukada; Naoki Kobayashi 001; Atsushi Igarashi (PEPM, 2017)

Stateful manifest contracts. - Taro Sekiyama; Atsushi Igarashi (POPL, 2017)

On polymorphic gradual typing. - Yuu Igarashi; Taro Sekiyama; Atsushi Igarashi (Proc. ACM Program. Lang., 2017)

Gradual session types. - Atsushi Igarashi; Peter Thiemann 001; Vasco T. Vasconcelos; Philip Wadler (Proc. ACM Program. Lang., 2017)

A Hoare Logic for GPU Kernels. - Kensuke Kojima; Atsushi Igarashi (ACM Trans. Comput. Log., 2017)

Polymorphic Manifest Contracts, Revised and Resolved. - Taro Sekiyama; Atsushi Igarashi; Michael Greenberg 002 (ACM Trans. Program. Lang. Syst., 2017)

ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions. - Hiroaki Inoue; Tomoyuki Aotani; Atsushi Igarashi (ECOOP, 2018)

A guess-and-assume approach to loop fusion for program verification. - Akifumi Imanishi; Kohei Suenaga; Atsushi Igarashi (PEPM, 2018)

Nondeterministic Manifest Contracts. - Yuki Nishida 001; Atsushi Igarashi (PPDP, 2018)

Reasoning about Polymorphic Manifest Contracts. - Taro Sekiyama; Atsushi Igarashi (CoRR, 2018)

ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact). - Hiroaki Inoue; Tomoyuki Aotani; Atsushi Igarashi (Dagstuhl Artifacts Ser., 2018)

Automated Verification of Functional Correctness of Race-Free GPU Programs. - Kensuke Kojima; Akifumi Imanishi; Atsushi Igarashi (J. Autom. Reason., 2018)

Method safety mechanism for asynchronous layer deactivation. - Tetsuo Kamina; Tomoyuki Aotani; Hidehiko Masuhara; Atsushi Igarashi (Sci. Comput. Program., 2018)

A Dependently Typed Multi-stage Calculus. - Akira Kawata; Atsushi Igarashi (APLAS, 2019)

Manifest Contracts with Intersection Types. - Yuki Nishida 001; Atsushi Igarashi (APLAS, 2019)

Handling Polymorphic Algebraic Effects. - Taro Sekiyama; Atsushi Igarashi (ESOP, 2019)

Temporal Verification of Programs via First-Order Fixpoint Logic. - Naoki Kobayashi 001; Takeshi Nishikawa; Atsushi Igarashi; Hiroshi Unno 001 (SAS, 2019)

Gradual Typing for Extensibility by Rows. - Taro Sekiyama; Atsushi Igarashi (CoRR, 2019)

Gradual session types. - Atsushi Igarashi; Peter Thiemann 001; Yuya Tsuda; Vasco T. Vasconcelos; Philip Wadler (J. Funct. Program., 2019)

Dynamic type inference for gradual Hindley-Milner typing. - Yusuke Miyazaki 001; Taro Sekiyama; Atsushi Igarashi (Proc. ACM Program. Lang., 2019)

A type system for first-class layers with inheritance, subtyping, and swapping. - Hiroaki Inoue; Atsushi Igarashi (Sci. Comput. Program., 2019)

Space-Efficient Gradual Typing in Coercion-Passing Style. - Yuya Tsuda; Atsushi Igarashi; Tomoya Tabuchi (ECOOP, 2020)

ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. - John Toman; Ren Siqi; Kohei Suenaga; Atsushi Igarashi; Naoki Kobayashi 001 (ESOP, 2020)

Compilation of Coordinated Choice. - Yuki Nishida 001; Atsushi Igarashi (CoRR, 2020)

Signature restriction for polymorphic algebraic effects. - Taro Sekiyama; Takeshi Tsukada; Atsushi Igarashi (Proc. ACM Program. Lang., 2020)

Verification of a Merkle Patricia Tree Library Using F. - Sota Sato 002; Ryotaro Banno; Jun Furuse; Kohei Suenaga; Atsushi Igarashi (CoRR, 2021)

(I Can't Get No) Verification (Keynote). - Atsushi Igarashi (SPLASH Companion, 2022)

Preface to the JOT special issue on ECOOP 2021: selected workshop papers. - Davide Ancona; Olivier Flückiger; Adrian Francalanza; Robert Hirschfeld; Atsushi Igarashi; Yu David Liu; Hidehiko Masuhara; Chris Seaton; Harumi Watanabe (J. Object Technol., 2022)

Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement Types. - Yuki Nishida 001; Hiromasa Saito; Ran Chen; Akira Kawata; Jun Furuse; Kohei Suenaga; Atsushi Igarashi (New Gener. Comput., 2022)

Contextual Modal Type Theory with Polymorphic Contexts. - Yuito Murase; Yuichi Nishiwaki; Atsushi Igarashi (ESOP, 2023)

Type-based Qubit Allocation for a First-Order Quantum Programming Language. - Ryo Wakizaka; Atsushi Igarashi (CoRR, 2023)

Type-Based Verification of Connectivity Constraints in Lattice Surgery. - Ryo Wakizaka; Yasunari Suzuki; Atsushi Igarashi (APLAS, 2024)

iCon: Automated Verification of Inter-Transaction Properties in Tezos Smart Contracts with Unknowns. - Yuki Nishida 001; Kohei Suenaga; Atsushi Igarashi (ICBC, 2024)

Rabbit: A Language to Model and Verify Data Flow in Networked Systems. - Terunobu Inaba; Yutaka Ishikawa; Atsushi Igarashi; Taro Sekiyama (ISNCC, 2024)

Linear Contextual Metaprogramming and Session Types. - Pedro Ângelo 002; Atsushi Igarashi; Vasco T. Vasconcelos (PLACES@ETAPS, 2024)

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric. - Atsushi Igarashi; Shota Ozaki; Taro Sekiyama; Yudai Tanabe (Proc. ACM Program. Lang., 2024)

Abstracting Effect Systems for Algebraic Effect Handlers. - Takuma Yoshioka; Taro Sekiyama; Atsushi Igarashi (Proc. ACM Program. Lang., 2024)

Functional and logic programming: Selected papers of FLOPS 2022. - Michael Hanus; Atsushi Igarashi (Sci. Comput. Program., 2024)

An ML-style module system for cross-stage type abstraction in multi-stage programming. - Takashi Suwa; Atsushi Igarashi (Sci. Comput. Program., 2026)