LogSem Seminar talks in 2021
16-12-2021: Towards a Language for Automated Verification of Probabilistic Programs
Speaker: Christoph Matheja
Time: 13:00-14:00
Location: Zoom (https://aarhusuniversity.zoom.us/j/66587119191)
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.
13-12-2021: Are fine-grained and coarse-grained dynamic information flow control always equally expressive?
Speaker: Aslan Askarov
Time: 13:00-14:00
Location: Ada-333
Abstract: In their POPL 2019 paper, Vassena et al. study the problem of expressiveness of fine-grained and coarse-grained techniques for dynamic information flow control. A notable result of that work is the semantics-preserving translation from a language with a fine-grained dynamic IFC system to a language with a coarse-grained dynamic IFC system, meaning that coarse-grained approaches can track information as precisely as fine-grained ones. In this work, we lift two technical assumptions that stand out among the details of Vassena et al.’s translation. First, the security property for which the equivalence is formally established is termination-insensitive noninterference. Second, both coarse and fine-grained languages are statically typed in a standard (security unaware) way. We derive a novel 2-labeled fine-grained dynamic IFC system, for which we have not found a semantics-preserving approach that is idiomatically coarse-grained. We conjecture that 2-labeled (and generally n-labeled) fine grained monitors unveil an expressiveness gap between the fine-grained and the coarse-grained approaches to dynamic IFC.
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