NIETS

Venue: 1 West

The Department of Computer Science is in the building 1 West, next to the big glass library in the middle of the Parade (the central walkway on campus). We have room 2.101 for talks and 2.102 as a breakout room, except for the last session on Thursday when talks will be in 2.102 instead. If the rooms 2.103 and 2.104 are free, you can use those as well.

Workshop Dinner: Roman Baths

The dinner will be in the Roman Baths, on the terrace overlooking the baths themselves. The picture shows the wrong entry, on Stall Street. Doors open at 7pm and we will be seated at 7.30. Here is the seating plan, and I will bring a printout of everyone's menu choices. There will be water on the table and you can ask for wine, beer, cider, and soda. The dinner ends at 9.30.

Tour: The Bad of Bath

The tour will be The Bad of Bath walking tour. Since tours are limited to 15 people, we will go in two shifts, Tuesday and Wednesday, as indicated in this tour plan. Straight after the last talk, someone from Bath will take the group on the bus to meet Simon, our guide, in front of Bath Abbey just after 5pm (First Bus willing). The Wednesday tour will drop you off in front of the Roman Baths for the workshop dinner.

Alessio Santamaria

Tape diagrams for rig categories with finite biproducts

Rig categories with finite biproducts are categories with two monoidal products, where one is a biproduct and the other distributes over it. In this talk we present tape diagrams, a sound and complete diagrammatic language for rig categories with finite biproducts, which can be thought intuitively as string diagrams of string diagrams.

Alex Kavvos

Concurrent Classical Effects

We add something akin to an effect-and-handler mechanism to Classical Linear Logic. Under Curry-Howard this corresponds to a system of session types and effects.

Chris Barrett

Categorical Semantics of the Functional Machine Calculus

The Functional Machine Calculus (FMC) is a lambda-calculus variant, based on a simple stack machine intuition, incorporating reader/writer effects. These are decomposed into the basic syntax such that beta-reduction implements their expected operational semantics, allowing the preservation of confluence. Simple types are available for the FMC which record all input/output information, including all changes to state, consumption from oracles, etc. Simple types constitute a very strong type system for effects, which restores referential transparency, confers strong normalisation and, remarkably, Cartesian closure.

I will investigate the categorical semantics of the FMC, showing how an appropriate equational theory recovers the free Cartesian closed category, with similar results for first-order and linear fragments of the FMC. We show that the equational theory is supported by a natural contextual equivalence induced by the stack machine. If there is time, I will then discuss links to (closed) Freyd categories, which have previously been given as a categorical semantics of computational effects. As corollaries, I show how the FMC gives a natural term language for (and computational interpretation of) string diagrams.

David Sherratt

Spinal atomic lambda-calculus

Giulio Manzonetto

Profunctors - what are they useful for?

Relational models of 𝜆-calculus can be presented as type systems, and the relational interpretation of a 𝜆-term as the set of its typings. We introduce a bicategorical model living in a distributors-induced semantics generalising the relational one, and show that it satisfies an Approximation Theorem. As in the relational case, the quantitative nature of our bicategory allows to prove this property via a simple induction, rather than using computability predicates. Unlike relational models, our bicategorical model is also proof-relevant in the sense that the interpretation of a 𝜆-term does not contain its typings, but the whole type derivations. The additional information carried by a type derivation allows to reconstruct an approximant having the same type in the same environment. From this, we obtain the characterisation of the theory induced by the bicategorical model as a corollary of the Approximation Theorem: two 𝜆-terms share the same interpretation exactly when their Böhm trees coincide.

Giulio Guerrieri

Decomposing Probabilistic Lambda-Calculi

Joint work with Ugo Dal Lago and Willem Heijltjes (FoSSaCS 2020)

A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.

Guy McCusker

Domain-theoretic semantics of the Functional Machine Calculus

The Functional Machine Calculus is a programming language in which higher-order functions and reader/writer-style computational effects are expressed with the same syntactic constructs: push and pop operations for a collection of stacks. In this talk I will show that this calculus arises naturally from a domain-theoretic semantics of lambda-calculus with effects, extending Streicher and Reus's observation that Krivine's abstract machine corresponds to Scott's D-infinity models.

Streicher and Reus observed that Scott's domain equation for models of the lambda-calculus can be understood as a continuations model in which programs manipulate stacks of terms. Amending the domain equation to incorporate simple computational effects, we discover first that the domains support the operation of sequencing from the Functional Machine Calculus, and then that effectful programs can be seen as manipulating multiple stacks as in the FMC. We arrive at a domain-theoretic model for the untyped FMC and obtain a computational adequacy theorem for this semantics in a standard manner. The model also provides an explanation for the FMC's type system, in which types are interpreted as retracts of the domain.

Ian Mackie

Functional programming with interaction nets

Matteo Acclavio

Graphical Proof Theory

Graphs are often used in mathematics and computer science to represent systems with complex interactions. However, few proof theoretical tools have been conceived to treat graphs as first class terms of the language, and most of these tools limit the language to specific classes of graphs with a simple topological structure.

In this talk we discuss a line of work designing proof systems operating on general graphs. We present the current results on the topic and we explain how the standard proof theoretical techniques have been adapted and extended to deal with this more expressive language. We conclude by discussing related works and outlining the future research directions.

Melissa Antonelli

