BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:SANDWICH Day  - Jon Sterling\, Ariadne Si Suo\, Kayvan Memarian\, 
 Gregor Feierabend\, Ines Wright (University of Cambridge)
DTSTART:20250602T090000Z
DTEND:20250602T160000Z
UID:TALK231808@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
DESCRIPTION:10:00–11:00 – Jon Sterling: An Invitation to Synthetic Dom
 ain Theory\n\nDomain theory offers a denotational semantics for general re
 cursive functional programming\, but working directly with domains and the
 ir 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 me
 thods can simplify the use of domain theory by recasting domains as specia
 l types in an alternate reality where all functions are automatically as c
 ontinuous as possible. We will see how to formulate domains and general re
 cursion in the synthetic setting by extending Homotopy Type Theory with a 
 bounded distributive lattice of observations satisfying a few additional l
 aws.\n\n11:15–12:15 – Ariadne Si Suo: Type Checking is Proof Reduction
 s in Classical Linear Logic\n\nI will try to convince you type checkers ca
 n be seen as logic programs with ‘directions’\, and doing type checkin
 g corresponds to doing proof reductions in classical linear logic. This gi
 ves us implementations of type checking algorithms for free\, by writing b
 idirectional typing rules as directional logic programs. Based on joint wo
 rk with Neel Krishnaswami and Vikraman Choudhury.\n\nIf time permits\, I m
 ight also tell you a bit about my (preliminary) understanding of transcend
 ental syntax (by Jean-Yves Girard) and Existence vs. Essence\, and why it 
 might be useful to think about these things sometimes.\n\n12:15-1:30 Lunch
 \n\n1:30–2:30 Kayvan Memarian: Executable Specification of a Production 
 Hypervisor\n\nDeveloping systems code that robustly provides its intended 
 security guarantees remains very challenging: conventional practice does n
 ot suffice\, and full functional verification\, while now feasible in some
  contexts\, has substantial barriers to entry and use.\n\nIn this work\, w
 e explore an alternative\, more lightweight approach to building confidenc
 e 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 desir
 ed behaviour in a way that can be used as a test oracle\, and check corres
 pondence between that and the implementation at runtime. The setting makes
  that challenging in several ways: the implementation and specification ar
 e intertwined with the underlying architecture\; the hypervisor is highly 
 concurrent\; the specification has to be loose in certain ways\; the hyper
 visor runs bare-metal in a privileged exception level\; naive random testi
 ng 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 bu
 gs in pKVM along the way.\n\n2:45–3:45 Gregor Feierabend (joint work wit
 h Marcelo Fiore): Confluence of Term Rewriting Systems with Variable Bindi
 ng\n\nIn this talk\, we will consider a generalised confluence theorem in 
 the spirit of Aczel [1] in the context of the model of second-order abstra
 ct syntax in the category of presheaves over the category of finite cardin
 als [2\, 3].\nWe will recall from Fiore et al [2\, 3] that a signature wit
 h variable-binding operators induces a strong term monad\, T\, on this cat
 egory.\nA 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 def
 ines a reduction relation ⤳ ⊆ T(0) × T(0).\nClosely 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.\n\n[1] 
 P. Aczel\, A General Church–Rosser Theorem. Unpublished note\, 1978.\n[2
 ] M. Fiore\, Second-Order and Dependently-Sorted Abstract Syntax\, In Proc
 eedings of the 23rd Annual ACM/IEEE Symposium on Logic in Computer Science
  (LICS 2008)\, pages 57–68. IEEE\nComputer Society\, 2008.\n[3] M. Fiore
 \, G. Plotkin\, and D. Turi\, Abstract Syntax and Variable Binding\, In Pr
 oceedings of the 14th Annual ACM/IEEE Symposium on Logic in Computer Scien
 ce (LICS 1999)\, pages 193–202. IEEE Computer Society\, 1999.\n\n4:00–
 5:00 Ines Wright: Dependent Linear Type Theory via Bunched(less) Implicati
 ons\n\nIntroducing the `number-of-usages` reading of linear variables to d
 ependent type theory has in prior work resulted in type theories with depe
 ndencies and identity types restricted to closed linear terms. In this tal
 k I will discuss work I have been doing for my Master's thesis\, supervise
 d by Neel Krishnaswami\, applying the ownership reading of resources as se
 en in the logic of bunched implications to dependent types\, with the goal
  of designing a dependently typed bunched implications which allows depend
 ency and identity types of terms which include resources.\n\n6:00- ? The M
 aypole 
LOCATION:FW26\, Computer Laboratory
END:VEVENT
END:VCALENDAR