# LogSem Seminar talks in 2021

# 14-12-2021: Towards a Language for Automated Verification of Probabilistic Programs

**Speaker:** Christoph Matheja

**Time:** 14:00-15:00

**Location:** Ada-333

**Abstract:** Probabilistic programs offer a structured way to describe
computations with access to a source of randomness. They appear naturally in
the design of efficient algorithms, security protocols, and, more recently, as
modeling languages used in planning and artificial intelligence.

While the semantics of probabilistic programs has been studied since the early 80s, renewed interest in probabilistic models led to new program logics and proof rules targeting probabilistic programs in recent years. However, a comprehensive methodology for reasoning about probabilistic programs is still in its infancy: most of the new proof systems are neither automated nor fully formalized. Moreover, combining (or even understanding the connection between) different proof systems is difficult due to the lack of common foundations.

In this talk, I will present ongoing work on developing an intermediate verification language, similar to Boogie, Danny, or Viper, for (discrete) probabilistic programs in which various existing reasoning techniques can be described, encoded, and automated

**Bio:** Christoph’s research interests include formal and automated reasoning
techniques, particularly deductive verification model checking, for programs
that sample from probability distributions or manipulate dynamic data
structures.

He received his PhD from RWTH Aachen in 2020 in the group of Joost-Pieter Katoen, was a postdoc at ETH Zürich in the group of Peter Müller from 2020-2021, and has been an assistant professor at DTU since November 2021.

# 29-11-2021: Deep Induction

**Speaker:** Patricia Johann

**Time:** 13:00-14:00

**Location:** Ada-333

**Abstract:** I will first introduce deep induction and argue that it is the
notion of induction most appropriate to ADTs, (truly) nested types, and other
data types defined over, or mutually recursively with, (other) such types.
Standard induction rules induct over only the top-level data in a data
structure, leaving any data internal to the top-level data untouched. By
contrast, deep induction rules induct over all of the data present in a data
structure.
Next, I will give a grammar generating a robust class of nested types (and
thus ADTs). I will then describe how deep induction rules for these types can
be obtained by instantiating their recently defined semantics as fixpoints of
accessible endofunctors on locally presentable categories to a suitable
category of predicates.
Along the way I will explain how deep induction rules specialize to i) recover
their standard structural induction rules for those ADTs and nested types
already known to have them, and ii) solve the long-open problem of deriving
structural induction rules for bushes and other truly nested types. I will also
indicate why extending deep induction from nested types to GADTs is
non-trivial, and indicate the status of ongoing work on this problem.

# 22-11-2021: Machine-Checked Semantic Session Typing

**Speaker:** Jonas Kastberg Hinrichsen

**Time:** 13:00-14:00

**Location:** Ada-333

**Abstract:** Session types—a family of type systems for message-passing concurrency—have been subject to many extensions,
where each extension comes with a separate proof of type safety. These extensions cannot be readily combined,
and their proofs of type safety are generally not mechanised, making their correctness less trustworthy.
We have overcome these shortcomings with a semantic approach to binary asynchronous affine session types, by
developing a logical relations model in Coq using the Iris program logic. I demonstrate the power of our
approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references,
and locks/mutexes. As an additional benefit of the semantic approach, I demonstrate how we can manually prove
typing judgements of racy, yet safe, programs that cannot be type checked using only the rules of the type system.
In particular, in this talk I will cover the basics of session types and the basics of semantic typing,
and demonstrate how we achieve a mechanisation of the former, by using the latter in combination with the
Actris session type-based separation logic (in Iris).

# 15-11-2021: Trying to make relaxed concurrency memory models more accessible: the case of Armv8

**Speaker:** Jean Pichon-Pharabod

**Time:** 13:00-14:00

**Location:** Ada-333

**Abstract:** The classical styles of semantics of programming language theory
can be adopted and adapted to capture the concurrent behaviour of a mainstream
hardware architecture or programming language in the form of a relaxed memory
model. In this talk, I will first describe how, for Armv8, these different
styles of relaxed memory models have been used to achieve different compromises
between different goals: validation, abstraction, executability, etc. Then, I
will present work on using a different style to try to make Armv8 concurrency
more accessible to programmers and programming language theorists.

# 08-11-2021: Consequences of univalence on the symmetries of the spheres

**Speaker:** Pierre Cagne

**Time:** 13:00-15:00

**Location:** Ada-333

