Scottish Programming Languages Seminar

Abstract

Hide Abstract

Many programs process secret data. In fact, they often need to reveal some amount of secret data. What declassification allows a programmer to specify what data they are willing to reveal. In this work in progress, we use dependency tracking to reason about what declassification in the higher-order setting. We present a novel dependency-tracking type system tracking dependencies of expressions on other expressions in their type and a novel compositional semantics interpreting those types to give what-declassification guarantees. The heart of our type system, the „trivial rule“, says that an expression’s dependency can always be replaced with the most precise dependency: the expression itself.

Abstract

Hide Abstract

Effect handlers generalise exception handlers, but allow resumption of the continuation from where the effect was raised. Allowing continuations to be resumed at most once (one-shot) or an arbitrary number of times (multi-shot) has far-reaching consequences. In addition to performance considerations, multi-shot effects break key rules of reasoning and thus render certain standard transformation/optimizations unsound, especially in languages with mutable references (such as OCaml 5). It is therefore desirable to statically track whether continuations are used in a one-shot or multi-shot discipline, so that a compiler could use this information to efficiently implement effect handlers and to determine what optimizations it may perform.

We address this problem by developing a type and effect system — called Affect — which uses affine types to track the usage of continuations. To prove soundness of Affect we model types and judgements semantically via a logical relation in the Iris separation logic framework in Rocq.

Abstract

Hide Abstract

Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. We explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We find that replication is not an equivalent alternative to recursion in MPST, and using both constructs in one type system in fact allows us to express both context-free protocols and protocols that make interesting use of mutual exclusion and races. In this talk, we will demonstrate the expressiveness of replication in MPST by example, observe the mutual non-inclusion result, and discuss the decidability of typechecking.

Abstract

Hide Abstract

Multiparty Session Types (MPST) offer a robust framework to ensure indispensable properties in distributed systems. However, their adoption in industry remains limited. Our work aims to facilitate industrial adoption by developing a toolchain that improves the usability and accessibility of MPST for industry use. This effort is guided by examples from Paxos — a fault-tolerant consensus algorithm known for its complexity, stemming from intricate message exchanges that are both challenging to understand and implement correctly.

In this talk, we extend previous work that models crash-stop processes and failure recovery via crash branches. Specifically, we present different ways and their challenges to semi-automatic refactoring of global protocols to facilitate crash branches introduction. Additionally, we introduce a fine-grained method to simulate crashed links using default communications, helping to prolong the session's lifespan. Finally, we extend both the Scribble language and Effpi, an MPST-based concurrency library for Scala, with syntactic sugar to enhance the modularity of MPST.

Abstract

Hide Abstract

Interest in metaprogramming, reflection, and compile-time evaluation continues to inspire and foster innovation among the users and designers of the C++ programming language. Regrettably, the impact on compile-times of such features can be significant; and outside of build systems, multi-core parallelism is unable to bring down compilation times of individual translation units. We present ClangOz, a novel Clang-based research compiler that addresses this issue by evaluating annotated constant expressions in parallel, thereby reducing compilation times.

Abstract

Hide Abstract

Esoteric programming languages are fun to learn, and their unusual features and constraints can improve programming ability. From languages designed to be intentionally obtuse (e.g. INTERCAL) to others targeting artistic expression (e.g. Piet) or philosophical exploration (e.g. Chef), this talk examines how esoteric languages push the boundaries of software development.

My key thesis is that esoteric languages can improve general PL awareness, as well as enabling the esoteric programmer to impress their peers with obscure knowledge. We will explore why people are attracted to esoteric languages in terms of (a) program comprehension and coding, as well as (b) language design and implementation.