Corecursion is the ability of defining a function that produces some infinite data in terms of the function and the data itself, as supported by lazy evaluation. However, in languages such as Haskell strict operations fail to terminate even on infinite regular data, that is, cyclic data. Regular corecursion is naturally supported by coinductive Prolog, an extension where predicates can be interpreted either inductively or coinductively, that has proved to be useful for formal verification, static analysis and symbolic evaluation of programs. In this paper we use the meta-programming facilities offered by Prolog to propose extensions to coinductive Prolog aiming to make regular corecursion more expressive and easier to program with. First, we propose an interpreter where the search tree is pruned to guarantee termination for certain kinds of predicate definition; then we introduce finally clauses, to provide a default value for all those cases where unification with a coinductive hypothesis is not correct. Finally, we propose a finer grain semantics where the user can specify only a subset of the arguments that have to be considered when coinductive hypotheses are unified. The semantics defined by these vanilla meta-interpreters are an interesting starting point for a more mature design and implementation of coinductive Prolog.

Migrating libraries is not a trivial task, even under the simplest assumption of a downward compatible upgrade. We propose a novel approach to partially relieve programmers from this task, based on the simple observation that class, method and field names and comments contained in a Java library should be a good approximation of its semantics, and that code migration requires knowing the semantic similarities between the two libraries. Following this assumption, we borrow the main concepts and notions from the Semantic Web, and show how (1) an ontology can be automatically generated from the relevant information extracted from the code of the library; (2) semantic similarities between two different libraries can be found by running a particular ontology matching (a.k.a. ontology alignment) algorithm on the two ontologies extracted from the libraries. The main advantages of the approach are that ontology extraction can be fully automated, without adding ad-hoc code annotations, and that results and tools produced by the Semantic Web research community can be directly re-used for our purposes. Experiments carried out even with simple and efficient freely available matchers show that our approach is promising, even though it would benefit from the use of more advanced ontology matchers possibly integrated with a component for checking type compatibility of the computed alignments.

Co-recursion is the ability of defining a function that produces some infinite data in terms of the function and the data itself, and is typically supported by languages with lazy evaluation. However, in languages as Haskell strict operations fail to terminate even on infinite regular data. Regular co-recursion is naturally supported by co-inductive Prolog, an extension where predicates can be interpreted either inductively or co-inductively, that has proved to be useful for formal verification, static analysis and symbolic evaluation of programs. In this paper we propose two main alternative vanilla meta-interpreters to support regular co-recursion in Prolog as an interesting programming style in its own right, able to elegantly solve problems that would require more complex code if conventional recursion were used. In particular, the second meta-interpreters avoids non termination in several cases, by restricting the set of possible answers. The semantics defined by these vanilla meta-interpreters are an interesting starting point to study new semantics able to support regular co-recursion for non logical languages.

It is well known that big-step operational semantics are not suitable for proving soundness of type systems, because of their inability to distinguish stuck from non-terminating computations. We show how this problem can be solved by interpreting coinductively the rules for the standard big-step operational semantics of a Java-like language, thus making the claim of soundness more intuitive: whenever a program is well-typed, its coinductive operational semantics returns a value. Indeed, coinduction allows non-terminating computations to return values; this is proved by showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a proper distance function. In this way, we are able to prove soundness of a nominal type system w.r.t. the coinductive semantics. Since the coinductive semantics is sound w.r.t. the usual small-step operational semantics, the standard claim of soundness can be easily deduced.

In previous work we have shown that more precise type analysis can be achieved by exploiting union types and static single assignment (SSA) intermediate representation (IR) of code. In this paper we exploit static single information (SSI), an extension of SSA proposed in literature and adopted by some compilers, to allow assignments of more precise types to variables in conditional branches. In particular, SSI can be exploited rather easily and effectively to infer more precise types in dynamic object-oriented languages, where explicit runtime typechecking is frequently used. We show how the use of SSI form can be smoothly integrated with abstract compilation, our approach to static type analysis. In particular, we define abstract compilation based on union and nominal types for a simple dynamic object-oriented language in SSI form with a runtime typechecking operator, to show how precise type inference can be.

