SANDWICH Day

Add to your list(s) Download to your calendar using vCal

• Jon Sterling, Ariadne Si Suo, Kayvan Memarian, Gregor Feierabend, Ines Wright (University of Cambridge)
• Monday 02 June 2025, 10:00-17:00
• FW26, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

10:00–11:00 – Jon Sterling: An Invitation to Synthetic Domain Theory

Domain theory offers a denotational semantics for general recursive functional programming, but working directly with domains and their continuity laws can be a bit technical; it is also not easy to find a single notion of “domain” that is good for most purposes. Synthetic methods can simplify the use of domain theory by recasting domains as special types in an alternate reality where all functions are automatically as continuous as possible. We will see how to formulate domains and general recursion in the synthetic setting by extending Homotopy Type Theory with a bounded distributive lattice of observations satisfying a few additional laws.

11:15–12:15 – Ariadne Si Suo: Type Checking is Proof Reductions in Classical Linear Logic

I will try to convince you type checkers can be seen as logic programs with ‘directions’, and doing type checking corresponds to doing proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, by writing bidirectional typing rules as directional logic programs. Based on joint work with Neel Krishnaswami and Vikraman Choudhury.

If time permits, I might also tell you a bit about my (preliminary) understanding of transcendental syntax (by Jean-Yves Girard) and Existence vs. Essence, and why it might be useful to think about these things sometimes.

12:15-1:30 Lunch

1:30–2:30 Kayvan Memarian: Executable Specification of a Production Hypervisor

Developing systems code that robustly provides its intended security guarantees remains very challenging: conventional practice does not suffice, and full functional verification, while now feasible in some contexts, has substantial barriers to entry and use.

In this work, we explore an alternative, more lightweight approach to building confidence for a production hypervisor: the pKVM hypervisor developed by Google to protect virtual machines and the Android kernel from each other. The basic approach is very simple and dates back to the 1970s: we specify the desired behaviour in a way that can be used as a test oracle, and check correspondence between that and the implementation at runtime. The setting makes that challenging in several ways: the implementation and specification are intertwined with the underlying architecture; the hypervisor is highly concurrent; the specification has to be loose in certain ways; the hypervisor runs bare-metal in a privileged exception level; naive random testing would quickly crash the whole system; and the hypervisor is written in C using conventional methods. We show how all of these can be overcome to make a practically useful specification, finding a number of critical bugs in pKVM along the way.

2:45–3:45 Gregor Feierabend (joint work with Marcelo Fiore): Confluence of Term Rewriting Systems with Variable Binding

In this talk, we will consider a generalised confluence theorem in the spirit of Aczel [1] in the context of the model of second-order abstract syntax in the category of presheaves over the category of finite cardinals [2, 3]. We will recall from Fiore et al [2, 3] that a signature with variable-binding operators induces a strong term monad, T, on this category. A rewrite rule, ρ, can then be defined to be a pair of terms in T(M)(0) for some presheaf of meta-variables, M. Every ρ inductively defines a reduction relation ⤳ ⊆ T(0) × T(0). Closely following Aczel’s approach, we will establish a coherence property for ρ and show that it yields the confluence of the reduction relation ⤳. As an application, we will examine the confluence of β-reduction in the λ-calculus.

[1] P. Aczel, A General Church–Rosser Theorem. Unpublished note, 1978. [2] M. Fiore, Second-Order and Dependently-Sorted Abstract Syntax, In Proceedings of the 23rd Annual ACM /IEEE Symposium on Logic in Computer Science (LICS 2008), pages 57–68. IEEE Computer Society, 2008. [3] M. Fiore, G. Plotkin, and D. Turi, Abstract Syntax and Variable Binding, In Proceedings of the 14th Annual ACM /IEEE Symposium on Logic in Computer Science (LICS 1999), pages 193–202. IEEE Computer Society, 1999.

4:00–5:00 Ines Wright: Dependent Linear Type Theory via Bunched(less) Implications

Introducing the `number-of-usages` reading of linear variables to dependent type theory has in prior work resulted in type theories with dependencies and identity types restricted to closed linear terms. In this talk I will discuss work I have been doing for my Master’s thesis, supervised by Neel Krishnaswami, applying the ownership reading of resources as seen in the logic of bunched implications to dependent types, with the goal of designing a dependently typed bunched implications which allows dependency and identity types of terms which include resources.

6:00- ? The Maypole

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory
• TBC
• tcw57’s list

Note that ex-directory lists are not shown.