Papers and Talks

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.

Research Talks

Papers

N.B. If your browser supports CSS2, you can see the abstract of a paper by pressing (and holding) a mouse button on the entry. Otherwise, (or if you are not patient enough to do so :-), just click "more details".

[1] 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 [22]. [ DOI | Creative Commons License Licensed under Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License | .pdf ]
Context-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers---modules to describe context-dependent behavioral variations of a software system---and their dynamic activation, which can modify the behavior of multiple objects that have already been instantiated. Typechecking programs written in a COP language is difficult because the activation of a layer can even change objects' interfaces. Inoue et al. have informally discussed how to make JCop, an extension of Java for COP by Appeltauer et al., type-safe. In this article, we formalize a small COP language called with its operational semantics and type system and show its type soundness. The language models main features of the type-safe version of JCop, including dynamically activated first-class layers, inheritance of layer definitions, layer subtyping, and layer swapping.

[2] 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 ]
[3] 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 | pdf in ACM DL ]

[4] 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 | pdf in ACM DL ]
[5] 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 ]
[6] Taro Sekiyama and Atsushi Igarashi. Reasoning about polymorphic manifest contracts, June 2018. Draft. [ DOI ]
[7] 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 [18]. [ DOI ]
[8] 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 [23]. [ DOI | Creative Commons License Licensed under Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License | .pdf ]
[9] 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 | pdf in ACM DL ]
Loop fusion---a program transformation to merge multiple consecutive loops into a single one---has been studied mainly for compiler optimization. In this paper, we propose a new loop fusion strategy, which can fuse any loops---even loops with data dependence---and show that it is useful for program verification because it can simplify loop invariants.

The crux of our loop fusion is the following observation: if the state after the first loop were known, the two loop bodies could be computed at the same time without suffering from data dependence by renaming program variables. Our loop fusion produces a program that guesses the unknown state after the first loop nondeterministically, executes the fused loop where variables are renamed, compares the guessed state and the state actually computed by the fused loop, and, if they do not match, diverges. The last two steps of comparison and divergence are crucial to preserve partial correctness. We call our approach “guess-and-assume” because, in addition to the first step to guess, the last two steps can be expressed by the pseudo-instruction assume, used in program verification.

We formalize our loop fusion for a simple imperative language and prove that it preserves partial correctness. We further extend the “guess-and-assume” technique to reversing loop execution, which is useful to verify a certain type of consecutive loops. Finally, we confirm by experiments that our transformation techniques are indeed effective for state-of-the-art model checkers to verify a few small programs that they could not.

[10] 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 | .pdf ]
[11] 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 | pdf in ACM DL | .pdf ]
[12] 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 | .pdf ]
[13] 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 | .pdf ]
We study an extension of gradual typing---a method to integrate dynamic typing and static typing smoothly in a single language---to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed languages, type safety, blame-subtyping theorem, and the gradual guarantee---the so-called refined criteria, advocated by Siek et al. We develop System FG, which is a gradually typed extension of System F with the dynamic type and a new type consistency relation, and translation to a new polymorphic blame calculus System FC, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System FG and System FC, geared to the criteria, is influenced by the distinction between static and gradual type variables, first observed by Garcia and Cimini. This distinction is also useful to execute statically typed code without incurring additional overhead to manage type names as in the prior calculi. We prove that System FG satisfies most of the criteria: all but the hardest property of the gradual guarantee on semantics. We show that a key conjecture to prove the gradual guarantee leads to the Jack-of-All-Trades property, conjectured as an important property of the polymorphic blame calculus by Ahmed et al.