Corecursive FeatherWeight Java (coFJ) is a recently proposed extension of the calculus FeatherWeight Java (FJ), supporting cyclic objects and regular recursion, and explicitly designed to promote a novel programming paradigm inspired by coinductive Logic Programming (coLP), based on coinductive, rather than inductive, interpretation of recursive function definitions. We present a slightly modified version of coFJ where the application of a coinductive hypothesis can trigger the evaluation of a specific expression at declaration, rather than at use site. Following an approach inspired by abstract compilation, we then show how coFJ can be directly translated into coLP, when coinductive SLD is extended with a similar feature for explicitly solving a goal when a coinductive hypothesis is applied. Such a translation is quite compact and, besides showing the direct relation between coFJ and coinductive Prolog, provides a first prototypical but simple and effective implementation of coFJ.

Global session types are behavioral types designed for specifying in a compact way multiparty interactions between distributed components, and verifying their correctness. We take advantage of the fact that global session types can be naturally represented as cyclic Prolog terms - which are directly supported by the Jason implementation of AgentSpeak - to allow simple automatic generation of self-monitoring MASs: given a global session type specifying an interaction protocol, and the implementation of a MAS where agents are expected to be compliant with it, we define a procedure for automatically deriving a self-monitoring MAS. Such a generated MAS ensures that agents conform to the protocol at run-time, by adding a monitor agent that checks that the ongoing conversation is correct w.r.t. the global session type. The feasibility of the approach has been experimented in Jason for a non-trivial example involving recursive global session types with alternative choice and fork type constructors. Although the main aim of this work is the development of a unit testing framework for MASs, the proposed approach can be also extended to implement a framework supporting self-recovering MASs.

In this paper we investigate the theoretical foundations of global types for dynamic checking of protocol compliance in multi-agents systems and we extend the formalism by introducing a concatenation operator that allows a significant enhancement of the expressive power of global types. As examples, we show how two non trivial protocols can be compactly represented in the formalism: a ping-pong protocol, and an alternating bit protocol, in the version proposed by Deni'elou and Yoshida. Both protocols cannot be specified easily (if at all) by other global type frameworks, while in our approach they can be expressed by two deterministic types (in a sense made precise in the sequel) that can be effectively employed for dynamic checking of the conformance to the protocol.

Despite cyclic data structures occur often in many application domains, object-oriented programming languages provide poor abstraction mechanisms for dealing with cyclic objects. Such a deficiency is reflected also in the research on theoretical foundation of object-oriented languages; for instance, Featherweigh Java (FJ), which is one of the most widespread object-oriented calculi, does not allow creation and manipulation of cyclic objects. We propose an extension to Featherweight Java, called coFJ, where it is possible to define cyclic objects, {abstractly corresponding to regular terms}, and where an abstraction mechanism, called regular corecursion, is provided for supporting implementation of coinductive operations on cyclic objects. We formally define the operational semantics of coFJ, and provide a handful of examples showing the expressive power of regular corecursion; such a mechanism promotes a novel programming style particularly well-suited for implementing cyclic data structures, and for supporting coinductive reasoning.

We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. In the former, as in standard lambda calculus, the matching betweeen parameter and argument is done on a positional basis, hence alpha-equivalence holds, whereas in the latter it is done on a nominal basis. The two mechanisms also respectively correspond to static binding, where the existence and type compatibility of the argument are checked at compile-time, and dynamic binding, where they are checked at runtime.

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.

In recent work we have proposed a novel approach to define idealized type systems for object-oriented languages, based on abstract compilation of programs into Horn formulas which are interpreted w.r.t. the coinductive (that is, the greatest) Herbrand model. In this paper we investigate how this approach can be applied also in the presence of imperative features. This is made possible by con- sidering a natural translation of Static Single Assignment intermediate form programs into Horn formulas, where phi functions correspond to union types.

