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] 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 | more details | .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.

[2] 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 | more details | .pdf ]
[3] 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 | more details | .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.

[4] 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 | more details ]
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.

[5] 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. [ more details | .pdf ]
[6] 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 | more details ]
[7] 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, 2016. [ DOI | more details | .pdf ]
[8] 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 | more details | .pdf ]
[9] 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 | more details | .pdf ]
[10] 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 | more details ]
[11] 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 | more details ]
[12] 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 | more details ]
[13] 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. [ more details ]
[14] 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 | more details ]
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.

[15] 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 | more details ]
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.

[16] 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 | more details ]
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.

[17] 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 | more details ]
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.

[18] 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 | more details ]
[19] 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 | more details | .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.

[20] 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 | more details ]
[21] 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. [ more details | .pdf ]
[22] 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 | more details | .pdf ]
[23] 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 | more details | .pdf ]
[24] 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 | more details | .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.

[25] 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 | more details | .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.

[26] 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 | more details | http ]
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.

[27] 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 | more details | .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.

[28] 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. [ DOI | pdf in ACM DL | more details | .pdf ]
Statically typed aspect-oriented programming languages restrict application of around advice only to the join points that have conforming types. Though the restriction guarantees type safety, it can prohibit application of advice that is useful, yet does not cause runtime type errors. To this problem, we present a novel weaving mechanism, called the type relaxed weaving, that allows such advice applications while preserving type safety. We formalized the mechanism, and implemented as an AspectJ compatible complier, called RelaxAJ.

[29] 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 | more details | .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.

[30] 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 | more details | 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.

[31] 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 | more details | http ]
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.

[32] 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 | more details | .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.

[33] 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 | more details | .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.

[34] 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 | more details | .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.

[35] 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 | more details | .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.

[36] 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 | more details | .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.

[37] 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 | more details | .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.

[38] 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 | more details | .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.

[39] 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 | more details | .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.

[40] 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. [ more details | .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 .

[41] 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 | more details | .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.

[42] 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 | more details | .ps.gz ]
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.

[43] 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 | more details | .pdf | .ps.gz ]
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.

[44] 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 | more details | .ps.gz ]
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.

[45] 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 | more details | .ps.gz ]
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.

[46] 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/. [ more details | .ps.gz ]
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.

[47] 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. [ more details | .ps.gz ]
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.

[48] 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 | more details | .pdf | .ps.gz ]
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.

[49] Atsushi Igarashi. Formalizing Advanced Class Mechanisms. PhD thesis, University of Tokyo, Tokyo, Japan, March 2000. [ more details | .ps.gz ]
Class-based languages, such as C++ and Java, form the mainstream of object-oriented programming. The basic function of classes is to describe objects with similar behavior concisely. Recent languages have added to the basic class mechanism a variety of advanced features, such as inner classes, found in Beta and in Java 1.1, and type parameterization of classes, found in C++ as templates and in several extensions for Java, including GJ [Bracha, Odersky, Stoutamire, and Wadler]. Inner classes enable a programming style similar to nested functions/procedures, while type parameterization makes programming of polymorphic data structures, such as lists, more convenient. However, this power comes at a significant cost in complexity, which makes it difficult to understand the behavior of programs.

The main goal of this work is to clarify the essence of the type systems and compilation schemes of inner classes and GJ-style type parameterization. We approach this goal by building their formal models based on a small core calculus, called Featherweight Java, for class-based object-oriented languages, and by proving their properties, such as type soundness. Our contributions are as follows.

    Design and formalization of Featherweight Java. It is intended to be a smallest possible language to capture the essential parts of type systems of class-based object-oriented languages, so that proofs for the complex extensions are tractable. Formalization of the core of inner classes and proof of its type safety. Featherweight Java is extended with inner classes; the definition of its semantics illuminates complexity related to interaction between inner classes and inheritance. Formalization of the core of GJ and proof of its type safety. We extend Featherweight Java with type parameterization and raw types, one of GJ's distinctive features. Raw types are designed to maintain compatibility between polymorphic classes and their legacy clients that still expect the old monomorphic version of those classes. The proof of type soundness of raw types uncovers some underspecifications and flaws in the current design of raw types. Formalization and proof of correctness of the compilation schemes of inner classes and GJ. We model the current compilers by giving translation from the extended languages into Featherweight Java, and prove that the translation preserves well-typedness and semantics.

[50] Atsushi Igarashi. Type-based analysis of usage of values for concurrent programming languages. Master's thesis, University of Tokyo, Tokyo, Japan, February 1997. [ more details | .ps.gz ]