[14] 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 | pdf in ACM DL | .pdf ]
We study a Hoare Logic to reason about parallel programs executed on graphics processing units (GPUs), called GPU kernels. During the execution of GPU kernels, multiple threads execute in lockstep, that is, execute the same instruction simultaneously. When the control branches, the two branches are executed sequentially, but during the execution of each branch only those threads that take it are enabled; after the control converges, all the threads are enabled and again execute in lockstep. In this article, we first consider a semantics in which all threads execute in lockstep (this semantics simplifies the actual execution model of GPUs), and adapt Hoare Logic to this setting by augmenting the usual Hoare triples with an additional component representing the set of enabled threads. It is determined that the soundness and relative completeness of the logic do not hold for all programs; a difficulty arises from the fact that one thread can invalidate the loop termination condition of another thread through shared memory. We overcome this difficulty by identifying an appropriate class of programs for which the soundness and relative completeness hold. Additionally, we discuss thread interleaving, which is present in the actual execution of GPUs but not in the lockstep semantics mentioned above. We show that, if a program is race-free, then the lockstep and interleaving semantics produce the same result. This implies that our logic is sound and relatively complete for race-free programs, even if the thread interleaving is taken into account.

[15] 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 | pdf in ACM DL | .pdf ]
[16] 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 | pdf in ACM DL | .pdf ]
This paper studies hybrid contract verification for an imperative higher-order language based on a so-called manifest contract system. In manifest contract systems, contracts are part of static types and contract verification is hybrid in the sense that some contracts are statically verified, typically by subtyping, but others are dynamically by casts. It is, however, not trivial to extend existing manifest contract systems, which have been designed mostly for pure functional languages, to imperative features, mainly because of the lack of flow-sensitivity, which should be taken into account in verifying imperative programs statically.

We develop an imperative higher-order manifest contract system λHref for flow-sensitive hybrid contract verification. We introduce a computational variant of Nanevski et al's Hoare types, which are flow-sensitive types to represent pre- and postconditions of impure computation. Our Hoare types are computational in the sense that pre- and postconditions are given by Booleans in the same language as programs so that they are dynamically verifiable. λHref also supports refinement types as in existing manifest contract systems to describe flow-insensitive, state-independent contracts of pure computation. While it is desirable that any---possibly state-manipulating---predicate can be used in contracts, abuse of stateful operations will break the system. To control stateful operations in contracts, we introduce a region-based effect system, which allows contracts in refinement types and computational Hoare types to manipulate states, as long as they are observationally pure and read-only, respectively. We show that dynamic contract checking in our calculus is consistent with static typing in the sense that the final result obtained without dynamic contract violations satisfies contracts in its static type. It in particular means that the state after stateful computations satisfies their postconditions.

As in some of prior manifest contract systems, static contract verification in this work is “post facto,” that is, we first define our manifest contract system so that all contracts are checked at run time, formalize conditions when dynamic checks can be removed safely, and show that programs with and without such removable checks are contextually equivalent. We also apply the idea of post facto verification to region-based local reasoning, inspired by the frame rule of Separation Logic.

[17] 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 | pdf in ACM DL ]
Dynamic code generation is useful for optimizing code with respect to information available only at run-time. Writing a code generator is, however, difficult and error prone. We consider a simple language for writing code generators and propose an automated method for verifying code generators. Our method is based on higher-order model checking, and can check that a given code generator can generate only closed, well-typed programs. Compared with typed multi-stage programming languages, our approach is less conservative on the typability of generated programs (i.e. can accept valid code generators that would be rejected by typical mul ti-stage languages) and can check a wider range of properties of code generators. We have implemented the proposed method and confirmed its effectiveness through experiments.

[18] 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 | .pdf ]
[19] 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. [ .pdf ]
[20] 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 | pdf in ACM DL ]
[21] 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 | .pdf ]
[22] 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 | .pdf ]
[23] 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 | pdf in ACM DL ]
[24] 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 | pdf in ACM DL ]
[25] 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 | .pdf ]
[26] 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. [ .pdf ]
[27] 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 | pdf in ACM DL ]
This paper describes a type system for JCop, which is an extension of Java with language mechanisms for context-oriented programming. A simple type system as in Java, however, is not sufficient to prevent errors due to the absence of invoked methods because interfaces of objects can change at run time by dynamic layer composition, a characteristic feature of context-oriented programming. Igarashi, Hirschfeld, and Masuhara have studied a type system for dynamic layer composition, but their type system is not directly applicable to JCop due to JCop-specific features such as layer inheritance, first-class layers, and declarative layer composition. We discuss how their type system can be extended to these language features.