We define a coinductive semantics for a simple Java-like language by simply interpreting coinductively the rules of a standard big-step operational semantics. We prove that such a semantics is sound w.r.t. the usual small-step operational semantics, and then prove soundness of a conventional nominal type system w.r.t. the coinductive semantics. From these two results, soundness of the type system w.r.t. the small-step semantics can be easily deduced. This new proposed approach not only opens up new possibilities for proving type soundness, but also provides useful insights on the connection between coinductive big-step operational semantics and type systems.

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.

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, consequently, 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 complete subtyping relation <= between types built on object and union type constructors: we interpret types as sets of values, and investigate on a definition of subtyping such that t_1 <= t_2 is derivable whenever the interpretation of t_1 is contained in the interpretation of t_2. Besides being an important theoretical result, completeness is useful for reasoning about possible implementations of the subtyping relation, when restricted to regular types.

In recent work we have shown how it is possible to define very precise type systems for object-oriented languages by abstractly compiling a program into a Horn formula f. Then type inference amounts to 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 in the most interesting instantiations both the terms of the coinductive Herbrand universe and goal derivations cannot be finitely represented. However, sound and quite expressive approximations can be implemented by considering only regular terms and derivations. In doing so, it is essential to introduce a proper subtyping relation formalizing the notion of approximation between types. In this paper we study a subtyping relation on coinductive terms built on union and object type constructors. We define an interpretation of types as set of values induced by a quite intuitive relation of membership of values to types, and prove that the definition of subtyping is sound w.r.t. subset inclusion between type interpretations. The proof of soundness has allowed us to simplify the notion of contractive derivation and to discover that the previously given definition of subtyping did not cover all possible representations of the empty type.

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.

This paper discusses an application of intelligent software agents and ontologies to solve the problem of semi-automatic porting of Java programs. We have designed a system for aiding users to adapt Java code in a type- and meaning-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 meaning of names that appear in the program to be adapted. Intelligent agents control the different components of the system and interact with other agents in order to provide the final user with the semi-automatic porting service he/she required.

The Common Language Infrastructure (CLI) is a virtual machine expressly designed for implementing statically typed languages such as C#, therefore programs written in dynamically typed languages are typically much slower than C# when executed on .NET. Recent developments show that Just In Time (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. Following this approach, we have in fact added a second layer of JIT compilation, by allowing dynamic generation of more efficient .NET bytecode, which in turn can be compiled to machine code by the .NET JIT compiler. The main and novel contribution of this paper is to show that this two-layers JIT technique is effective, since programs written in dynamic languages can run on .NET as fast as (and in some cases even faster than) the equivalent C# programs. The practicality of the approach is demonstrated by showing some promising experiments done with benchmarks written in a simple dynamic language.

We propose a novel approach to constraint-based type inference based on coinductive logic programming. That is, constraint generation corresponds to translation into a conjunction of Horn clauses P, and constraint satisfaction is defined in terms of the maximal coinductive Herbrand model of P. We illustrate the approach by formally defining this translation for a small object-oriented language similar to Featherweight Java, where type annotations in field and method declarations can be omitted. In this way, we obtain a very precise type inference and provide new insights into the challenging problem of type inference for object-oriented programs. Since the approach is deliberately declarative, we define in fact a formal specification for a general class of algorithms, which can be a useful road maps to researchers. Moreover, despite we consider here a particular language, the methodology could be used in general for providing abstract specifications of type inference for different kinds of programming languages.

