Programming Languages
Rusty Variation (RV) is a library for session-typed communication in Rust which offers strong compile-time correctness guarantees. Programs written using RV are guaranteed to respect a specified protocol, and are guaranteed to be free from…
We study compliance relations between behavioural contracts in a syntax independent setting based on Labelled Transition Systems. We introduce a fix-point based family of compliance relations, and show that many compliance relations…
Programming-by-Example (PBE) systems synthesize an intended program in some (relatively constrained) domain-specific language from a small number of input-output examples provided by the user. In this paper, we motivate and define the…
The Scala programming language offers two distinctive language features implicit parameters and implicit conversions, often referred together as implicits. Announced without fanfare in 2004, implicits have quickly grown to become a widely…
Sharing confidential information in distributed systems is a necessity in many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which…
One form of type checking used in gradually typed language is transient type checking: whenever an object 'flows' through code with a type annotation, the object is dynamically checked to ensure it has the methods required by the…
We present the first formal semantics of Findel - a DSL for specifying financial derivatives. The semantics is encoded in Coq, and we use it to prove properties of several Findel contracts.
In modern runtime systems, memory layout calculations are hand-coded in systems languages. Primitives in these languages are not powerful enough to describe a rich set of layouts, leading to reliance on ad-hoc macros, numerous interrelated…
This volume contains the proceedings of ICE'19, the 12th Interaction and Concurrency Experience, which was held in Copenhagen, Denmark on the 20th and 21st of June 2019, as a satellite event of DisCoTec'19. The ICE workshop series features…
Probabilistic programming is a powerful abstraction for statistical machine learning. Applying static analysis methods to probabilistic programs could serve to optimize the learning process, automatically verify properties of models, and…
Haskell functions are defined as a series of clauses consisting of patterns that are matched against the arguments in the order of definition. In case an input is not matched by any of the clauses, an error occurs. Therefore it is desirable…
Most software factories contain applications with sensitive information that needs to be protected against breaches of confidentiality and integrity, which can have serious consequences. In the context of large factories with complex…
In this article we present a tool for the verification of programs built on top replicated databases. The tool evaluates a sequential specification and deduces which operations need to be synchronized for the program to function properly in…
Debugging is one of the most important and time consuming activities in software maintenance, yet mainstream debuggers are not well-adapted to several debugging scenarios. This has led to the research of new techniques covering specific…
Blockchain platforms are coming into broad use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, supporting smart contracts, which maintain persistent state and…
We consider the problem of data race prediction where the program's behavior is represented by a trace. A trace is a sequence of program events recorded during the execution of the program. We employ the schedulable happens-before relation…
In this report, we have explored the issues associated with the specification of event-based systems in a mobile environment using Unity \cite{unity}. We used a few constructs and concepts from Mobile UNITY which was proposed as an…
The R programming language combines a number of features considered hard to analyze and implement efficiently: dynamic typing, reflection, lazy evaluation, vectorized primitive types, first-class closures, and extensive use of native code.…
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 memory accesses and exception throwing. Here we present CallE, an…
During the past decade, differential privacy has become the gold standard for protecting the privacy of individuals. However, verifying that a particular program provides differential privacy often remains a manual task to be completed by…