Davide Ancona's reports

Coinductive abstract compilation is a novel technique, which has been recently introduced for defining precise type systems for object- oriented languages. In this approach, type inference consists in translating the program to be analyzed into a Horn formula f, and in resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of f. Type systems defined in this way are idealized, since types and, con- sequently, goal derivations, are not finitely representable. Hence, sound implementable approximations have to rely on the notions of regular types and derivations, and of subtyping and subsumption between types and atoms, respectively. In this paper we address the problem of defining a sound and complete axiomatization of a subtyping relation between coinductive object and union types, defined as set inclusion between type interpretations. Besides being an important theoretical result, completeness is useful for reasoning about possible implementations of the subtyping relation, when restricted to regular types.

This paper further investigates the potential and practical applicability of abstract compilation in two different directions. First, we formally define an abstract compilation scheme for precise prediction of uncaught exceptions for a simple Java-like language; besides the usual user declared checked exceptions, the analysis covers the runtime ClassCastException. Second, we present a general implementation schema for abstract compilation based on coinductive CLP with variance annotation of user-defined predicates, and propose an implementation based on a Prolog prototype meta-interpreter, parametric in the solver for the subtyping constraints.

We propose a novel general approach for defining expressive type systems for object-oriented languages, based on abstract compilation of programs into coinductive constraint logic programs defined on a specific constraint domain X called type domain. In this way, type checking and type inference amount to resolving a certain goal w.r.t. the coinductive (that is, the greatest) Herbrand model of a logic program (that is, a Horn formula) with constraints over a fixed type domain X. In particular, we show an interesting instantiation where the constraint predicates of X are syntactic equality and subtyping over coinductive object and union types. The corresponding type system is so expressive to allow verification of simple properties like data structure invariants. Finally, we show a prototype implementation, written in Prolog, of the inference engine for coinductive CLP(X), which is parametric in the solver for the type domain X.

Writing an optimizing static compiler for dynamic languages is not an easy task, since quite complex static analysis is required. On the other hand, recent developments show that JIT compilers can exploit runtime type information to generate quite efficient code. Unfortunately, writing a JIT compiler is far from being simple. In this paper we report our positive experience with automatic generation of JIT compilers as supported by the PyPy infrastructure, by focusing on JIT compilation for .NET. The paper presents two main and novel contributions: we show that partial evaluation can be used in practice for generating a JIT compiler, and we experiment with the potentiality offered by the ability to add a further level of JIT compilation on top of .NET. The practicality of the approach is demonstrated by showing some promising experiments done with benchmarks written in a simple dynamic language.

This paper proposes a solution to the problem of semi-automatic porting of Java programs. In particular, our work aims at the design of tools able to aid users to adapt Java code in a type-safe way, when an application has to migrate to new libraries which are not fully compatible with the legacy ones. To achieve this, we propose an approach based on an integration of the two type-theoretic notions of subtyping and type isomorphism with ontology matching. While the former notions are needed to ensure flexible adaptation in the presence of type-safety, the latter supports the user to preserve the semantics of the program to be adapted.

Although coinductive logic programming (Co-LP) has proved to have several applications, including verification of infinitary properties, model checking and bisimilarity proofs, type inference via Co-LP has not been properly investigated yet. In this paper we show a novel approach to solve the problem of type inference in the context of Java-like languages, that is, object-oriented languages based on nominal subtyping. The proposed approach follows a generic scheme: first, the program P to be analyzed is translated into an approximating logic program P' and a goal G; then, the solution of the type inference problem corresponds to find an instantiation of the goal G which belongs to the greatest model of P', that is, the coinductive model of P'. Operationally, this corresponds to find a co-SLD derivation of G in P', according to the operational semantics of Co-LP recently defined by Simon et al. [ICLP06,ICALP07]. A complete formalization of an instantiation of this scheme is considered for a simple object-oriented language and a corresponding type soundness theorem is stated. A prototype implementation based on a meta-interpreter of co-SLD has been implemented. Finally, we address scalability issues of the approach, by sketching an instantiation able to deal with a much more expressive object-oriented language.

We define a framework of components based on Java-like languages, where components are binary mixin modules. Basic components can be obtained from a collection of classes by compiling such classes in isolation; for allowing that, requirements in the form of type constraints are associated with each class. Requirements are specified by the user who, however, is assisted by the compiler that can generate missing constraints essential to guarantee type safety. Basic components can be composed together by using a set of expressive typed operators; thanks to soundness results, such a composition is always type safe. The framework is designed as a separate layer that can be instantiated on top of any Java-like language; to show the effectiveness of the approach, an instantiation on a small Java subset is provided, together with a prototype implementation. Besides safety, the approach achieves great flexibility in reusing components for two reasons: (1) type constraints generated for a single component exactly capture all possible contexts where it can be safely used; (2) composition of components is not limited to conventional linking, but is achieved by means of a set of powerful operators typical of mixin modules.

We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries, and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context. We propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints. We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as what would have been produced by standard compilation of all fragments).

In this paper we present a simple calculus (called CJE) in order to fully investigate the exception mechanism of Java (in particular its interaction with inheritance). We first define a type system for the calculus, called FULL, directly driven by the Java Language Specification and prove its soundness; then, we show that this type system uses redundant types and we formally capture this fact by defining equivalence relations on types and by proving that the static semantics of CJE programs is preserved under these equivalences; furthermore, for each type we show that there exists the smallest equivalent type. Finally, we propose a simplification of the Java specification concerning throws clause which minimally affects the expressive power of the language.

We propose a new way of handling imperative features in the algebraic approach to composition of software modules, meant in its abstract categorical formulation. The basic idea is to consider, instead of a global state, orthogonal to the modular structure, the local state of a module as the collection of those components which have no associated definition but an extension which may vary dynamically. Following this intuition, composition of modules via classical operators like merge, renaming and hiding involves composition of the corresponding states, allowing one to give a truly compositional semantics of module languages. Thanks to the abstract categorical formulation, we are able to define a canonical construction of a framework for modules with state starting from a framework with no imperative features. This provides the theoretical basis for designing languages of modules with state in a way independent of the underlying core language.

In this thesis we present two formal frameworks for modeling modular languages. Following a modular approach, we separate the module and the core level of a modular language. On the linguistic side, this corresponds to define a kernel module language parametric in the underlying core language. On the semantic side, this corresponds to build a model part (in the sense of institutions), on top of a standard module framework. The standard module framework is a model part, too, satisfying some additional properties and intended as the formal counterpart of the core language. The first formal framework we propose deals with the notion of state, an essential component of modules in imperative languages. The second one is concerned with a notion of module, called mixin, which includes those of generic module and abstract class. In both cases, we present two canonical constructions yielding a formal framework where models denote modules with state and mixins, respectively, and we define a set of primitive operations over them.