Security-critical software applications contain confidential information which has to be protected from leaking to unauthorized systems. With language-based techniques, the confidentiality of applications can be enforced. Such techniques are for example type systems that enforce an information flow policy through typing rules. The precision of such type systems, especially in object-oriented languages, is an area of active research: an appropriate system should not reject too many secure programs while soundly preserving noninterference. In this work, we introduce the language SIFO which supports information flow control for an object-oriented language with type modifiers. Type modifiers increase the precision of the type system by utilizing immutability and uniqueness properties of objects for the detection of information leaks. We present SIFO informally by using examples to demonstrate the applicability of the language, formalize the type system, prove noninterference, implement SIFO as a pluggable type system in the programming language L42, and evaluate it with a feasibility study and a benchmark.

Functional Reactive Programming (FRP) is a powerful abstraction for building deterministic concurrent systems. However, some programmers prefer a more imperative approach for certain tasks, and that approach is required to implement some imperative algorithms. The Actor Model provides an abstraction for building concurrent systems in a more imperative way without as much of the chaos typical of traditional shared-memory imperative concurrent programming. While the Actor Model offers more structure than other imperative approaches, it still suffers from nondeterminism due to message-ordering and processing times. That makes actor systems hard to reason about, limiting their effectiveness for critical tasks. We formally define an elegant multi-paradigm unification of event-driven FRP constructs and the Actor Model. Our unification enables an intuitive form of declarative programming that can integrate imperative and declarative code within each other. We use reference and object capabilities to tame imperative features: reference capabilities track aliasing and mutability, and object capabilities track I/O. Notably, in our system expressions with deeply immutable input behave deterministically. Additionally, capabilities provide a boundary to allow nondeterministic code to intermingle safely with deterministic code.

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.

In this paper we use pre-existing language support for both reference and object capabilities to enable sound runtime verification of representation invariants. Our invariant protocol is stricter than the other protocols, since it guarantees that invariants hold for all objects involved in execution. Any language already offering appropriate support for reference and object capabilities can support our invariant protocol with minimal added complexity. In our protocol, invariants are simply specified as methods whose execution is statically guaranteed to be deterministic and to not access any externally mutable state. We formalise our approach and prove that our protocol is sound, in the context of a language supporting mutation, dynamic dispatch, exceptions, and non-deterministic I/O. We present case studies showing that our system requires a lighter annotation burden compared to Spec#, and performs orders of magnitude less runtime invariant checks compared to the ‘visible state semantics’ protocols of D and Eiffel.

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.

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

Multiple inheritance is a valuable feature for Object-Oriented Programming. However, it is also tricky to get right, as illustrated by the extensive literature on the topic. A key issue is the ambiguity arising from inheriting multiple parents, which can have conflicting methods. Numerous existing work provides solutions for conflicts which arise from diamond inheritance: i.e. conflicts that arise from implementations sharing a common ancestor. However, most mechanisms are inadequate to deal with unintentional method conflicts: conflicts which arise from two unrelated methods that happen to share the same name and signature. This paper presents a new model called Featherweight Hierarchical Java (FHJ) that deals with unintentional method conflicts. In our new model, which is partly inspired by C++, conflicting methods arising from unrelated methods can coexist in the same class, and hierarchical dispatching supports unambiguous lookups in the presence of such conflicting methods. To avoid ambiguity, hierarchical information is employed in method dispatching, which uses a combination of static and dynamic type information to choose the implementation of a method at run-time. Furthermore, unlike all existing inheritance models, our model supports hierarchical method overriding: that is, methods can be independently overridden along the multiple inheritance hierarchy. We give illustrative examples of our language and features and formalize FHJ as a minimal Featherweight-Java style calculus.

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.

This paper presents an OO style without classes, which we call interface-based object-oriented programming (IB). IB is a natural extension of closely related ideas such as traits. Abstract state operations provide a new way to deal with state, which allows for flexibility not available in class-based languages. In IB state can be type-refined in subtypes. The combination of a purely IB style and type-refinement enables powerful idioms using multiple inheritance and state. To introduce IB to programmers we created Classless Java: an embedding of IB directly into Java. Classless Java uses annotation processing for code generation and relies on new features of Java 8 for interfaces. The code generation techniques used in Classless Java have interesting properties, including guarantees that the generated code is type-safe and good integration with IDEs. Usefulness of IB and Classless Java is shown with examples and case studies.

Traditionally, formal semantic models of Java-like languages use an explicit model of the store which mimics pointers and ram. These low level models hamper understanding of the semantics, and development of proofs about ownerships and other encapsulation properties, since the real (graph) structure of the data is obscured by the encoding. Such models are also inadequate for didactic purposes since they rely on run-time structures that do not exist in the source program --- in order to understand the meaning of an expression in the middle of the execution one is required to visualize the memory structure which is hard to relate to the abstract program state.

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.

"Exception-safety strong guarantee: The operation has either completed successfully or thrown an exception, leaving the program state exactly as it was before the operation started." David Abrahams [1] The above definition of strong exception-safety comes from the world of C++, but it can be applied to any language.

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.