We introduce the abstract notions of monadic operational semantics, a small-step semantics where computational effects are modularly modeled by a monad, and type-and-effect system, including effect types whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usual in the non-monadic case, we can express progress and subject reduction, and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects, equipped with an expressive type-and-effect system We provide proofs of progress and subject reduction, parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.

In recent work, non-periodic streams have been defined corecursively, by representing them with finitary equational systems built on top of various operators, besides the standard constructor. When only the stream constructor is allowed in equations, only periodic streams can be represented, and the structures of periodic streams and infinite regular trees are isomorphic. Therefore, one can use the theory of regular trees to get a sound and complete procedure to decide whether two equational systems are equivalent, that is, define the same streams. However, such an isomorphism no longer exists if one allows other operators in equations; in particular, there exist systems of equations which have the same unique solution as streams, but not as regular trees. Hence, equality of regular trees becomes stronger then equality of streams, with a negative impact on termination of functions whose definition is based on the equivalence of the representation of streams as finitary equational systems. To overcome this problem, we provide a weaker definition of equivalence, and prove its soundness and relative completeness. This definition is coinductive, hence non-algorithmic. However, we show that it can be turned into an equivalent inductive procedure.

Resource-aware type systems statically approximate not only the expected result type of a program, but also the way external resources are used, e.g., how many times the value of a variable is needed. We extend the type system of Featherweight Java to be resource-aware, parametrically on an arbitrary grade algebra modeling a specific usage of resources. We prove that this type system is sound with respect to a resource-aware version of reduction, that is, a well-typed program has a reduction sequence which does not get stuck due to resource consumption. Moreover, we show that the available grades can be heterogeneous, that is, obtained by combining grades of different kinds, via a minimal collection of homomorphisms from one kind to another. Finally, we show how grade algebras and homomorphisms can be specified as Java classes, so that grade annotations in types can be written in the language itself.

We extend the semantics and type system of a lambda calculus equipped with common constructs to be resource-aware . That is, reduction is instrumented to keep track of the usage of resources, and the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no needed resource gets exhausted. The resource-aware extension is parametric on an arbitrary grade algebra , and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.

We propose a Java-like calculus where declared variables can be annotated by coeffects specifying constraints on their use, e.g., affinity or privacy levels. Such coeffects are heterogeneous, in the sense that different kinds of coeffects can be used in the same program; combining coeffects of different kinds leads to the trivial coeffect. We prove subject reduction, which includes preservation of coeffects, and show several examples. In a Java-like language, coeffects can be expressed in the language itself, as expressions of user-defined classes.

In type-and-coeffect systems , contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bottom-up, combining, for each term, the coeffects of its subterms, through a fixed set of algebraic operators. We show that this principled approach can be adopted to track sharing in the imperative paradigm, that is, links among variables possibly introduced by the execution. This provides a significant example of non-structural coeffects, which cannot be computed by-variable, since the way a given variable is used can affect the coeffects of other variables. To illustrate the effectiveness of the approach, we enhance the type system tracking sharing to model a sophisticated set of features related to uniqueness and immutability. Thanks to the coeffect-based approach, we can express such features in a simple way and prove related properties with standard techniques.

We show that a minimal subset of Java 8 excluding classes supports a simple and natural programming style, which we call λ-based object-oriented programming. That is, on one hand the programmer can use tuples in place of objects (class instances), and tuples can be desugared to lambdas following their classical encoding in the λ-calculus. On the other hand, lambdas can be equipped with additional behaviour, thanks to the fact that they may implement interfaces with default methods, hence inheritance and dynamic dispatch are still supported. We formally describe the encoding by a translation from FJλ, an FJ variant including lambdas and interfaces with default methods, to FJλ-, a subset of FJλ with no classes (hence no constructors and fields). We provide several examples illustrating this novel programming style.

We provide an Agda library for inference systems, also supporting their recent generalization allowing flexible coinduction, that is, interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules, in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive intepretation and the corresponding proof principles. Moreover, a significant modularity is achieved. Indeed, rather than being defined from scratch and with a built-in interpretation, an inference system can also be obtained by composition operators, such as union and restriction to a smaller universe, and its semantics can be modularly chosen as well. In particular, flexible coinduction is obtained by composing in a certain way the interpretations of two inference systems. We illustrate the use of the library by several examples. The most significant one is a big-step semantics for the λ-calculus, where flexible coinduction allows to obtain a special result (∞) for all and only the diverging computations, and the proof of equivalence with small-step semantics is carried out by relying on the proof principles offered by the library.