We propose a novel approach based on coinductive logic to specify type systems of programming languages. The approach consists in encoding programs in Horn formulas which are interpreted w.r.t. their coinductive Herbrand model. We illustrate the approach by first specifying a standard type system for a small object-oriented language similar to Featherweight Java. Then we define an idealized type system for a variant of the language where type annotations can be omitted. The type system involves infinite terms and proof trees not representable in a finite way, thus providing a theoretical limit to type inference of object-oriented programs, since only sound approximations of the system can be implemented. Approximation is naturally captured by the notions of subtyping and subsumption; indeed, rather than increasing the expressive power of the system, as it usually happens, here subtyping is needed for approximating infinite non regular types and proof trees with regular ones.

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 present a simple parametric calculus of processes which exchange open mobile code, that is, code which may contain free variables to be bound by the receiver's code. Type safety is ensured by a combination of static and dynamic checks. That is, internal consistency of each process is statically verified, by relying on local type assumptions on missing code; then, when code is sent from a process to another, a runtime check based on a subtyping relation ensures that it can be successfully received, without requiring re-inspection of the code. In order to refuse communication in as few cases as possible, the runtime check accepts even mobile code which would be rejected if statically available, by automatically inserting coercions driven by the subtyping relation, as in the so-called Penn translation. The calculus is parametric in some ingredients which can vary depending on the specific language or system. Notably, we abstract away from the specific nature of the code to be exchanged, and of the static and dynamic checks. We formalize the notion of type safety in our general framework and provide sufficient conditions on the above ingredients which guarantee this property. We illustrate our approach on a simple lambda-calculus with records, where type safe exchange of mobile code is made problematic by conflicts due to components which were not explicitly required. In particular, we show that the standard coercion semantics given in the literature, with other aims, for this calculus, allows to detect and eliminate conflicts due to inner components, thus solving a problem which was left open in previous work on type-safe exchange of mobile code.

We present a translation from Fickle, a small object-oriented language allowing objects to change their class at runtime, into Java. The translation is provenly correct in the sense that it preserves the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected. In this article, we discuss four possible approaches we considered for the design of the translation and to justify our choice, we present formally the translation and proof of preservation of the static and dynamic semantics, and discuss the prototype implementation. Moreover, we outline an alternative translation based on generics that avoids most of the casts (but not all) needed in the previous translation. The language Fickle has undergone and is still undergoing several phases of development. In this article we are discussing the translation of FickleII.

In languages like C++, Java and C#, typechecking algorithms require methods to be annotated with their parameter and result types, which are either fixed or constrained by a bound. We show that, surprisingly enough, it is possible to infer the polymorphic type of a method where parameter and result types are left unspecified, as happens in most functional languages. These types intuitively capture the (less restrictive) requirements on arguments needed to safely apply the method. We formalize our ideas on a minimal Java subset, for which we define a type system with polymorphic types and prove its soundness. We then describe an algorithm for type inference and prove its soundness and completeness. A prototype implementing inference of polymorphic types is available.

We define a general framework for compositional compilation, meant as the ability of building an executable application by separate compilation and linking of single fragments, opposed to global compilation of the complete source application code. More precisely, compilation of a source code fragment in isolation generates a corresponding binary fragment equipped with type information, formally modeled as a typing, allowing type safe linking of fragments without re-inspecting code. We formally define a notion of soundness and completeness of compositional compilation w.r.t. global compilation, and show how linking can be in practice expressed by an entailment relation on typings. Then, we provide a sufficient condition on such entailment to ensure soundness and completeness of compositional compilation, and compare this condition with the principal typings property. Furthermore, we show that this entailment relation can often be modularly expressed by an entailment relation on type environments and a subtyping relation.