[28] 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 | .pdf ]
We develop yet another typed multi-stage calculus λ^%. It extends Tsukada and Igarashi's λ^ with cross-stage persistence and is equipped with all the key features that MetaOCaml-style multi-stage programming supports. It has an arguably simple, substitution-based full-reduction semantics and enjoys basic properties of subject reduction, confluence, and strong normalization. Progress also holds under an alternative semantics that takes staging into account and models program execution. The type system of λ^% gives a sufficient condition when residual programs can be safely generated, making λ^% more suitable for writing generating extensions than previous multi-stage calculi.

[29] 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. [ DOI | .pdf ]
We study a Hoare Logic to reason about GPU kernels, which are parallel programs executed on GPUs. We consider the SIMT (Single Instruction Multiple Threads) execution model, in which multiple threads execute in lockstep (that is, execute the same instruction at a time). When control branches both branches are executed sequentially but during the execution of each branch only those threads that take it are enabled; after the control converges, all threads are enabled and execute in lockstep again. In this paper we adapt Hoare Logic to the SIMT setting, by adding an extra component representing the set of enabled threads to the usual Hoare triples. It turns out that soundness and relative completeness do not hold for all programs; a difficulty arises from the fact that one thread can invalidate the loop termination condition of another thread through shared memory. We overcome this difficulty by identifying an appropriate class of programs for which soundness and relative completeness hold.

[30] 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 | pdf in ACM DL ]
Most if not all extensions to object-oriented languages that allow for context-oriented programming (COP) are asymmetric in the sense that they assume a base implementation of a system to be composed into classes and a set of layers to provide behavioral variations applied to those classes at run-time. We propose L as an experimental language to further explore the design space for COP languages. In this position paper we talk about first steps towards the unification of classes and layers and with that the removal of the asymmetry in composition mechanisms of contemporary COP implementations.

[31] 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. [ DOI | .pdf ]
[32] 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 \bgroupProceedings of the 24th Annual ACM Symposium on Applied Computing (SAC2009), pages 1851-1858, March 2009.DOI | .pdf ]
The notion of MyType has been proposed to promote type-safe reuse of binary methods and recently extended to mutually recursive definitions. It is well known, however, that MyType does not match with subtyping well. In the current type systems, type safety is guaranteed at the expenses of subtyping, hence dynamic dispatch. In this article, we propose two mechanisms, namely, nonheritable methods and exact statements to remedy the mismatch between MyType and subtyping. We rigorously prove their safety by modeling them in a small calculus.

[33] 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 | pdf in ACM DL ]
[34] 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 ]
[35] 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. [ DOI | pdf in ACM DL | .pdf ]
[36] 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. [ DOI | .pdf ]
[37] 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. [ DOI | pdf in ACM DL | .pdf ]
We develop a minimal core calculus called ContextFJ to model language mechanisms for context-oriented programming (COP). Unlike other formal models of COP, ContextFJ has a direct operational semantics that can serve as a precise description of the core of COP languages. We also discuss a simple type system that helps to prevent undefined methods from being accessed via proceed.