The aim of the paper is to provide solid foundations for a programming paradigm natively supporting the creation and manipulation of cyclic data structures. To this end, we describe coFJ, a Java-like calculus where objects can be infinite and methods are equipped with a codefinition (an alternative body). We provide an abstract semantics of the calculus based on the framework of inference systems with corules. In coFJ with this semantics, FJ recursive methods on finite objects can be extended to infinite objects as well, and behave as desired by the programmer, by specifying a codefinition. We also describe an operational semantics which can be directly implemented in a programming language, and prove the soundness of such semantics with respect to the abstract one.

The known is finite, the unknown infinite - Thomas Henry Huxley The behaviour of programs can be described by the final results of computations, and/or their interactions with the context, also seen as observations. For instance, a function call can terminate and return a value, as well as have output effects during its execution. Here, we deal with semantic definitions covering both results and observations. Often, such definitions are provided for finite computations only. Notably, in big-step style, infinite computations are simply not modelled, hence diverging and stuck terms are not distinguished. This becomes even more unsatisfactory if we have observations, since a non-terminating program may have significant infinite behaviour. Recently, examples of big-step semantics modeling divergence have been provided [Davide Ancona et al., 2017; Davide Ancona et al., 2018] by means of generalized inference systems [Davide Ancona et al., 2017; Francesco Dagnino, 2019], which allow corules to control coinduction. Indeed, modeling infinite behaviour by a purely coinductive interpretation of big-step rules would lead to spurious results [Xavier Leroy and Hervé Grall, 2009] and undetermined observation, whereas, by adding appropriate corules, we can correctly get divergence (∞) as the only result, and a uniquely determined observation. This approach has been adopted in [Davide Ancona et al., 2017; Davide Ancona et al., 2018] to design big-step definitions including infinite behaviour for lambda-calculus and a simple imperative Java-like language. However, in such works the designer of the semantics is in charge of finding the appropriate corules, and this is a non-trivial task. In this paper, we show a general construction that extends a given big-step semantics, modeling finite computations, to include infinite behaviour as well, notably by generating appropriate corules. The construction consists of two steps: 1) Starting from a monoid O modeling finite observations (e.g., finite traces), we construct an ω-monoid ⟨O, O_∞⟩ also modeling infinite observations (e.g., infinite traces). The latter structure is a variation of the notion of ω-semigroup [Dominique Perrin and Jean-Eric Pin, 2004], including a mixed product composing a finite with a possibly infinite observation, and an infinite product mapping an infinite sequence of finite observations into a single one (possibly infinite). 2) Starting from an inference system defining a big-step judgment c⇒⟨r, o⟩, with c denoting a configuration, r ∈ R a result, and o ∈ O a finite observation, we construct an inference system with corules defining an extended big-step judgment c⇒c ⇒ ⟨r_∞, o_∞⟩ with r_∞ ∈ R_∞ = R+{∞}, and o_∞ ∈ O_∞ a "possibly infinite" observation. The construction generates additional rules for propagating divergence, and corules for introducing divergence in a controlled way. The exact corules added in the construction depend on the type of observations that one starts with. To show the effectiveness of our approach, we provide several instances of the framework, with different kinds of (finite) observations. Finally, we prove a correctness result for the construction. To this end, we assume the original big-step semantics to be equivalent to (finite sequences of steps in) a reference small-step semantics, and we show that, by applying the construction, we obtain an extended big-step semantics which is still equivalent to the small-step semantics, where we consider possibly infinite sequences of steps.} As hypotheses, rather than {just} equivalence in the finite case {(which would be not enough)}, we assume a set of equivalence conditions between individual big-step rules and the small-step relation. This proof of equivalence holds for deterministic semantics; issues arising in the non-deterministic case and a possible solution are sketched in the conclusion of the full paper.

