We generalise a theory of multiparty session types for the π-calculus through asynchronous communication subtyping, which allows partial commutativity of actions with maximal fle...
Abstract. Structural subtyping is popular in research languages, but all mainstream object-oriented languages use nominal subtyping. Since languages with structural subtyping are n...
Tools for analysing secure information flow are almost exclusively based on ideas going back to Denning’s work from the 70’s. This approach embodies an imperfect notion of sec...
This paper explores the surprisingly rich design space for the simply typed lambda calculus with casts and a dynamic type. Such a calculus is the target intermediate language of th...
Just as some functions have uniform behavior over distinct types, other functions have uniform behavior over distinct arities. These variable-arity functions are widely used in scr...
T. Stephen Strickland, Sam Tobin-Hochstadt, Matthi...
Abstract. We present a separation logic framework which can express properties of memory separation between different points in a program. We describe an algorithm based on this fr...
Mohammad Raza, Cristiano Calcagno, Philippa Gardne...
Abstract. Multithreaded programs are prone to errors caused by unintended interference between concurrent threads. This paper focuses on verifying that deterministically-parallel c...
Caitlin Sadowski, Stephen N. Freund, Cormac Flanag...
Modern development environments support refactoring by providing atomically behaviour-preserving transformations. While useful, these transformations are limited in three ways: (i)...
Abstract. The global cumulative constraint was proposed for modelling cumulative resources in scheduling problems for finite domain (FD) propagation. Since that time a great deal ...
Andreas Schutt, Thibaut Feydy, Peter J. Stuckey, M...
We introduce Hegel and Fichte’s dialectic as a search meta-heuristic for constraint satisfaction and optimization. Dialectic is an appealing mental concept for local search as it...