3 citations · 5 across the 11 of their papers we have counts for
11 papers
The Fearless Journey [Draft]
Nick Webster, Marco Servetto, Michael Homer
Existing minimal Object-Oriented models (OO), like Featherweight Java (FJ), are valuable for modelling programs and designing new programming languages and tools. However, their ut…
Coeffects for Sharing and Mutation
Riccardo Bianchini, Francesco Dagnino, Paola Giannini +2
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 bott…
Information Flow Control-by-Construction for an Object-Oriented Language Using Type Modifiers
Tobias Runge, Alexander Kittelmann, Marco Servetto +2
In security-critical software applications, confidential information must be prevented from leaking to unauthorized sinks. Static analysis techniques are widespread to enforce a se…
Mμl: The Power of Dynamic Multi-Methods
Isaac Oscar Gariano, Marco Servetto
Multi-methods are a straightforward extension of traditional (single) dynamic dispatch, which is the core of most object oriented languages. With multi-methods, a method call will…
CallE: An Effect System for Method Calls
Isaac Oscar Gariano, James Noble, Marco Servetto
Effect systems are used to statically reason about the effects an expression may have when evaluated. In the literature, such effects include various behaviours as diverse as memor…
A Syntactic Model of Mutation and Aliasing
Paola Giannini, Marco Servetto, Elena Zucca
Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownership and other encapsulation properties need to be reconstr…
Sound Invariant Checking Using Type Modifiers and Object Capabilities
Isaac Oscar Gariano, Marco Servetto, Alex Potanin
In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees…
Iteratively Composing Statically Verified Traits
Isaac Oscar Gariano, Marco Servetto, Alex Potanin +1
Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static ver…
Separating Use and Reuse to Improve Both
Hrshikesh Arora, Marco Servetto, Bruno C. D. S. Oliveira
Context: Trait composition has inspired new research in the area of code reuse for object oriented (OO) languages. One of the main advantages of this kind of composition is that it…
Flexible recovery of uniqueness and immutability (Extended Version)
Paola Giannini, Marco Servetto, Elena Zucca +1
We present an imperative object calculus where types are annotated with qualifiers for aliasing and mutation control. There are two key novelties with respect to similar proposals.…
Tracing sharing in an imperative pure calculus (Extended Version)
Paola Giannini, Tim Richter, Marco Servetto +1
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 equivalen…