**Abstract:** I will start the talk by a gentle introduction to univalent
mathematics and how the univalent axiom impacts basic types. The focus will be
on *symmetries* of types, that is on the type A=A for a type A of the univalent
universe. We’ll start our exploration with symmetries of simple sets and then
move on to symmetries of more structured types, namely the spheres S¹, S², etc.
We will see that the case of the circle is highly special and I’ll try to convey
the reasons for it.

# 01-11-2021: Between abstraction and composition…

**Speaker:** Jon Sterling

**Time:** 13:00-15:00

**Location:** Nygaard-295

**Abstract:** The fundamental contradiction of programming and program verification can be
located in the tension between abstraction and composition. We make programs
more abstract in order to prevent bad interactions between components; on the
other side of the coin, we impede the composition of components when we
abstract them. Modern programming practice evinces many distinct levels of
abstraction that must be considered at the same time — for instance, compilers
break module boundaries during linking, complexity analysis breaks the
abstraction of extensional equivalence, and logical relations proofs break the
abstraction of closure under substitution. What is needed to meet this challenge
is linguistic tools that smoothly interpolate between these different levels
of abstraction. Building on my doctoral dissertation and joint work with Bob
Harper, I introduce a new plan for modal programming languages and logics that
treat the transition between different abstraction levels as a first-class
notion.

# 25-10-2021: On the accuracy of differentially private algorithms

**Speaker:** Boel Nelson

**Time:** 13:00-15:00

**Location:** Ada-333

**Abstract:** Differential privacy is emerging as the gold standard for
privacy. Still, in real settings, practitioners struggle to achieve low values
for the privacy parameter, epsilon. Essentially, the accuracy needed by
practitioners forces them to increase epsilon. So, why’s it so hard to achieve
meaningful differential privacy in practice?

In this talk I will highlight challenges with achieving high accuracy. In particular, I will elaborate on why accuracy is context dependent. I will also present a novel, data-aware approach to predicting accuracy.

# 04-10-2021: A parametrized bisimulation for interaction trees

**Speaker:** Alban Reynaud

**Time:** 13:00-15:00

**Location:** Ada-333

**Abstract:** Interaction trees are a data-structure for representing the
behavior of programs that interact with their environment. Implemented in Coq,
they can be used to verify compilers. Indeed, to prove that a program v and its
transformation C(v) are semantically equivalent, we usually proceed in two
steps:

- First, we represent the behaviors of v and C(v) with interaction trees;
- Then, we give an implementation of these interaction trees in a monad. The proof of the equivalence is performed for the interpretations. Nonetheless, this approach compels us to specify a concrete implementation. We lose some generality as other reasonnable implementations are not covered.

In this talk, I present an attempt to remedy this problem by providing an new equivalence. This equivalence is defined at the level of interaction trees, before the interpretation, while it still allows to derive the equivalence of reasonnable interpretation. This equivalence is based on an algebra of events.

# 20-09-2021: Categorical models for focused lambda-calculus

**Speaker:** Maxime Legoupil

**Time:** 13:00-14:00

**Location:** Nygaard-295

**Abstract:** Since the 70s, categories defined using lambda-calculus terms
have been introduced to allow to reason about lambda-calculus using the full
versatility of category theory. By interpreting on these categories theorems we
know to hold for any category, one can obtain new theorems on lambda-calculus,
or new proofs for well-known results. Simultaneously, the theory of focusing,
initially introduced to facilitate automated proofsearch, brought forth a new
kind of normal forms in the lambda-calculus that greatly reduces complexity
when reasoning with sum types. The question of a categorical model for focused
lambda-calculus thus arises, as it would allow for a new point of view on the
expanding field of focused lambda-calculus. Contrary to previous works on the
subject, this paper makes an effort to keep a syntax very close to the
simply-typed lambda-calculus that many are used to, and proposes a category for
the normal forms of focused lambda-calculus with sums. This allows, among other
things, for a new categorical proof for completeness of focused
lambda-calculus, and for a new proof of termination of simply-typed
lambda-calculus.

# 10-09-2021: Making pigs fly: design and implementation of the Futhark language

**Speaker:** Troels Henriksen

**Time:** 11:00-12:00

**Location:** Nygaard-295