[38] 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 \bgroupProceedings of the Intutionistic Modal Logics and Applications Workshop (IMLA'08).DOI | .pdf ]
In this paper we study a version of constructive linear-time temporal logic (LTL) with the “next” temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time analysis via the Curry-Howard isomorphism. However, he did not investigate the logic itself in detail; he has proved only that the logic augmented with negation and classical reasoning is equivalent to (the “next” fragment of) the standard formulation of classical linear-time temporal logic. We give natural deduction, sequent calculus and Hilbert-style proof systems for constructive LTL with conjunction, disjunction and falsehood, and show that the sequent calculus enjoys cut elimination. Moreover, we also consider Kripke semantics and prove soundness and completeness. One distinguishing feature of this logic is that distributivity of the “next” operator over disjunction “O(A VB) OA VOB” is rejected in view of a type-theoretic interpretation.

[39] 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 \bgroupProceedings of the 9th International Conference on Typed Lambda-Calculi and Applications (TLCA'09), volume 5608 of Springer LNCS, pages 341-355, June, 2009.DOI ]
Taha and Nielsen have developed a multi-stage calculus λ^α with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable.

In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by developing a typed λ-calculus λ^. It corresponds to multi-modal logic that allows quantification by transition variables---a counterpart of classifiers---which range over (possibly empty) sequences of labeled transitions between possible worlds. This interpretation will reduce the “run” construct---which has a special typing rule in λ^α---and embedding of closed code into other code fragments of different stages---which would be only realized by the cross-stage persistence operator in λ^α---to merely a special case of classifier application. λ^ enjoys not only basic properties including subject reduction, confluence, and strong normalization but also an important property as a multi-stage calculus: time-ordered normalization of full reduction.

Then, we develop a big-step evaluation semantics for an ML-like language based on λ^ with its type system and prove that the evaluation of a well-typed λ^ program is properly staged. We also identify a fragment of the language, where erasure evaluation is possible.

Finally, we show that the proof system augmented with a classical axiom is sound and complete with respect to a Kripke semantics of the logic.

[40] 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. [ DOI | pdf in ACM DL | .pdf ]
We propose an enhancement of method dispatch for enabling to compose both normal and crosscutting program structures. Our idea is to use predicate dispatch modified to refer to external calling contexts. Despite the support of crosscutting structures, our language based on this idea, named GluonJ, allows mostly modular typechecking and compilation. Its execution overhead is negligible. We show these facts through practice and theory.

[41] 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. [ DOI | pdf in ACM DL | .pdf ]
Bruce and Foster proposed the language LOOJ, an extension of Java with the notion of MyType, which represents the type of a self reference and changes its meaning along with inheritance. MyType is useful to write extensible yet type-safe classes for objects with recursive interfaces, that is, ones with methods that take or return objects of the same type as the receiver.

Although LOOJ has also generics, MyType has been introduced as a feature rather orthogonal to generics. As a result, LOOJ cannot express an interface that refers to the same generic class recursively but with different type arguments. This is a significant limitation because such an interface naturally arises in practice, for example, in a generic collection class with method map(), which converts a collection to the same kind of collection of different elements. Altherr and Cremet and Moors, Piessens, and Odersky gave solutions to this problem but they used a highly sophisticated combination of advanced mechanisms such as abstract type members, higher-order type constructors, and F-bounded polymorphism.

In this paper, we give another solution by introducing self type constructors, which integrate MyType and generics so that MyType can take type arguments in a generic class. Our solution is simpler---it uses only first-order type constructors and neither abstract type members nor F-bounds. We demonstrate the expressive power of self type constructors by means of examples, formalize a core language with self type constructors, and prove its type safety.

[42] 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. [ DOI | pdf in ACM DL | .pdf ]
Gradual typing, proposed by Siek and Taha, is a framework to combine the benefits of static and dynamic typing. Under gradual typing, some parts of the program are type-checked at compile time, and the other parts are type-checked at run time. The main advantage of gradual typing is that a programmer can write a program rapidly without static type annotations in the beginning of development, then add type annotations as the development progresses and end up with a fully statically typed program; and all these development steps are carried out in a single language.

This paper reports work in progress on the introduction of gradual typing into class-based object-oriented programming languages with generics. In previous work, we have developed a gradual typing system for Featherweight Java and proved that statically typed parts do not go wrong. After reviewing the previous work, we discuss issues raised when generics are introduced, and sketch a formalization of our solutions.

[43] 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. [ DOI | pdf in ACM DL | .pdf ]

[44] 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 \bgroupProceedings of the 11th Annual Asian Computing Science Conference (ASIAN'06), volume 4435 of Springer LNCS, pages 302-316, December, 2006.DOI | http ]
Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F preserves the logical relations defined for both calculi. In fact, we have found a counterexample for it. Instead, we prove noninterference for sealing calculus, a new variant of DCC, by reduction to the basic lemma of a logical relation for the simply typed λ-calculus, using a fully complete translation to the simply typed λ-calculus. Full completeness plays an important role in showing preservation of the two logical relations through the translation. Also, we investigate relationship among sealing calculus, DCC, and an extension of DCC by Tse and Zdancewic and show that the first and the last of the three are equivalent.

[45] 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 ]
We have proposed lightweight family polymorphism, a programming style to support reusable yet type-safe mutually recursive classes, and introduced its formal core calculus .FJ. In this paper, we give a formal translation, which changes only type declarations, from .FJ into FGJself, an extension of Featherweight GJ with self type variables. They improve self typing and are required for the translation to preserve typing. Therefore we claim that self type variables represent the essential difference between .FJ and Featherweight GJ, namely, lightweight family polymorphism provides better self typing for mutually recursive classes than Java generics. To support this claim rigorously, we show that FGJself enjoys type soundness and the formal translation preserves typing and reduction.

[46] Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Lightweight family polymorphism. Journal of Functional Programming, 18(3):285--331, 2008. A preliminary summary appeared in \bgroupProceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS 2005), Springer LNCS vol. 3780, pages 161--177, November, 2005.DOI | .pdf ]
Family polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system.