Although the C-based interpreter of Python is reasonably fast, implementations on the CLI or the JVM platforms offers some advantages in terms of robustness and interoperability. Unfortunately, because the CLI and JVM are primarily designed to execute statically typed, object-oriented languages, most dynamic language implementations cannot use the native bytecodes for common operations like method calls and exception handling; as a result, they are not able to take full advantage of the power offered by the CLI and JVM. We describe a different approach that attempts to preserve the flexibility of Python, while still allowing for efficient execution. This is achieved by limiting the use of the more dynamic features of Python to an initial, bootstrapping phase. This phase is used to construct a final RPython (Restricted Python) program that is actually executed. RPython is a proper subset of Python, is statically typed, and does not allow dynamic modification of class or method definitions; however, it can still take advantage of Python features such as mixins and first-class methods and classes. This paper presents an overview of RPython, including its design and its translation to both CLI and JVM bytecode. We show how the bootstrapping phase can be used to implement advanced features, like extensible classes and generative programming. We also discuss what work remains before RPython is truly ready for general use, and compare the performance of RPython with that of other approaches.

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 which 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 which can be instantiated on top of any Java-like language; a prototype implementation is available for a small Java subset. 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 present SmartJavaMod, a language of mixin modules supporting compositional compilation, and constructed on top of the Java language. More in detail, this means that basic modules are collections of Java classes which can be typechecked in isolation, inferring constraints on missing classes and allowing safe reuse of the module in as many contexts as possible. Furthermore, it is possible to write structured module expressions by means of a set of module operators, and a type system at the module level ensures type safety, in the sense that we can always reduce a module expression to a well-formed collection of Java classes. What we obtain is a module language which is extremely flexible and allows the encoding (without any need of enriching the core level, that is, the Java language) of a variety of constructs supporting software reuse and extensibility.

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

The notion of an intelligent agent as an entity which appears to be the subject of mental attitudes like beliefs, desires and intentions (hence, the BDI acronym) is well known and accepted by many researchers. Besides the definition of various BDI logics, many languages and integrated environments for programming BDI-style agents have been proposed since the early nineties. In this reasoned bibliography, nine languages and implemented systems, namely PRS, dMARS, JACK, JAM, Jadex, AgentSpeak(L), 3APL, Dribble, and Coo-BDI, are discussed and compared. References to other systems and languages based on the BDI model are also provided, as well as pointers to surveys dealing with related topics.

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

Dynamic rebinding is the ability of changing the definitions of names at execution time. While dynamic rebinding is clearly useful in practice, and increasingly needed in modern systems, most programming languages provide only limited and ad-hoc mechanisms, and no adequate semantic understanding currently exists. Here, we provide a simple and powerful mechanism for dynamic rebinding by means of a calculus of mixin modules (mutually recursive modules allowing redefinition of components) where, differently from the traditional approach, module operations can be performed after selecting and executing a module component: in this way, execution can refer to virtual components, which can be rebound when module operators are executed. In particular, in our calculus module operations are performed on demand, when execution would otherwise get stuck. We provide a sound type system, which ensures that execution never tries to access module components which cannot become available, and show how the calculus can be used to encode a variety of real-world dynamic rebinding mechanisms.

Mainstream research in Web Services is currently looking at two main aspects, namely formally describing interactions among services, and finding and combining services. Much work made in the intelligent agents area is being applied to these issues. In this paper, we investigate the application of agent research to Web Services from a different perspective, that is, procedural learning. The final objective is to enable an adaptive system (an agent in our terminology) to discover or being fed with knowledge concerning how to solve a specific set of problems in a specific software or physical environment. Our work is a very preliminary step into the issue, with the main objective of assessing how current Web Services technology can support a component, described in terms of beliefs, desires and intentions, dynamically adapting its behaviour to new environments.

The first part of the paper gives a brief overview of meta-programming, in particular program generation, and its use in software development. The second part introduces a basic calculus, related to FreshML, that supports program generation (as described through examples and a translation of MetaML into it) and programming in-the-large (this is demonstrated by a translation of CMS into it).

Building on our previous work, we present a simple module calculus where execution steps of a module component can be interleaved with reconfiguration steps (that is, reductions at the module level), and where execution can partly control precedence between these reconfiguration steps. This is achieved by means of a low priority link operator which is only performed when a certain component, which has not been linked yet, is both available and really needed for execution to proceed, otherwise precedence is given to the outer operators. We illustrate the expressive power of this mechanism by a number of examples. We ensure soundness by combining a static type system, which prevents errors in applying module operators, and a dynamic check which raises a linkage error if the running program needs a component which cannot be provided by reconfiguration steps. In particular no linkage errors can be raised if all components are potentially available.