On Counting Logics and Randomized Computation

Interactions between logic and theoretical computer science have been deeply investigated in the realm of deterministic computation, but, strikingly, when switching to the probabilistic framework the literature seems to not offer much. I present a joint work with U. Dal Lago and P. Pistone the aim of which is precisely to start bridging this gap by developing inherently quantitative logics and investigating their relations with specific aspects of probabilistic models.

The presentation is conceived as an overview of our study and is bipartite. In the first part, I introduce counting propositional logics, obtained by endowing standard propositional systems with counting quantifiers, which basically "counts" the probability of the (argument) formula. Remarkably, classical counting logic is linked to computational complexity as characterizing the full counting hierarchy, while the intuitionistic fragment provides the counterpart for the first probabilistic Curry-Howard correspondence.

In the second part of the talk, I introduce a more expressive language, which is defined by extending that of PA with measure quantifiers, and briefly consider its connections with probabilistic computations (e.g. the "randomized arithmetization" result). This language is also the starting point of our ongoing study, conducted together with I. Oitavem and D. Davoli, aiming at developing randomized bounded theories to logically characterize probabilistic complexity classes, as BPP.

Paul Levy

Numbered recursion: operational and denotational semantics

Numbered recursion is the practice of annotating each recursive call or type definition with a (finite or infinite) maximum number of unwindings. Although formally equivalent to ordinary recursion, it is useful for giving easy proofs of syntactic continuity and computational adequacy in a continuous setting.

In this talk, we’ll explore numbered recursion firstly in PCF (call-by-name typed lambda-calculus with term recursion), then in call-by-push-value with term recursion. Lastly we include type recursion, using a form of denotational semantics that avoids the need to separate positive and negative occurrences of type variables.

At each stage, we’ll see two kinds of operational semantics: “unwinding” evaluation is deterministic and partial, whereas “decreasing” evaluation is nondeterministic and total, and allows us to prove adequacy by a simple induction. The relationship between them is the centrepiece of the story.

Paolo Pistone

Curry and Howard Meet Borel

Joint work with Melissa Antonelli and Ugo Dal Lago

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but rather reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by extending the type system with intersection types.

Pierre Clairambault

The Geometry of Causality : Multi-token GoI and its Causal Unfolding

Joint work with Simon Castellan

In this talk, I will introduce a multi-token machine for Idealized Parallel Algol (IPA), a higher-order concurrent programming language with shared state and semaphores. For the purely functional fragment, the machine is conceptually close to Geometry of Interaction token machines, originating from Linear Logic and presenting higher-order computation as the low-level process of a token walking through a graph (a proof net) representing the term. However, our methodology is somewhat different: instead of representing terms as proof nets, the machine takes the shape of a compositional interpretation of terms as "Petri structures", certain coloured Petri nets. Formalizing the token machine as a Petri net allows us to pair GoI with folklore ideas on the representation of first-order imperative concurrent programs as coloured Petri nets.

To prove our machine correct, we follow game semantics and represent types as certain games specifying dependencies and conflict between computational events. We define Petri strategies as those Petri structures obeying the rules of the game. In turn, we show how Petri strategies unfold to concurrent strategies in the sense of concurrent games on event structures. This not only entails correctness and adequacy of our machine, but also lets us generate operationally a causal description of the behaviour of programs at higher-order types.

The Geometry of Causality machine is implemented, and available at: https://ipatopetrinets.github.io/

Sam Staton

Stochastic Memoization

Ugo Dal Lago

On Bounded Arithmetic and Probabilistic Complexity Classes

Victor Arrial

Quantitative Inhabitation in Call-by-Push-Value

Joint work with Giulio Guerrieri and Delia Kesner

We study the inhabitation problem in a Call-by-Push-Value (λ!-calculus) with quantitative typing system. We provide a notion of finite basis of all solutions and an algorithm computing such basis. We then show how simple restrictions of the grammar guiding the algorithm search solves the inhabitation problem for both Call-by-Name and Call-by-Value in quantitative settings.

Vincent van Oostrom

The FMC from a higher-order rewriting perspective

A syntactician's prology

We discuss how the FMC can be embedded in a third-order term rewriting systems, begetting meta-theoretical results such as confluence.

Willem Heijltjes

The Functional Machine Calculus

Joint work with Chris Barrett and Guy McCusker

I will present the Functional Machine Calculus (FMC), a simple model of higher-order computation with "reader/writer" effects: state, input/output, probabilities, and non-determinism. The main result is to extend two fundamental features of the lambda-calculus to these effects: confluence and simple types.

The premise is to view the lambda-calculus as an instruction language for a simple stack machine, in the standard way of the Krivine machine, where application is "push" and abstraction is "pop". The FMC then consists of two independent generalizations. The first is to allow multiple stacks (or streams) on the machine and use these to model input streams, output streams, and memory cells. The second is to introduce sequential composition, similar to Hasegawa's kappa-calculus and concatenative programming languages, which gives control over evaluation behaviour and allows the encoding of Plotkin's call-by-value lambda-calculus and Moggi's metalanguage.

Reduction for the encoded effect operations captures the laws for algebraic effects of Plotkin and Power, and because effects reduce algebraically, reduction is confluent. Simple types are available, and confer termination of the stack machine.

This workshop was made possible by:
EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing Inria Project COPRONOM