In this article, we propose a simpler solution of lightweight family polymorphism, based on the idea that families are represented by classes rather than objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.

[47] 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. [ DOI | .pdf ]
We develop virtual machines and compilers for a multi-level language, which supports multi-stage run-time specialization by composing program fragments with quotation mechanisms. We consider two styles of virtual machines---ones equipped with special instructions for code generation and ones without---and show that the latter kind can deal with, more easily, low-level code generation, which avoids the overhead of (run-time) compilation by manipulating instruction sequences, rather than source-level terms, as data. The virtual machines and accompanying compilers are derived by program transformation, which extends Ager et al.'s derivation of virtual machines from evaluators.

[48] 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. [ DOI | pdf in ACM DL | .pdf ]
Much recent work in the design of object-oriented programming languages has been focusing on identifying suitable features to support so-called scalable extensibility, where the usual extension mechanism by inheritance works in different scales of software components---that is, classes, groups of classes, groups of groups and so on. We contribute to this topic by introducing the mechanism of variant path types. They provide a flexible means to intra-group relationship (among classes) that has to be preserved through extension, and rich abstractions to express various kinds of sets of objects with flexible subtyping, by the new notions of exact and inexact qualifications. We formalize a safe type system for variant path types on top of Featherweight Java. Our development results in a lightweight solution for scalable extensibility in Java-like programming languages.

[49] 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. [ DOI | pdf in ACM DL | .pdf ]
We propose union types for statically typed class-based object-oriented languages as a means to enhance the flexibility of subtyping. As its name suggests, a union type can be considered the set union of instances of several types and behaves as their least common supertype. It also plays the role of an interface that “factors out” commonality---fields of the same name and methods with similar signatures---of given types. Union types can be useful for implementing heterogeneous collections and for grouping independently developed classes with similar interfaces, which has been considered difficult in languages like Java. To rigorously show the safety of union types, we formalize them on top of Featherweight Java and prove that the type system is sound.