We describe an inductive abstract semantics for coFJ, a Java-like calculus where, when the same method call is encountered twice, non-termination is avoided, and the programmer can decide the behaviour in this case, by writing a codefinition. The proposed semantics is abstract in the sense that evaluation is non-deterministic, and objects are possibly infinite. However, differently from typical coinductive handling of infinite values, the semantics is inductive, since it relies on detection of cyclic calls. Whereas soundness with respect to the reference coinductive semantics has already been proved, we conjecture that completeness with respect to the regular subset of such semantics holds as well. This relies on the fact that in the proposed semantics detection of cycles is non-deterministic, that is, does not necessarily happens the first time a cycle is found.

Abstract We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-terminating and stuck computations, hence soundness cannot even be expressed. The key idea is to define constructions yielding an extended version of a given arbitrary big-step semantics, where the difference is made explicit. The extended semantics are exploited in the meta-theory, notably they are necessary to show that the proof technique works. However, they remain transparent when using the proof technique, since it consists in checking three conditions on the original rules only, as we illustrate by several examples.

Abstract Recursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.

© 2018 Elsevier B.V. We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize, widely-used notions in literature, notably uniqueness and borrowing. Moreover, the calculus is pure in the sense that reduction is defined on language terms only, since they directly encode store. The advantage of this non-standard execution model with respect to a behaviorally equivalent standard model using a global auxiliary structure is that reachability relations among references are partly encoded by scoping.

Generalized inference systems have been recently introduced, and used, among other applications, to define semantic judgments which uniformly model terminating computations and divergence. We show that the approach can be successfully extended to more sophisticated notions of infinite behaviour, that is, to express that a diverging computation produces some possibly infinite result. This also provides a motivation to smoothly extend the theory of generalized inference systems to include, besides coaxioms, also corules, a more general notion for which significant examples were missing until now. We first illustrate the approach on a lambda-calculus with output effects, for which we also provide an alternative semantics based on standard notions, and a complete proof of the equivalence of the two semantics. Then, we consider a more involved example, that is, an imperative Java-like language with I/O primitives.

We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression. Sharing is directly represented at the syntactic level as a relation among free variables, thanks to the fact that the calculus is pure. That is, imperative features are modeled by just rewriting source code terms. We consider both standard variables and affine variables, which can occur at most once in their scope. The latter are used as temporary references, to "move" a capsule (an isolated portion of store) to another location in the store. The sharing effects inferred by the type system are very expressive, and generalize notions introduced in literature by type modifiers.

We extend the simply-typed lambda-calculus with a mechanism for dynamic and incremental rebinding of code. Fragments of open code which can be dynamically rebound are values. Differently from standard static binding, which is done on a positional basis, rebinding is done on a nominal basis, that is, free variables in open code are associated with names which do not obey α-equivalence. Moreover, rebinding is incremental, that is, just a subset of names can be rebound, making possible code specialization, and rebinding can even introduce new names. Finally, rebindings, which are associations between names and terms, are first-class values, and can be manipulated by operators such as overriding and renaming. We define a type system in which the type for a rebinding, in addition to specify an association between names and types (similarly to record types), is also annotated. The annotation says whether or not the domain of the rebinding having this type may contain more names than the ones that are specified in the type. We show soundness of the type system.

Coaxioms have been recently introduced to enhance the expressive power of inference systems, by supporting interpretations which are neither purely inductive, nor coinductive. This paper proposes a novel approach based on coaxioms to capture divergence in semantic definitions by allowing inductive and coinductive semantic rules to be merged together for defining a unique semantic judgment. In particular, coinduction is used to derive a special result which models divergence. In this way, divergent, terminating, and stuck computations can be properly distinguished even in semantic definitions where this is typically difficult, as in big-step style. We show how the proposed approach can be applied to several languages; in particular, we first illustrate it on the paradigmatic example of the λ-calculus, then show how it can be adopted for defining the big-step semantics of a simple imperative Java-like language. We provide proof techniques to show classical results, including equivalence with small-step semantics, and type soundness for typed versions of both languages.

In previous work we have presented coFJ, an extension to Featherweight Java that promotes coinductive programming, a sub-paradigm expressly devised to ease high-level programming and reasoning with cyclic data structures.