**Abstract:** As an undergrad, I was taught that functional languages were the
future, because they are intrinsically parallel, and the future would be
parallel. It is now the future, but functional programming is still rarely used
for high-performance parallel programming. My research is about figuring out
why that is, and what we can do about it. In this talk I will talk about how we
carefully restricted and subsetted an ML-family language in order to compile it
to efficient GPU code, while still preserving the “feel” of functional
programming. I will talk about some of the crucial compiler optimisations and
transformations needed to generate code that is truly fast, even compared to
hand-written GPU code. I will keep the talk high level, and not assume any deep
knowledge of optimising compilers, functional programming, or GPUs.

**Bio:** Troels Henriksen is an assistant professor at DIKU working on the Futhark programming language.

# 21-06-2021: Recursion and sequentiality in categories of sheaves

**Speaker:** Cristina Matache

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
In this talk I will discuss how to build models of programming languages by using monads on categories of sheaves, leading up to a sheaf-based fully abstract model for a sequential language. I will explain what sheaves are, and how sheaf-based models are related to logical relations. As I will explain, our full abstraction result is connected to earlier work by O’Hearn and Riecke, which we have shown can now be viewed through the lens of synthetic domain theory.

The talk will be based on the following paper accepted to FSCD, which is joint work with Sean Moss and Sam Staton: https://arxiv.org/abs/2105.02156

# 14-06-2021: Formal security analysis of MPC-in-the-head zero-knowledge protocols

**Speaker:** Nikolaj Sidorenco

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
Zero-knowledge proofs allow a prover to convince a verifier of the veracity of a statement without revealing any other information. An interesting class of zero-knowledge protocols are those following the MPC-in-the-head paradigm (Ishai et al., STOC ’07) which use secure multiparty computation (MPC) protocols as the basis. Efficient instances of this paradigm have emerged as an active research topic in the last years, starting with ZKBoo (Giacomelli et al., USENIX ’16).
Zero-knowledge protocols are a vital building block in the design of privacy-preserving technologies as well as cryptographic primitives like digital signature schemes that provide post-quantum security.This work investigates the security of zero-knowledge protocols following the MPC-in-the-head paradigm. We provide the first machine-checked security proof of such a protocol on the example of ZKBoo. Our proofs are checked in the EasyCrypt proof assistant. To enable a modular security proof, we develop a new security notion for the MPC protocols used in MPC-in-the-head zero-knowledge protocols. This allows us to recast existing security proofs in a black-box fashion which we believe to be of independent interest.

# 07-06-2021: Relational logics for probabilistic programs

**Speaker:** Alejandro Aguirre

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
Relational logics express properties that relate two executions of a single
program, or two executions of two different programs. Properties such as
program equivalence, non-interference, differential privacy, robustness
or sensitivity fall under this umbrella. Probabilistic programs, in their simplest definition,
are programs that have a command to make a probabilistic choice. Verifying their behavior
is challenging and requires specialized techniques.

In this talk I present an overview of my work towards improving the state of the art of the techniques for reasoning about relational properties for both first- and higher-order probabilistic programs. We set out by developing Relational Higher-Order Logic (RHOL), a logic to prove relational properties of a pair of pure functional programs. We then showcase the versatility of RHOL by extending it to support reasoning about higher-order probabilistic programs, and in particular verifying adversarial properties that specify the behavior of a known program (an oracle) with respect to an unknown program or environment (the adversary). In the imperative setting, I present a predicate transformer to reason about expected sensitivity of probabilistic programs, which can be used to estimate how much the output of a probabilistic program can change when making changes to the input.

# 31-05-2021: Semantic approach to cut elimination

**Speaker:** Dan Frumin

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
We sketch a modular semantic proof of cut elimination
that works for sequent calculi for the intuitionistic sequent calculus
as well as the logic of bunched implications. The proof goes through
algebraic semantics and, arguably, more modular and less brittle than
the direct-style cut elimination proofs.

# 10-05-2021: Complete compositional relational reasoning for state and control

**Speaker:** Guilhem JABER

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages, with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.

(joint work with Andrzej Murawski)

# 03-05-2021: Certification of timed systems model checking: past, now, and future

**Speaker:** Simon Wimmer

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
Timed automata are a popular formalism for modeling real-time systems in safety-critical applications. Model checkers for timed automata are an effective verification method that can automatically prove safety of such a model with respect to a temporal specification. In my PhD thesis I have addressed the question of the trustworthiness of verification results obtained by timed automata model checkers. To this end, I have studied two approaches that try to significantly increase the level of trustworthiness by employing another popular verification method, interactive theorem proving.