[50] 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 \bgroup Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP2002), Springer LNCS vol. 2374, pages 441--469, June 2002.DOI | pdf in ACM DL | .pdf ]
We develop the mechanism of variant parametric types, as a means to enhance synergy between parametric and inclusion polymorphism in object-oriented programming languages. Variant parametric types are used to control both subtyping between different instantiations of one generic class and the accessibility of their fields and methods. On one hand, one parametric class can be used to derive covariant types, contravariant types, and bivariant types (generally called variant parametric types), by attaching a variance annotation to a type argument. On the other hand, the type system prohibits certain method/field accesses according to variance annotations, when those accesses may otherwise make the program unsafe. By exploiting variant parametric types, a programmer can write generic code abstractions working on a wide range of parametric types in a safe way. For instance, a method that only reads the elements of a container of numbers can be easily modified so as to accept containers of integers, floating numbers, or any subtype of the number type.

Technical subtleties in typing for the proposed mechanism are addressed in terms of an intuitive correspondence between variant parametric types and bounded existential types. Then, for a rigorous argument of correctness of the proposed typing rules, we extend FGJ---an existing formal core calculus for Java with generics---with variant parametric types and prove type soundness.

[51] 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. [ DOI | pdf in ACM DL | .pdf ]
Multi-level generating extensions, studied by Glück and Jørgensen, are generalization of (two-level) program generators, such as parser generators, to arbitrary many levels. By this generalization, the notion of persistent code---a quoted code fragment that can be used for different stages---naturally arises.

In this paper we propose a typed lambda calculus λO, based on linear-time temporal logic, as a basis of programming languages for multi-level generating extensions with persistent code. The key idea of the type system is correspondence of (1) linearly ordered times in the logic to computation stages; (2) a formula O A (next A) to a type of code that runs at the next stage; and (3) a formula A (always A) to a type of persistent code executable at and after the current stage. After formalizing λO, we prove its key property of time-ordered normalization that a well-typed program can never go back to a previous stage in a “time-ordered” execution, as well as basic properties such as subject reduction, confluence and strong normalization. Commuting conversion plays an important role for time-ordered normalization to hold.

[52] 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. [ DOI | pdf in ACM DL | .pdf ]
Igarashi and Kobayashi have proposed a general type system for checking whether resources such as files and memory are accessed in a valid manner. Their type system is, however, for call-by-value λ-calculus with resource primitives, and does not deal with non-functional primitives such as exceptions and pointers. We extend their type system to deal with exception primitives and prove soundness of the type system. Dealing with exception primitives is especially important in practice, since many resource access primitives may raise exceptions. The extension is non-trivial: While Igarashi and Kobayashi's type system is based on linear types, our new type system is a combination of linear types and effect systems. We also report on a prototype analyzer based on the new type system.

[53] 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. [ DOI | .pdf ]
Family polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system. In this paper, we propose a simpler solution of lightweight family polymorphism, based on the idea that families are represented by classes rather than objects. This change makes the type system significantly simpler without losing much expressibility of the language. Moreover, “family-polymorphic” methods now take a form of parametric methods; thus it is easy to apply the Java-style type inference. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove the type system is sound. An algorithm of type inference for family-polymorphic method invocations is also formalized and proved to be correct.

[54] 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 \bgroup 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.DOI | pdf in ACM DL | .pdf ]
It is an important criterion of program correctness that a program accesses resources in a valid manner. For example, a memory region that has been allocated should be eventually deallocated, and after the deallocation, the region should no longer be accessed. A file that has been opened should be eventually closed. So far, most of the methods to analyze this kind of property have been proposed in rather specific contexts (like studies of memory management and verification of usage of lock primitives), and it was not so clear what is the essence of those methods or how methods proposed for individual problems are related. To remedy this situation, we formalize a general problem of analyzing resource usage as a resource usage analysis problem, and propose a type-based method as a solution to the problem.

[55] 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 ]
Information flow analysis is a program analysis that detects possible illegal information flow such as the leakage of (partial information on) passwords to the public. Recently, several type-based techniques for information flow analysis have been proposed for various kinds of programming languages. Details of those type systems, however, vary substantially and even their core parts are often slightly different, making the essence of the type system unclear.