We present a new Java-like language design coupling disciplined meta-programming features with a composition language. That is, programmers can write meta expressions that combine class definitions, on top of a small set of composition operators, inspired by the seminal Bracha's Jigsaw framework. Moreover, such operators are deep, that is, they allow manipulation (e.g., renaming or duplication) of a nested class at any level of depth.

Despite cyclic data structures occur often in many application domains, object-oriented programming languages provide poor abstraction mechanisms for dealing with cyclic objects.

We propose a Java-like language where class definitions are first class values and new classes can be derived from existing ones by exploiting the full power of the language itself, used on top of a small set of primitive composition operators, instead of using a fixed mechanism like inheritance.Hence, compilation requires to perform (meta-)reduction steps, by a process that we call compile-time execution. This approach differs from meta-programming techniques available in mainstream languages since it is meta-circular, hence programmers are not required to learn new syntax and idioms.Compile-time execution is guaranteed to be sound (not to get stuck) by a lightweight technique, where class composition errors are detected dynamically, and conventional typing errors are detected by interleaving typechecking with meta-reduction steps. This allows for a modular approach, that is, compile-time execution is defined, and can be implemented, on top of typechecking and execution of the underlying language. Moreover, programmers can handle errors due to composition operators.Besides soundness, our technique ensures an additional important property called meta-level soundness, that is, typing errors never originate from (meta-)code in already compiled programs.

We present a simple module calculus where selection and execution of a component is possible onopenmodules, that is, modules that still need to import some external definitions. Hence, it provides a kernel model for a computational paradigm in which standard execution (that is, execution of a single computation described by a fragment of code) can be interleaved with operations at the meta-level, which can manipulate in various ways the context in which this computation takes place. Formally, this is achieved by introducingconfigurationsas basic terms. These are, roughly speaking, pairs consisting of an (open, mutually recursive) collection of named components and a term representing a program running in the context of these components. Configurations can be manipulated by classical module/fragment operators, hence reduction steps can be either execution steps of the program or steps that perform module operations (calledreconfigurationsteps). Since configurations combine the features of lambda abstractions (first-class functions), records, environments with mutually recursive definitions and modules, the calculus extends and integrates both traditional module calculi and recursive lambda calculi. We state confluence of the calculus, and propose different ways to prevent errors arising from the lack of some required component, either by a purely static type system or by a combination of static and run-time checks. Moreover, we define a call-by-need strategy that performs module simplificationonly when needed and only once, leading to a generalisation of call-by-need lambda calculi that includes module features. We prove the soundness and completeness of this strategy using an approach based on information content, which also allows us to preserve confluence, even when local substitution rules are added to the calculus.

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

We define compositional compilation as the ability to typecheck source code fragments in isolation, generate 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 would have been produced by standard compilation of all fragments).

The contribution of the paper is twofold. First, we define a general notion of type system equipped with an entailment relation between type environments; this generalisation serves as a pattern for instantiating type systems able to support separate compilation and inter-checking of Java-like languages, and allows a formal definition of soundess and completeness of inter-checking w.r.t. global compilation. These properties are important in practice since they allow selective recompilation. In particular, we show that they are guaranteed when the type system has principal typings and provides sound and complete entailment relation between type environments.The second contribution is more specific, and is an instantiation of the notion of type system previously defined for Featherweight Java with method overloading and field hiding. The aim is to show that it is possible to define type systems for Java-like languages, which, in contrast to those used by standard compilers, have principal typings, hence can be used as a basis for selective recompilation.

In this paper we present Jam, an extension of the Java language supporting mixins , that is, parametric heir classes. A mixin declaration in Jam is similar to a Java heir class declaration, except that it does not extend a fixed parent class, but simply specifies the set of fields and methods a generic parent should provide. In this way, the same mixin can be instantiated on many parent classes, producing different heirs, thus avoiding code duplication and largely improving modularity and reuse. Moreover, as happens for classes and interfaces, mixin names are reference types, and all the classes obtained by instantiating the same mixin are considered subtypes of the corresponding type, and hence can be handled in a uniform way through the common interface. This possibility allows a programming style where different ingredients are "mixed" together in defining a class; this paradigm is somewhat similar to that based on multiple inheritance, but avoids its complication.The language has been designed with the main objective in mind to obtain, rather than a new theoretical language, a working and smooth extension of Java. That means, on the design side, that we have faced the challenging problem of integrating the Java overall principles and complex type system with this new notion; on the implementation side, it means that we have developed a Jam-to-Java translator which makes Jam sources executable on every Java Virtual Machine.

