SANDWICH Seminar (Computer Laboratory)


2023-09-25 13:00: Polymorphic Subtyping with Polarisation: ∀ ± ∃ (Ilya Kaysin, University of Cambridge)

2023-10-02 13:00: Definitional Functoriality for Dependent (Sub)Types  (Dr Meven Lennon-Bertrand (University of Cambridge))

2023-10-03 11:00:  Generic bidirectional typing for dependent type theories (Thiago Felicissimo, INRIA)

2023-10-09 13:00: A couple of things I’ve learned about algebraically universal categories (Ioannis Eleftheriadis, University of Cambridge)

2023-10-16 13:00: Higher-Order Algebraic Effects and Handlers (Zhixuan Yang, Imperial College London)

2023-10-23 13:00: Type theoretic approaches to semistrictness (Alex Rice (University of Cambridge))

2023-10-30 13:00: Computing inverses in higher categories (Thibaut Benjamin, University of Cambridge)

2024-01-22 13:00: A Denotational Approach to Release/Acquire Concurrency (Yotam Dvir (Tel Aviv University))

2024-02-20 13:00: SSA is Freyd Categories (University of Cambridge)

2024-09-30 13:00: Some cool facts about dualities (Vikraman Choudhury, University of Bologna & Inria OLAS team)

2024-10-21 13:00: Traversing the Eckmann-Hilton Hyperclock (Wilf Offord (University of Cambridge))

2024-10-25 14:00: On the Operational Theory of the CPS-Calculus (Paulo Torrens (University of Kent) )

2024-10-28 13:00:  Toward a Coq formalisation of the Arm architecture (Thibaut Perami (University of Cambridge))

2024-11-04 13:00: Executable Separation Logic Specifications in CN (Rini Banerjee (University of Cambridge))

2024-11-11 13:00: Do You Really Understand Incompleteness? (Lingyuan Ye (University of Cambridge))

2024-11-18 13:00: Unrolling Lists (Jake Bennett-Woolf (University of Cambridge))

2024-11-25 13:00: Mixed Linear-Cartesian Theories as Substitution Monoids (Sanjiv Ranchod (University of Cambridge))

2024-12-02 13:00:  Substitution, Normalization, and Formalization (Yulong Huang (University of Cambridge))

2025-01-20 13:00:  Decision Procedures for Bitvector Reasoning in Lean (Siddharth Bhat (University of Cambridge))

2025-01-27 13:00: The Denotational Semantics of SSA (Jad Ghalayini (University of Cambridge))

2025-02-03 13:00: What does it take to certify a conversion checker? (Meven Lennon-Bertrand (University of Cambridge))

2025-02-10 13:00: Generalised J rules and simultaneous pattern matching of equalities (Thibaut Benjamin (University of Cambridge))

2025-02-17 13:00: Closing the Gap between Transactional Consistency Models and Executable Code using Separation Logic  (Anders A. Mathiasen)

2025-03-03 13:00: Free algebras for free theories (Ioannis Markakis (University of Cambridge))

2025-03-10 13:00: Skew structure in categories (Dima Szamozvancev (University of Cambridge))

2025-03-17 13:00: A Typed, Algebraic Approach to Parsing (Neel Krishnaswami (University of Cambridge) )

2025-03-28 12:30: The 2-Category of Graded Monads (Tori Vollmer (University of Kent))

2025-04-28 13:00: Toward a liquid call-by-push-value (Dimitrios Economou (University of Cambridge))

2025-05-06 13:00: A Computer Architect's Attempt at Using Type Theoretic Concepts to Model Branch Predictors (Karl Mose (University of Cambridge))

2025-05-12 13:00:  PNVI-ae-udi: the last (most recent) C memory object model (Dhruv Makwana (University of Cambridge))

2025-05-19 13:00: Heyting Algebras and Higher-Order Logic (Prof. Andrew M Pitts (University of Cambridge))

2025-05-27 13:00: Automated Methods for Logic-Based Higher-Order Program Verification (Hiroyuki Katsura (University of Cambridge))

2025-06-02 10:00: SANDWICH Day  (Jon Sterling, Ariadne Si Suo, Kayvan Memarian, Gregor Feierabend, Ines Wright (University of Cambridge))

2025-06-02 10:00: An Invitation to Synthetic Domain Theory (Jon Sterling (University of Cambridge))

2025-06-02 11:15: Type Checking is Proof Reductions in Classical Linear Logic (Ariadne Si Suo  (University of Cambridge))

2025-06-02 13:30: Executable Specification of a Production Hypervisor (Kayvan Memarian (University of Cambridge))

2025-06-02 14:45: Confluence of Term Rewriting Systems with Variable Binding (Gregor Feierabend (University of Cambridge))

2025-06-02 16:00: Dependent Linear Type Theory via Bunched(less) Implications (Ines Wright (University of Cambridge))

2025-11-24 13:00: Soteria and Compositional Symbolic Execution à la Carte (Sacha-Élie Ayoun)

2025-12-01 13:00: Decision procedures for parametric multi-width bitvectors (Siddharth Bhat (University of Cambridge))

2026-01-26 13:00: ArchSem: Reusable Rigorous Semantics of Relaxed Architectures (Thibaut Pérami)