In my talks I will summarize my results on the first approach where a timed automata model checker was fully verified in Isabelle/HOL. The main focus, however, will be on our more recent work on certification where unverified model checkers provide a certificate that is checked by an independent, verified certifier.

Finally, I will give an outlook on some of my ongoing and planned research that tries to expand on the certification approach.

# 26-04-2021: Efficient Binary Decision Diagram Manipulation in External Memory

**Speaker:** Steffan Sølvsten Jørgensen

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
We follow up on the idea of Lars Arge to rephrase the Reduce and Apply algorithms of Binary Decision Diagrams (BDDs) as iterative I/O-efficient algorithms. We identify multiple avenues to improve the performance of his proposed algorithms and extend the technique to other basic BDD algorithms.

These algorithms are implemented in a new BDD library, named Adiar . We see very promising results when comparing the performance of Adiar with conventional BDD libraries that use recursive depth-first algorithms. For instances of about 50 GiB, our algorithms, using external memory, are only up to 3.9 times slower compared to Sylvan, exclusively using internal memory. Yet, our proposed techniques are able to obtain this performance at a fraction of the internal memory needed by Sylvan to function. Furthermore, with Adiar we are able to manipulate BDDs that outgrow main memory and so surpass the limits of the other BDD libraries.

**Extra material:**

Preprint: https://arxiv.org/abs/2104.12101

Project Url: https://github.com/ssoelvsten/adiar

Slides: PDF

# 19-04-2021: Adjoint Reactive GUI Programming

**Speaker:** Neel Krishnaswami

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**

Most interaction with a computer is done via a graphical user interface. Traditionally, a GUI is implemented in an imperative fashion using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this talk, I will present an asynchronous FRP calculus for designing GUIs called λ𝖶𝗂𝖽𝗀𝖾𝗍. This calculus offers a novel categorical semantics for widgets, the building block of GUIs, and has both a natural Curry-Howard logical interpretation and an efficient implementation strategy.

# 22-03-2021: SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq

(joint work with Carmine Abate, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hrițcu, Kenji Maillard, and Bas Spitters)

**Speaker:** Philipp G. Haselwarter

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way. While very promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing fully machine-checked crypto proofs in the Coq proof assistant. Moreover, SSProve is itself formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.

**Extra material:**

Source code: https://github.com/SSProve/ssprove

# 15-03-2021: A model of Clocked Cubical Type Theory

**Speaker:** Magnus Baunsgaard Kristensen

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**

Guarded recursion allows for recursive reasoning in type theory, and has been applied in e.g. separation logic to extend the domain equation reasoning to those with negative occurrences. We present here a multi-clocked version of guarded recursion which can be used to encode coinductive types. This is done with Cubical Type Theory as the ambient type theory. The novel results relate to the interplay between the modal reasoning employed in guarded recursion and the constructors of CTT. A key advantage of such a theory is that we can employ the simple proof from CTT of functional extensionality in a setting with multi-clocked guarded recursion. Other important features include a large class of higher inductive types, which in turn lets one encode a large class of coinductive types, and the identification of bisimilarity and path equality for the type of labelled transition systems. We present a denotational model of this theory. One result of general interest is a method for including a modality defined in extensional type theory in CTT.

**Extra material:**

Preprint: https://arxiv.org/abs/2102.01969

# 01-03-2021: The multiverse model of dependent type theory

**Speaker:** Martin Ernst Bidlingmaier

**Time:** 12:00-13:00

**Location:** https://aarhusuniversity.zoom.us/j/67955180279

**Abstract:**
Since Seely’s work on the topic, we’ve been used to think of each
locally cartesian closed (lcc) category as a separate model of dependent
type theory. In this talk I want to argue you that also the collection
of all lcc categories is a model of dependent type theory. This “gros”
model is thus given by assembling the “petits” mathematical universes
(by which we understand lcc categories) into a single *multiverse*
model.

To make this precise, a coherence problem has to be resolved and I will sketch a solution based on model category theory, but we will focus on two applications: First, the multiverse model validates a form of predicative, bounded and parametric polymorphism. And second, the infinity categorical version of the multiverse model sheds new light on the somewhat mysterious J elimination principle of intensional equality types.

**Extra material:**

Preprint: https://arxiv.org/abs/2007.02900

Video from the Masaryk university seminar: https://www.youtube.com/watch?v=SJgnQUM5GEE