Talks in 2020

08-06-2020: A Polymorphic Type and Effect System with Boolean Unification

Speaker: Magnus Madsen, Jaco van de Pol

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/65045574235

Abstract: We present a simple, practical, and expressive type and effect system based on Boolean constraints. The effect system extends the Hindley-Milner type system, supports parametric polymorphism, and preserves principal types modulo Boolean equivalence. We show how to support type inference by extending Algorithm W with Boolean unification based on the successive variable elimination algorithm.

We implement the type and effect system in the Flix programming language. We perform an in-depth evaluation on the impact of Boolean unification on type inference time and end-to-end compilation time. While the computational complexity of Boolean unification is NP-hard, the experimental results demonstrate that it works well in practice. We find that the impact on type inference time is on average a 1.4x slowdown and the overall impact on end-to-end compilation time is a 1.1x slowdown.

25-05-2020: Nakamoto-Style Blockchain Consensus 101

Speaker: Søren Eller Thomsen

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/68049508119

Abstract: This talk will present the basic functionality of a Nakamoto-style consensus mechanism. I will focus on under what circumstances this functionality is provided and how that reflects upon on an ongoing verification effort of a Proof-of-Stake Nakamoto-style blockchain.

18-05-2020: The right answer at the right time: an introduction to time complexity verification using time credits

Speaker: Armaël Gueneau

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/65650808630

Abstract: Algorithms textbooks typically contain informal theorems and proofs about the complexity of algorithms, e.g. "binary search runs in O(log n)". In this talk, I will give a gentle introduction to how one might go and formally verify such claims in a proof assistant, with respect to concrete programs. Formally, I will demonstrate the use of Separation Logic with Time Credits for verifying both the correctness and complexity of concrete code, in a way that scales up from textbook examples to state of the art algorithms. The talk will be based on work that I did during my PhD, but is mostly intended as a general introduction of the topic.

11-05-2020: How to Define Things by Recursion

Speaker: Alex Kavvos

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/68849066187

Abstract: A crash course in the basic notions of domain theory.

04-05-2020: Analysis in univalent type theory

Speaker: Auke Booij

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/67856492801

Abstract: This talk is a thematic introduction to my thesis work on constructive analysis in univalent type theory. The central role of identity types in univalent type theory allows us to develop constructive analysis in a style highly reminiscent of traditional analysis, but additionally carrying computational content. The description of propositions in univalent type theory is key, and in this talk this is motivated by considering a locatedness structure on the real numbers.

27-04-2020: Blame for Null

Speaker: Abel Nieto

Time: 13:00-14:00

Location: https://aarhusuniversity.zoom.us/j/61149665805

Abstract: Multiple modern programming languages, including Kotlin, Scala, Swift, and C#, have type systems where nullability is explicitly specified in the types. All of the above also need to interoperate with languages where types remain implicitly nullable, like Java. This leads to runtime errors that can manifest in subtle ways. In this talk, I will show how to reason about the presence and provenance of such nullability errors using the concept of blame from gradual typing. Specifically, I will present a calculus, “lambda null”, where some terms are typed as implicitly nullable and others as explicitly nullable. Just like in the original blame calculus of Wadler and Findler, interactions between both kinds of terms are mediated by casts with attached blame labels, which indicate the origin of errors. On top of lambda null, we then define a second calculus, “stratified lambda null“, which closely models the interoperability between languages with implicit nullability and languages with explicit nullability, such as Java and Scala. The main result is a theorem that states that nullability errors in stratified lambda null can always be blamed on terms with less-precise typing; that is, terms typed as implicitly nullable. By analogy, this would mean that NullPointerExceptions in combined Java/Scala programs are always the result of unsoundness in the Java type system. The result can be summarized with the slogan “explicitly nullable programs can't be blamed”. The results are formalized in the Coq proof assistant.

30-03-2020: High-assurance modular inversion using Fiat Cryptography

Speaker: Benjamin Salling Hvass

Time: 13:00-14:00

Location: Zoom: https://aarhusuniversity.zoom.us/j/359931396

Abstract:

Crypto-code is highly vulnerable to attacks and therefore a worthwhile target for verification/formalization.

A recent contribution to this area of ‘high-assurance crypto’ is the Fiat Cryptography library which allows synthesis of constant-time and verified code implementing finite field arithmetic (modulo any prime).

The work presented in this talk, is an attempt to extend the Fiat Crypto framework to also be able to generate a verified, constant-time and efficient modular inversion implementation.

This is joint work with Bas Spitters and Diego F. Aranha.

23-03-2020: ∃R-Completeness of Stationary Nash Equilibria in Perfect Information Stochastic Games

Speaker: Steffan Sølvsten

Time: 13:00-14:00

Location: Zoom: https://aarhusuniversity.zoom.us/j/364163471

Abstract: In applications of modelling, verification, and synthesis one can reason about the system in terms of a stochastic game, where the system is pitted against the environment. From such a perspective, it is then of common interest to discern whether there is a strategy, such that the system is always winning in respect to some goal. For this, the concept of Nash equilibria is often used to reason about agents that behave rationally.

We show that the problem of deciding whether in a multi-player perfect information recursive game there exists a stationary Nash equilibrium ensuring each player a certain payoff is ∃R-complete. Combining our result with known gadget games without any stationary Nash equilibrium, we obtain that for cyclic games, just deciding existence of any stationary Nash equilibrium is ∃R-complete, and thereby also existence of a surely winning strategy. This holds for both reachability and safety goals, and for deterministic recursive games.

