LogSem Seminar talks in 2023
15-05-2023: On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments
Speaker: Ugo Dal Lago, University of Bologna and INRIA Sophia Antipolis
Time: 13:00-14:00
Location: Turing-014
Abstract: A system of session types is introduced as induced by a Curry Howard correspondence applied to bounded linear logic, suitably extended with probabilistic choice operators and ground types. The resulting system satisfies some expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.
01-05-2023: A higher-order language for Markov kernels and linear operators
Speaker: Pedro H. Azevedo de Amorim, Cornell University
Time: 13:00-14:00
Location: Ada-333
Abstract: Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators. Both styles of semantics have found numerous applications, but each has their strengths and weaknesses. In this work we define a two-level calculus that makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, one where the resource being kept track of is sampling, not variable usage.
17-04-2023: Denotational semantics in impredicative guarded dependent type theory
Speaker: Jon Sterling
Time: 13:00-14:00
Location: Nygaard-297
Abstract: Impredicative guarded dependent type theory (iGDTT) is a new version of type theory that combines guarded recursion (the “later” modality) with impredicative polymorphism (universal and existential types). It turns out that these two features are sufficient to define a very simple denotational semantics for System F with recursive types and higher-order store. We believe that the expressivity of iGDTT brings us one step closer to a general metalanguage for realistic denotational semantics, and provides a compelling strategy to elude the burden of operational semantics. As a further benefit, we are now able to justify the extension of full dependent type theory with a Haskell-style IO-monad and IORef types.
27-03-2023: Some applications of free extensions to partial evaluation, equational-proof synthesis, and normalisation-by-evaluation
Speaker: Ohad Kammar, University of Edimburgh
Time: 13:00-14:00
Location: Ada-333
Abstract: The free extension (frex) offers a uniform theoretical foundation for the collection of partial-evaluation techniques known as partially-static data structures. The frex approch identifies concepts from universal algebra with concepts from partially-static data structures: signature with syntax; equations with semantics; algebra with static domain; and free extension with open-terms modulo semantics. This identification allows us to design and implement generic partial evaluators, with promising results regarding code-reuse and modularly. I will start by motivating the use of algebra for partial evaluation from first principles, and introduce the concept of a free extension. Then I will review our existing and recent work applying this approach to staged partial evaluation and equational-proof synthesis in dependently-typed languages. Time-permitting, I will outline ongoing work. First, developing generic algorithms for normalisation-by-evaluation modulo algebraic-structure. Second, concerning the modular construction of free extensions. Joint work with: Guillaume Allais, Edwin Brady, Greg Brown, Nathan Corbyn, Tamara von Glehn, Sam Lindley, Nachi Valliappan, and Jeremy Yallop
20-03-2023: Expectation-Transformer Reasoning with Concurrent Separation Logic: A story about Invariants, Quantities and their Expectation
Speaker: Ira Fesefeldt, RWTH Aachen
Time: 13:00-14:00
Location: Ada-333
Abstract: Reasoning about both - Concurrent and Probabilistic Programs - is hard. For the former Concurrent Separation Logic, for the latter Weakest Preexpectations is facilitated. Luckily, a combination is possible and give rise to Concurrent Quantitative Separation Logic. In this talk, I will introduce you to weakest preexpectation reasoning and present you a separation logic extension of it for reasoning with concurrency.
13-03-2023: Defining contextual refinement for capability machines
Speaker: Dorian Lesbre
Time: 13:00-14:00
Location: Ada-333
Abstract: Contextual refinement is a useful notion to relate two open programs x and y by saying that for all contexts C, any observable behavior of C[x] is also seen in C[y]. As such it offers a strong relation based only on the operational semantics of closed programs. I present here a definition of contextual refinement for capability machines, a type of CPU which uses special hardware checks to enforce safety constraints on memory accesses. I present the challenges of porting refinement to low-level programs, some results obtained by combining refinement with capability safety, and explore how refinement can be shown using a logical binary relation.
06-03-2023: Overview of Proost, a student-made proof assistant in Rust
Speaker: Vincent Lafeychine
Time: 13:00-14:00
Location: Ada-333
Abstract: In this talk, I will present, from a software-engineering point of view, a Rust proof-assistant that we, three fellows and myself, have built over a semester. As it has been observed in many other proof-assistant projects, inconsistencies can arise quickly (https://inutile.club/estatis/falso/). In the absence of a formal proof of the soundness of the kernel, a series of tests and coverage verifications are performed to provide a certain level of confidence in its well-functioning. Besides, Rust’s borrow-checker can be challenging to work with. That can be solved by using a specific memory model that, moreover, allows to do some optimisations.
27-02-2023: Denotational semantics of type theory
Speaker: Daniel Gratzer
Time: 13:00-14:00
Location: Ada-333
Abstract: Many of us use proof assistants like Coq or Agda to formalize the logics and arguments that we study. In so doing, however, it is not uncommon to bump into uncomfortable restrictions imposed by the type theory these tools support. In these circumstances, it is usually quickest to extend the proof assistant through postulates, rewrite rules, or plugins to better host our informal arguments. Doing this, however, carries a substantial risk: how do we know that we have not introduced an inconsistency? In this talk I review the basics of denotational semantics for type theory with the aim of answering this question. We will work through the definition of a model of type theory and discuss how to construct one. Throughout, our focus be on how semantics can provide us with confidence that what we write in a proof assistant corresponds with our intentions.
20-02-2023: Program Logics for Probabilistic Programs
Speaker: Alejandro Aguirre
Time: 13:00-14:00
Location: Ada-333
Abstract: Probabilistic programs have a wide range of applications to fields like cryptography or algorithms, but reasoning about probabilistic programs is complicated and unintuitive. In this talk, I will give an overview of how formal methods are used in the literature to reason about probabilistic programs. I will begin by presenting the semantics for a simple imperative language extended with probabilistic choice, and then proceed to present different program logics that can be used to formally verify different properties of programs written in this language.
06-02-2023: Higher-Order Weakest Precondition Transformers via a CPS Transformation
Speaker: Satoshi Kura, National Institute of Informatics / University of Oxford
Time: 13:00-14:00
Location: Ada 333
Abstract: Weakest precondition transformers are essential notions for program verification, and various extensions have been studied. However, only a few consider both higher-order languages and syntactic calculation of weakest precondition transformers. In this talk, we consider weakest precondition transformers for a higher-order functional language with computational effects and recursion. Based on a general framework of categorical semantics, we show that we can calculate the weakest precondition transformers via a CPS transformation. We also show how to instantiate our result to (1) verification of trace properties by Kobayashi et al. and (2) expected cost analysis by Avanzini et al.
16-01-2023: Demonstration of Vercors: a Verifier of Concurrent and Distributed Software
Speaker: Pieter Bos, University of Twente
Time: 13:00-14:00
Location: Ada 333
Abstract: https://vercors.ewi.utwente.nl