Jamie Vicary

Name:	Jamie Vicary
Affiliation:	University of Cambridge
E-mail:	(only provided to users who are logged into talks.cam)
Last login:	13 Apr 2026, 9:25 a.m.

Public lists managed by Jamie Vicary

• Logic and Semantics Seminar (Computer Laboratory)

Talks given by Jamie Vicary

Obviously this only lists talks that are listed through talks.cam. Furthermore, this facility only works if the speaker's e-mail was specified in a talk. Most talks have not done this.

Talks organised by Jamie Vicary

This list is based on what was entered into the 'organiser' field in a talk. It may not mean that Jamie Vicary actually organised the talk, they may have been responsible only for entering the talk into the talks.cam system.

• A selective and biased choice of techniques for building a distributed data store
• Synthesis modulo oracles
• Testing GPU Memory Consistency at Large
• A categorical semantics for neural networks
• Computing inverses in higher categories
• Coherence by Normalization for Linear Multicategorical Structures
• Software for Compositional Modeling
• Higher-Order Algebraic Effects and Handlers
• A couple of things I’ve learned about algebraically universal categories
• Polymorphic Subtyping with Polarisation: ∀ ± ∃
• Optimizations in a formally verified compiler
• Formalizing General Calculi with Binders in Rewriting Logic
• RoboCert: A Formal Specification Notation for Robotic Software
• Making concurrency functional
• Compound Memory Models
• Types-To-Sets and Types-to-PERs Relativization in Higher-Order Logic
• Model Checking Disjoint-Paths Logic on Topological-Minor-Free Graph Classes
• Graduality and Parametricity - Together again for the first time, for the second time
• Stochastic games and strategy complexity
• The Functional Machine Calculus
• Bidirectional typing is not just an implementation technique
• When Concurrency Strikes
• Functional Programming with an Incremental Datalog
• Functional Programming with an Incremental Datalog
• String diagrams for semistrict n-categories
• The linear operator semantics of probabilistic programs
• Linear Logic and the Semantics of Concurrent Computation
• On bilinearity of Whitehead products in Homotopy Type Theory
• Subcubic certificates for CFL reachability
• Coherent differentiation makes the differential lambda-calculus deterministic
• Generic pattern unification: a categorical approach
• ∞-type theories and coherence problems
• Mixing finite and infinite structure
• Verification for free: using K to build a theorem prover for any language
• Title to be confirmed
• The Expressive Power of CSP Quantifiers
• Algebraic type theory
• Staged Compilation with Two-Level Type Theory
• Decoding Nets: A Formal Take on Address Translation
• Finite-state polynomial computation
• Symmetries in quantitative semantics
• Title to be confirmed
• Symmetries in Reversible Programming
• Game comonads, FVM theorems, and bilinear maps
• The complexity of counting problems
• Cyclic Implicit Complexity
• How undecidable are HyperLTL and HyperCTL*?
• A categorical view of conditional expectation
• CANCELLED -- The complexity of counting problems
• Relational databases versus relational models
• Theorem Provers to Protect Democracy: Formally Verified Vote-Counting-Software
• A computational method for left adjointness
• Towards a geometry for syntax
• Enriched categories for optimal transport
• The Semantics of Shared Memory in Intel CPU/FPGA Systems
• CaTT, a type-theory to describe weak omega-categories
• Quantum Software in 2021: Patterns and Problems
• Unfinity Categories
• Promising ARMv8/RISC-V relaxed memory
• Fully Abstract Models of Call-by-Value Languages, à la O'Hearn & Riecke
• Fully Abstract Models of Call-by-Value Languages, à la O'Hearn & Riecke
• Fully Abstract Models of Call-by-Value Languages, à la O'Hearn & Riecke
• Lovász' Theorem and Comonads in Finite Model Theory
• Free Commutative Monoids in Homotopy Type Theory
• Symmetric Arithmetic Circuits
• Axiomatic Concurrency Semantics for Full-Scale ARMv8-A using Symbolic Execution
• Incrementality xor currency for monotone fixed points
• Higher Algebra in Computer Science