In this paper we propose a typed lambda calculus as a foundation for information flow analysis. The type system is developed so that it corresponds to a proof system of an intuitionistic modal logic of validity by the Curry-Howard isomorphism. The calculus enjoys the properties of subject reduction, confluence, and strong normalization. Moreover, we show that the noninterference property, which guarantees that, in a well-typed program, no information on confidential data is leaked to the public, can be proved in a purely syntactic and surprisingly simple manner. We also demonstrate that a core part of the SLam calculus by Heintze and Riecke can be encoded into .

[56] 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 \bgroup 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.DOI | .pdf ]
We propose a general, powerful framework of type systems for the π-calculus, and show that we can obtain as its instances a variety of type systems guaranteeing non-trivial properties like deadlock-freedom and race-freedom. A key idea is to express types and type environments as abstract processes: We can check various properties of a process by checking the corresponding properties of its type environment. The framework clarifies the essence of recent complex type systems, and it also enables sharing of a large amount of work such as a proof of type preservation, making it easy to develop new type systems.

[57] 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. [ DOI | .pdf ]
The notion of meta-variable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of meta-variables in textbooks, we propose two formal systems that have the notion of meta-variable.

In both calculi, each variable is given a level (non-negative integer), which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a meta-level function operating on the metameta-level. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a meta-variable, free object-level variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as meta-level functions on object-level terms, hence uses capture-avoiding substitution.

We show both calculi enjoy a number of properties including Church-Rosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.

[58] 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 \bgroup Proceedings of the 14th European Conference on Object-Oriented Programming (ECOOP2000), Springer LNCS 1850, pages 129--153, June, 2000.DOI | .pdf ]
Inner classes in object-oriented languages play a role similar to nested function definitions in functional languages, allowing an object to export other objects that have direct access to its own methods and instance variables. However, the similarity is deceptive: a close look at inner classes reveals significant subtleties arising from their interactions with inheritance.

The goal of this work is a precise understanding of the essential features of inner classes; our object of study is a fragment of Java with inner classes and inheritance (and almost nothing else). We begin by giving a direct reduction semantics for this language. We then give an alternative semantics by translation into a yet smaller language with only top-level classes, closely following Java's Inner Classes Specification. We prove that the two semantics coincide, in the sense that translation commutes with reduction, and that both are type-safe.

[59] 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 \bgroup Proceedings of the 13th European Conference on Object-Oriented Programming (ECOOP'99), Springer LNCS 1628, pages 161--185, June, 1999.DOI | .pdf ]
Virtual types have been proposed as a notation for generic programming in object-oriented languages---an alternative to the more familiar mechanism of parametric classes. The tradeoffs between the two mechanisms are a matter of current debate: for many examples, both appear to offer convenient (indeed almost interchangeable) solutions; in other situations, one or the other seems to be more satisfactory. However, it has proved difficult to draw rigorous comparisons between the two approaches, partly because current proposals for virtual types vary considerably in their details, and partly because the proposals themselves are described rather informally, usually in the complicating context of full-scale language designs.

Work on the foundations of object-oriented languages has already established a clear connection between parametric classes and the polymorphic functions found in familiar typed lambda-calculi. Our aim here is to explore a similar connection between virtual types and dependent records.

We present, by means of examples, a straightforward model of objects with embedded type fields in a typed lambda-calculus with subtyping, type operators, fixed points, dependent functions, and dependent records with both “bounded” and “manifest” type fields (this combination of features can be viewed as a measure of the inherent complexity of virtual types). Using this model, we then discuss some of the major differences between previous proposals and show why some can be checked statically while others require run-time checks. We also investigate how the partial “duality” of virtual types and parametric classes can be understood in terms of translations between universal and (dependent) existential types.

[60] 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 \bgroup 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.DOI | pdf in ACM DL | .pdf ]
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.

Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational “feel,” providing classes, methods, fields, inheritance, and dynamic typecasts, with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations.

As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

