The Theory of Call-by-Value Solvability The denotational semantics of the untyped $\lambda$-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus is instead still in its […]

High-Level Type-Safe Effect Handlers in C++ DAN GHICA, Huawei Research, UK SAM LINDLEY, The University of Edinburgh, UK MARCOS MAROÑAS BRAVO, Huawei Research, UK MACIEJ PIRÓG, Huawei Research, UK Effect handlers allow the programmer to implement computational effects, such as custom error handling, various forms of lightweight concurrency, and dynamic binding, inside the programming language. […]

Making Concurrency Functional by Glynn Winskel   http://arxiv.org/abs/2202.13910   The article bridges between two major paradigms in computation, the functional, at basis computation from input to output, and the interactive, where computation reacts to its environment while underway.  Central to  any compositional theory of interaction is the dichotomy between a system and its environment.  Concurrent […]

James Wood and Robert Atkey. A Framework for Substructural Type Systems. ESOP 2022, to appear. 2022. [BIB] [PDF] Abstract Mechanisation of programming language research is of growing interest, and the act of mechanising type systems and their metatheory is generally becoming easier as new techniques are invented. However, state-of-the-art techniques mostly rely on structurality of the type system — […]

ath.CT String diagrams for non-strict monoidal categories Authors: Paul Wilson, Dan R. Ghica, Fabio Zanasi Abstract: Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string […]

Effect handlers allow for programming with user-defined computational effects, with applications including custom lightweight concurrency (threads, async-await, actors, generators), error handling, dependency injection, etc. Effect handlers originate from the realm of functional programming, and the main goal of this highly experimental library is to explore how they fit in the more object-oriented setting of C++. The library relies […]

OpenMP Taskloop Dependences Authors   Marcos Maroñas Bravo (Huawei Edinburgh RC, Programming Languages team) Xavier Teruel Vicenç Beltran Abstract Exascale systems will contain multicore/manycore processors with high core count in each node. Therefore, using a model that relaxes the synchronization, such as data-flow, is crucial to adequately exploit the potential of the hardware. The flexibility of the […]