This work is part of a project with Kristoffer Arnsfelt Hansen.

09-03-2020: Towards Computational Models for Authorization Logics

Speaker: Andrew Hirsch

Time: 13:00-14:00

Location: Nygaard meeting room 395

Abstract: Authorization logics are multi-modal logics used to reason about authorization in distributed systems. Significant work has been done developing proof theory and model theory for authorization logics. However, the model theories built so far cannot represent distribution and communication. This means they can neither be used to inform proof-system design decisions nor to build verification tools.

In this talk, I will introduce current work in building computational models for authorization logics. This interprets proofs as programs, in the style of the propositions-as-types principal. However, unlike previous attempts at propositions-as-types correspondences for authorization logics, we embrace the distributed nature of authorization logics. To do this, we adapt choreographic programming, a programming paradigm for concurrent programming, with modal types. A long-term goal is to build a type theory based on choreographic programming, allowing programmers to build certified secure distributed systems.

09-03-2020: Bi-Intuitionistic Types via Alternating Contexts

(The talk has been cancelled)

Speaker: Ranald Clouston

Time: 14:15-15:00

Location: Nygaard meeting room 395

Abstract: Bi-intuitionistic logic is the conservative extension of intuitionistic logic with a binary operator called exclusion, dual to implication. In the early 2000s Crolard designed a type system for this logic, introducing a notion of control operator more restricted than classical call/cc. However this system is flawed, as it is claimed to imply cut-elimination for a sequent calculus of Rauszer, which is now known not to hold. We propose a new type system that is sound and complete for this logic, with a novel notion of 'alternating' variable context inspired by work in modal type theory. Alternating contexts allow one to interleave lambda- and mu-variables, with structural symbols interpreted variously as products, sums, and exclusion.

02-03-2020: How programming language research can help securely implement cryptography

Speaker: Alix Trieu

Time: 13:00-14:00

Location: Nygaard meeting room 395

Abstract: Cryptography is a mature research field where clear techniques and methodology to show security of algorithms as reductions of well identified problems are known. However, the art of implementing cryptography is reserved to a few experts. Indeed, it does not suffice that the implementation be functionally correct, but it also needs to be secure. In this talk, I will give a small overview of the concerns that cryptography implementers have to worry about, the countermeasures they came up with and how these map to a well-known property in the language-based security community, namely non-interference. Finally, I will talk about how PL research techniques have and can help to securely implement cryptography.

Disclaimer 1: This will be a whiteboard presentation.

Disclaimer 2: I will give the same talk with slides at the crypto seminar on March 16th.

24-02-2020: Univalent parametricity and refinements for free

Speaker: Andreas Aagaard Lynge

Time: 13:00-13:45

Location: Nygaard meeting room 395

Abstract: I will present parametricity and discuss its relation to univalent parametricity and refinements for free. The parametricity abstraction theorem provides free theorems about polymorphic terms. The abstraction theorem in univalent parametricity similarly provides free theorems. These can be used to transport properties between equivalent types. I will explore on this and discuss benefits of univalent parametricity. Afterwards I introduce refinements for free, a method to apply free theorems from parametricity to transport properties between related structures.

03-02-2020: Enumerating and Counting N-Queens solutions: Between heuristics and structure

Speaker: Irfansha Shaik

Time: 13:00-14:00

Location: Nygaard meeting room 395

Abstract: The N-Queens problem is a 150-year-old classical mathematical problem of placing N queens on an N * N chessboard such that no two queens share the same row, column or a diagonal, i.e. non-attacking queens. The counting N-Queens is the task of counting all such solutions of the N-Queens problem.

There are two main research directions here, one is to find scalable efficient algorithms and the other to find structure in the problem. Despite being a widely researched problem there seems to be a wide gap between finding/using the structure and algorithmic implementations.

In this talk, we will try to bring them together by looking closely at enumeration algorithms and counting algorithms with respect to the constraints of the problem. In Enumeration, we focus on SAT solving perspective with propagation, unsatisfiability and heuristics (given as parameters) where as in counting we utilize the structure of the problem.

This work is part of MSc by Research degree from Swansea University in collaboration with Oliver Kullmann.

13-01-2020: Multimodal Dependent Type Theory

Speaker: Daniel Gratzer

Time: 13:00-14:30

Location: Nygaard meeting room 395

Abstract:
Modalities have proved to be a recurring phenomenon in type theories, arising in both mathematical and computational contexts. Despite the wide variety of uses, a general framework for modal dependent type theories has still proven elusive. Each modal situation requires a handcrafted type theory, and establishing the properties of these type theories requires a significant technical investment.

In this work, we have attempted to isolate a class of modal situations which can be given a single uniform syntax and allow for the typical metatheorems of type theory to be proven once and for all. Our approach generalizes the ideas latent in Nuyts, Vezzosi, and Devriese, and simplifies the forthcoming work by Licata, Shulman, and Riley on a of subset of mode theories. This calculus is sufficiently flexible to model internal parametricity, guarded recursion, and even axiomatic cohesion.

In the interest of giving an interesting talk for everyone, we will focus on modal type theory in general, and discuss the historical approaches and challenges and how our type theory handles these difficulties.

joint work with Lars Birkedal, Alex Kavvos, and Andreas Nuyts