[61] 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. [ DOI | pdf in ACM DL | .pdf ]
[62] 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 ]
The design of GJ (Bracha, Odersky, Stoutamire and Wadler), an extension of Java with parametric polymorphism, was significantly affected by the issue of compatibility between legacy Java code and new GJ code. In particular, the introduction of raw types made it easier to interface polymorphic code with monomorphic code. In GJ, for example, a polymorphic class List<X>, parameterized by the element type X, provides not only parameterized types such as List<Object> or List<String> but also the raw type List; then, a Java class using List can be compiled without adding element types to where List is used. Raw types, therefore, can reduce (or defer, at least) programmers' burden of modifying their old Java code to match with new polymorphic code.

From the type-theoretic point of view, raw types are close to existential types in the sense that clients using a raw type C expect some implementation of a polymorphic class of the same name C. Unlike ordinary existential types, however, raw types allow several unsafe operations such as coercion from the raw type List, whose element type is abstract, to List<T> for any concrete type T. In this paper, basing on Featherweight GJ, proposed by the authors as a tiny core language of GJ, we formalize a type system and direct reduction semantics of raw types. The bottom type, which is subtype of any type, plays a key role in our type-preserving reduction semantics. In the course of the work, we have found a flaw in the typing rules from the GJ specification; type soundness is proved with respect to a repaired version of the type system.

[63] 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 ]
We propose a type-directed garbage collection (GC) scheme for a programming language with static memory management based on a linear type system. Linear type systems, which can guarantee certain values (called linear values) to be used only once during program execution, are useful for memory management: memory space for linear values can be reclaimed immediately after they are used. However, conventional pointer-tracing GC does not work under such a memory management scheme: as linear values are used, dangling pointers to the memory space for them will be yielded.

This problem is solved by exploiting static type information during garbage collection in a way similar to tag-free GC. Type information in our linear type system represents not only the shapes of heap objects but also how many times the heap objects are accessed in the rest of computation. Using such type information at GC-time, our GC can avoid tracing dangling pointers; in addition, our GC can reclaim even reachable garbage. We formalize such a GC algorithm and prove its correctness.

[64] 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. [ DOI | .pdf ]
Powerful concurrency primitives in recent concurrent languages and thread libraries provide great flexibility about implementation of high-level features like concurrent objects. However, they are so low-level that they often make it difficult to check global correctness of programs or to perform non-trivial code optimization, such as elimination of redundant communication. In order to overcome those problems, advanced type systems for input-only/output-only channels and linear (use-once) channels have been recently studied, but the type reconstruction problem for those type systems remained open, and therefore, their applications to concurrent programming languages have been limited. In this paper, we develop type reconstruction algorithms for variants of Kobayashi, Pierce, and Turner's linear channel type system with Pierce and Sangiorgi's subtyping based on input-only/output-only channel types, and prove correctness of the algorithms. To our knowledge, no complete type reconstruction algorithm has been previously known for those type systems. We have implemented one of the algorithms and incorporated it into the compiler of the concurrent language HACL. This paper also shows some experimental results on the algorithm and its application to compile-time optimizations.

[65] 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. [ DOI | .pdf ]
[66] 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. [ DOI | pdf in ACM DL | .pdf ]
Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy.

Featherweight Java bears a similar relation to full Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational “feel,” providing classes, methods, fields, inheritance, and dynamic typecasts, with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The syntax, type rules, and operational semantics of Featherweight Java fit on one page, making it easier to understand the consequences of extensions and variations.

As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and sketch a proof of type safety. The extended system formalizes for the first time some of the key features of GJ.

[67] 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 ]
[68] Atsushi Igarashi and Naoki Kobayashi. Type-based analysis of communication for concurrent programming languages. In Pascal Van Hentenryck, editor, Proceedings of the Fourth International Static Analysis Symposium (SAS'97), volume 1302 of Lecture Notes in Computer Science, pages 187--201, Paris, France, September 1997. Springer-Verlag. [ DOI | .pdf ]