Papers and Talks

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.

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.

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 and Kripke semantics for constructive LTL with conjunction and disjunction, and prove soundness and completeness. Distributivity of the ``next'' operator over disjunction is rejected from a computational viewpoint. We also give a formalization by sequent calculus and its cut-elimination procedure.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 .

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.

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.

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.

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.

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.

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.

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.

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.

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.

1. 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.
2. 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.
3. 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.
4. 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.