Programming Languages

Robotics is incredibly fun and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic…

Writing concurrent programs is highly error-prone due to the nondeterminism in interprocess communication. The most reliable indicators of errors in concurrency are data races, which are accesses to a shared resource that can be executed…

We present a domain-specific language called SAL(the Streaming Analytics Language) for processing data in a semi-streaming model. In particular we examine the use case of processing netflow data in order to identify malicious actors within…

In the Calculus of Dependent Lambda Eliminations (CDLE), a pure Curry-style type theory, it is possible to generically {\lambda}-encode inductive datatypes which support course-of-values (CoV) induction. We present a datatype subsystem for…

Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic…

We describe the LoopInvGen tool for generating loop invariants that can provably guarantee correctness of a program with respect to a given specification. LoopInvGen is an efficient implementation of the inference technique originally…

Liquid typing provides a decidable refinement inference mechanism that is convenient but subject to two major issues: (1) inference is global and requires top-level annotations, making it unsuitable for inference of modular code components…

Event-driven programming is widely used for implementing user interfaces, web applications, and non-blocking I/O. An event-driven program is organized as a collection of event handlers whose execution is triggered by events. Traditional…

We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and relations it uses are assumed to interpreted by arbitrary…

Hybrid systems are dynamical systems with continuous evolution of states and discrete evolution of states and governing equations. We have worked on the design and implementation of HydLa, a constraint-based modeling language for hybrid…

In this paper we propose a calculus for expressing algorithms for programming languages transformations. We present the type system and operational semantics of the calculus, and we prove that it is type sound. We have implemented our…

Lambda lifting is a well-known transformation, traditionally employed for compiling functional programs to supercombinators. However, more recent abstract machines for functional languages like OCaml and Haskell tend to do closure…

Happens-before based data race prediction methods infer from a trace of events a partial order to check if one event happens before another event. If two two write events are unordered, they are in a race. We observe that common tracing…

Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult…

The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected…

Choreography extraction deals with the generation of a choreography (a global description of communication behaviour) from a set of local process behaviours. In this work, we implement a previously proposed theory for extraction and show…

If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and…

Traversals are commonly seen in tree data structures, and performance-enhancing transformations between tree traversals are critical for many applications. Existing approaches to reasoning about tree traversals and their transformations are…

Bidirectional transformation, also called lens, has played important roles in maintaining consistency in many fields of applications. A lens is specified by a pair of forward and backward functions which relate to each other in a consistent…

WebAssembly (Wasm) is a next-generation portable compilation target for deploying applications written in high-level languages on the web. In order to protect their memory from untrusted code, web browser engines confine the execution of…