Papers and Talks

Licensed under Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License

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.

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.

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 F_G, 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 F_C, which is based on previous polymorphic blame calculi by Ahmed et al. The design of System F_G and System F_C, 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 F_G 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.

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.

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 λ^H_ref 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. λ^H_ref 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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 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.

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.