We define a type system modeling true separate compilation for a small but significant Java subset, in the sense that a single class declaration can be intra-checked (following the Cardelli's terminology) and compiled providing a minimal set of type requirements on missing classes. These requirements are specified by a local type environment associated with each single class, while in the existing formal definitions of the Java type system classes are typed in a global type environment containing all the type information on a closed program. We also provide formal rules for static interchecking and relate our approach with compilation of closed programs, by proving that we get the same results.

We present CMS , a simple and powerful calculus of modules supporting mutual recursion and higher order features, which can be instantiated over an arbitrary core calculus satisfying standard assumptions. The calculus allows expression of a large variety of existing mechanisms for combining software components, including parameterized modules similar to ML functors, extension with overriding as in object-oriented programming, mixin modules and extra-linguistic mechanisms like those provided by a linker. Hence CMS can be used as a paradigmatic calculus for modular languages, in the same spirit the lambda calculus is used for functional programming. We first present an untyped version of the calculus and then a type system; we prove confluence, progress, and subject reduction properties. Then, we define a derived calculus of mixin modules directly in terms of CMS and show how to encode other primitive calculi into CMS (the lambda calculus and the Abadi-Cardelli object calculus). Finally, we consider the problem of introducing a subtype relation for module types.

Mixins are modules that may contain deferred components, that is, components not defined in the module itself; moreover, in contrast to parameterised modules (like ML functors), they can be mutually dependent and allow their definitions to be overridden. In a preceding paper we defined a syntax and denotational semantics of a kernel language of mixin modules. Here, we take instead an axiomatic approach, giving a set of algebraic laws expressing the expected properties of a small set of primitive operators on mixins. Interpreting axioms as rewriting rules, we get a reduction semantics for the language and prove the existence of normal forms. Moreover, we show that the model defined in the earlier paper satisfies the given axiomatisation.

In this paper we present a simple calculus (called CJE) in ourder to fully investigate the exception mechanism of Java, and in particular its interaction with inheritance, which turns out to be non trivial. Moreover, we show that the type system for the calculus directly dirven by the Java language specification (called FULL) uses too many types, in the sense that there are different types which rpovide exactly the same information. Hence, we obtain from FULL a simplified type system called MIN where equivalent types have been identified. We show that is useful both for type-checking optimization and for clarifying the static semantics of the language. The two type systems are proved to satisfy the subject reduction property

Abstract. We claim that a continuation style semantics of a programming language can provide a starting point for constructing its proof system. The basic idea is to see weakest preconditions as a particular instance of continuation style semantics, hence to interpret correctness assertions (e.g. Hoare triples { p } C { r }) as inequalities over continuations. This approach also shows a correspondence between labels in a program and annotations.

Abstract This paper presents an algebraic semantics schema for object oriented languages including concurrent features. A class, the basic syntactic unit of an object oriented language, in our approach denotes a set of algebras determined by an algebraic specification. This specification describes a system of (possibly active) objects interacting via method calls. Extending other approaches, structured classes are modelled in a fully compositional way. This means that the semantic counterpart of class combinators such as inheritance and clientship are specification combinators. A model of records with sharing allows us to describe typical object oriented features like object sharing, inheritance polymorphism and dynamic binding. For modelling the dynamic behaviour of objects, we rely on an algebraic description of labelled transition systems.

We propose a semantic framework for dynamic systems, which, in a sense, extends the well-known algebraic approach for modelling static data structures to the dynamic case. The framework is based on a new mathematical structure, called a d-oid, consisting of a set of instant structures and a set of dynamic operations. An instant structure is a static structure, e.g. an algebra; a dynamic operation is a transformation of instant structures with an associated point to point map, which allows us to keep track of the transformations of single objects and thus is called a tracking map. By an appropriate notion of morphism, the d-oids over a dynamic signature constitute a category. It is shown that d-oids can model object systems and support an abstract notion of possibly unique object identity; moreover, for a d-oid satisfying an identity preserving condition, there exists an essentially equivalent d-oid where the elements of instant structures are just names.