![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Prateek Dwivedi (University of Copenhagen).
Friday 27 March 2026, 14:00-15:00
sb2743's list
A personal list of talks.
Contact: Siddharth Bhat
2 upcoming talks View 409 archived talks
Algorithms and Complexity Seminar
Non-Closure Properties of Read-Once Oblivious Algebraic Branching Programs
Formalisation of mathematics with interactive theorem provers
Faithful Logic Embeddings in HOL: Deep and Shallow, Propositional and Quantified
Formalisation of mathematics with interactive theorem provers
The Serre finiteness theorem in Cubical Agda
Formalisation of mathematics with interactive theorem provers
Certifying Synthetic Mathematics in Lean
Formalisation of mathematics with interactive theorem provers
HoTTLean: Semantics of HoTT in Lean
Algorithms and Complexity Seminar
Complexity in the Era of AI and Data-Driven Computing
Formalisation of mathematics with interactive theorem provers
Aristotle, an AI theorem prover using Lean
SANDWICH Seminar (Computer Laboratory)
ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
Formalisation of mathematics with interactive theorem provers
Lean4Less: Translating Lean to Smaller Theories via an Extensional-to-Intensional Translation
DPMMS Departmental Colloquia
Nonparametric inference under shape constraints: past, present and future
Quantum Computing Seminar
Cryptography, Distribution Verification, and Quantum Advantage
Formalisation of mathematics with interactive theorem provers
Integrating Formal and Informal Reasoning
SANDWICH Seminar (Computer Laboratory)
Decision procedures for parametric multi-width bitvectors
Archimedeans Talks MT25
Title to be confirmed
Formalisation of mathematics with interactive theorem provers
Combining Two Representations of Matrices for a Formalization of the Perron-Frobenius Theorem
Quantum Computing Seminar
Exploiting randomness in quantum algorithms
SANDWICH Seminar (Computer Laboratory)
Soteria and Compositional Symbolic Execution Γ la Carte
Archimedeans Talks MT25
Title to be confirmed
Formalisation of mathematics with interactive theorem provers
Human oriented tools for theorem proving in Lean
Archimedeans Talks MT25
Title to be confirmed
Formalisation of mathematics with interactive theorem provers
Lambda-Superposition for Successful Hammering
Algorithms and Complexity Seminar
The Karchmer-Raz-Wigderson Conjecture
Archimedeans Talks MT25
The generalised Fermat equation
Formalisation of mathematics with interactive theorem provers
A Lean Tactic to Automatically Generalize Proofs
Archimedeans Talks MT25
The Wave of Translation
Formalisation of mathematics with interactive theorem provers
Using interactive theorem provers in physics
Archimedeans Talks MT25
Infinite games
Formalisation of mathematics with interactive theorem provers
The Road to Formalising 8-Dimensional Sphere Packing in Lean
DPMMS Departmental Colloquia
Uniformity in arithmetic dynamics
Algorithms and Complexity Seminar
Monotone Circuit Complexity of Matching
Logic and Semantics Seminar (Computer Laboratory)
On Solution Discovery via Reconfiguration
Algorithms and Complexity Seminar
Proximity Gaps for Multilinear Interactive Oracle Proofs
Algorithms and Complexity Seminar
Extractors for Samplable Distributions from the Two-Source Extractor Recipe
Quantum Computing Seminar
Classical Commitments to Quantum States
Algorithms and Complexity Seminar
An Upper Bound on the Weisfeiler-Leman Dimension
Formalisation of mathematics with interactive theorem provers
Formalising the Multigraded Proj Construction in Lean 4
Quantum Computing Seminar
Learning shallow quantum circuits with many-qubit gates
Algorithms and Complexity Seminar
Expander decompositions
SANDWICH Seminar (Computer Laboratory)
Dependent Linear Type Theory via Bunched(less) Implications
SANDWICH Seminar (Computer Laboratory)
Confluence of Term Rewriting Systems with Variable Binding
SANDWICH Seminar (Computer Laboratory)
Executable Specification of a Production Hypervisor
SANDWICH Seminar (Computer Laboratory)
Type Checking is Proof Reductions in Classical Linear Logic
SANDWICH Seminar (Computer Laboratory)
SANDWICH Day
SANDWICH Seminar (Computer Laboratory)
An Invitation to Synthetic Domain Theory
Formalisation of mathematics with interactive theorem provers
Universal Diophantine Equations in Isabelle
SANDWICH Seminar (Computer Laboratory)
Automated Methods for Logic-Based Higher-Order Program Verification
Formalisation of mathematics with interactive theorem provers
Completeness Theorems for Variations of Higher-Order Logic
β οΈ CANCELLED
SANDWICH Seminar (Computer Laboratory)
Heyting Algebras and Higher-Order Logic
SANDWICH Seminar (Computer Laboratory)
PNVI-ae-udi: the last (most recent) C memory object model
Formalisation of mathematics with interactive theorem provers
Algebraic Geometry in Mathlib
SANDWICH Seminar (Computer Laboratory)
A Computer Architect's Attempt at Using Type Theoretic Concepts to Model Branch Predictors
Formalisation of mathematics with interactive theorem provers
Formalizing Fermat: an update
SANDWICH Seminar (Computer Laboratory)
Toward a liquid call-by-push-value
Algorithms and Complexity Seminar
Distribution Learning Meets Graph Structure Sampling
Algorithms and Complexity Seminar
Relaxed Locally Decodable and Correctable Codes Do Not Need Adaptivity and Two-Sided Error
Algorithms and Complexity Seminar
A super-linear lower bound for the iteration number of the Weisfeiler-Leman algorithm
SANDWICH Seminar (Computer Laboratory)
The 2-Category of Graded Monads
Formalisation of mathematics with interactive theorem provers
Verified Unsolvability of Temporal Planning
Algorithms and Complexity Seminar
Distinct Elements in Streams and the Klee's Measure Problem
SANDWICH Seminar (Computer Laboratory)
A Typed, Algebraic Approach to Parsing
Formalisation of mathematics with interactive theorem provers
Formal verification of the 5th Busy Beaver value
Quantum Computing Seminar
Classical and Quantum Algorithms for Characters of the Symmetric Group
Formalisation of mathematics with interactive theorem provers
Why do I write proofs?
β οΈ NOTE UNUSUAL DAY
Algorithms and Complexity Seminar
The Algebraic Circuit-Based Approach to Proof Complexity
Quantum Computing Seminar
The Role of piracy in quantum proofs
SANDWICH Seminar (Computer Laboratory)
Skew structure in categories
SANDWICH Seminar (Computer Laboratory)
Free algebras for free theories
Algorithms and Complexity Seminar
Zero-Knowledge in Streaming Interactive Proofs
Formalisation of mathematics with interactive theorem provers
Formalising Brauer Group and Group Cohomology in Lean4
SANDWICH Seminar (Computer Laboratory)
Closing the Gap between Transactional Consistency Models and Executable Code using Separation Logic
Formalisation of mathematics with interactive theorem provers
Algebraising foundations of elliptic curves
Quantum Computing Seminar
Symmetric Quantum Computation
SANDWICH Seminar (Computer Laboratory)
Generalised J rules and simultaneous pattern matching of equalities
Formalisation of mathematics with interactive theorem provers
Formalisation of Combinatorial Optimisation in Isabelle/HOL: Network Flows
SANDWICH Seminar (Computer Laboratory)
What does it take to certify a conversion checker?
Formalisation of mathematics with interactive theorem provers
Prospects for formalizing the theory of weak infinite-dimensional categories
Algorithms and Complexity Seminar
A stronger bound for linear 3-LCC
SANDWICH Seminar (Computer Laboratory)
The Denotational Semantics of SSA
Formalisation of mathematics with interactive theorem provers
Decision Procedures for Bitvector Reasoning in Lean
DPMMS Departmental Colloquia
The cutoff phenomenon for random walks
Algorithms and Complexity Seminar
Near-Optimal Alphabet Soundness Tradeoff PCPs
SANDWICH Seminar (Computer Laboratory)
Decision Procedures for Bitvector Reasoning in Lean
Quantum Computing Seminar
Interactive proofs for verifying (quantum) learning and testing
Algorithms and Complexity Seminar
Models that prove their own correctness
Quantum Computing Seminar
Quantum circuit lower bounds with entangled inputs
Formalisation of mathematics with interactive theorem provers
How to teach Fourier analysis to a large library of formalised mathematics
Quantum Computing Seminar
Deniable encryption in a quantum world
SANDWICH Seminar (Computer Laboratory)
Substitution, Normalization, and Formalization
Formalisation of mathematics with interactive theorem provers
Automatic Verification of BitVector Identities in SSA-Based Compiler IRs
Algorithms and Complexity Seminar
Dimension-free discretization inequalities with applications to low-degree learning
SANDWICH Seminar (Computer Laboratory)
Mixed Linear-Cartesian Theories as Substitution Monoids
Formalisation of mathematics with interactive theorem provers
Computer Algebra and the Formalisation of New Mathematics
SANDWICH Seminar (Computer Laboratory)
Unrolling Lists
Formalisation of mathematics with interactive theorem provers
Formalizing the divided power envelope in Lean
Discrete Analysis Seminar
Subgroup tests and the Aldous-Lyons conjecture
β οΈ Joint seminar: Discrete Analysis - Geometric Group Theory - Combinatorics - Quantum Computing - Algorithms and Complexity
SANDWICH Seminar (Computer Laboratory)
Do You Really Understand Incompleteness?
Formalisation of mathematics with interactive theorem provers
A tour in (formalised) type theory
SANDWICH Seminar (Computer Laboratory)
Executable Separation Logic Specifications in CN
Formalisation of mathematics with interactive theorem provers
Equational theories project: metatheorems and how to formalise them
SANDWICH Seminar (Computer Laboratory)
Toward a Coq formalisation of the Arm architecture
SANDWICH Seminar (Computer Laboratory)
On the Operational Theory of the CPS-Calculus
Formalisation of mathematics with interactive theorem provers
New Foundations: the story of a large formalisation project
SANDWICH Seminar (Computer Laboratory)
Traversing the Eckmann-Hilton Hyperclock
Algorithms and Complexity Seminar
Rate-1 Zero-Knowledge Proofs from One-Way Functions
Formalisation of mathematics with interactive theorem provers
Computer environments for math problem solving
Algorithms and Complexity Seminar
Homomorphism Indistinguishability: Characterisations, Closure, Complexity
Formalisation of mathematics with interactive theorem provers
Reasoning with Kan fillings about Morse reductions
DPMMS Departmental Colloquia
Functions with no critical points
SANDWICH Seminar (Computer Laboratory)
Some cool facts about dualities
Algorithms and Complexity Seminar
Low Degree Testing over the Reals
Quantum Computing Seminar
The quantum games PCP: results and confessions
Algorithms and Complexity Seminar
When and why do efficient algorithms exist (for constraint satisfaction and beyond)?
Formalisation of mathematics with interactive theorem provers
Alpha-Beta Pruning Explored, Extended and Verified
Algorithms and Complexity Seminar
From Query to Sequential Computation: A New Approach
Algorithms and Complexity Seminar
A strongly polynomial algorithm for the minimum-cost generalized flow problem
Formalisation of mathematics with interactive theorem provers
Little theories for big formal proofs
Algorithms and Complexity Seminar
Incompressibility and Next-Block Pseudoentropy
Formalisation of mathematics with interactive theorem provers
Teaching using a proof assistant and controlled natural language
Algorithms and Complexity Seminar
Perfect Zero-Knowledge PCPs for #P
Formalisation of mathematics with interactive theorem provers
Scientific Computing in Lean
Formalisation of mathematics with interactive theorem provers
Condensed Type Theory
Algorithms and Complexity Seminar
Polynomial-Time Pseudodeterministic Construction of Primes
Formalisation of mathematics with interactive theorem provers
Can a computer judge interestingness?
β οΈ (NOTE UNUSUAL DAY/TIME)
Formalisation of mathematics with interactive theorem provers
Formalising Theory of Combinatorial Optimisation
β οΈ Online
DPMMS Departmental Colloquia
When is a mathematical object well behaved?
Algorithms and Complexity Seminar
The Value of Errors in Proofs
Algorithms and Complexity Seminar
Understanding linear programming and the simplex algorithm
SciSoc β Cambridge University Scientific Society
Folding a Protein: Natureβs Origami
Formalisation of mathematics with interactive theorem provers
Lawvere Theories in Lean
β οΈ Online
Formalisation of mathematics with interactive theorem provers
Formalising (part of) the Diagonal Ramsey Paper
Formalisation of mathematics with interactive theorem provers
The Mandelbrot set is connected (and other Lean explorations)
Algorithms and Complexity Seminar
Space-Bounded Quantum State Testing via Space-Efficient Quantum Singular Value Transformation
Formalisation of mathematics with interactive theorem provers
Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
Formalisation of mathematics with interactive theorem provers
Structures in dependent type theory
β οΈ Online
Formalisation of mathematics with interactive theorem provers
How to prove Fermat's Last Theorem
β οΈ Online
Algorithms and Complexity Seminar
On Parallel Repetition of PCPs
Formalisation of mathematics with interactive theorem provers
Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean
SANDWICH Seminar (Computer Laboratory)
A Denotational Approach to Release/Acquire Concurrency
DPMMS Departmental Colloquia
Equidistribution and reciprocity in number theory
Formalisation of mathematics with interactive theorem provers
Towards Autoformalization and Mathematical Reasoning using language models
β οΈ Note unusual time
Quantum Fields and Strings Seminars
How Non-local is Quantum Gravity? (CANCELLED)
SANDWICH Seminar (Computer Laboratory)
Computing inverses in higher categories
SANDWICH Seminar (Computer Laboratory)
Type theoretic approaches to semistrictness
SANDWICH Seminar (Computer Laboratory)
Higher-Order Algebraic Effects and Handlers
SANDWICH Seminar (Computer Laboratory)
A couple of things Iβve learned about algebraically universal categories
DPMMS Departmental Colloquia
About random objects in the continuum
SANDWICH Seminar (Computer Laboratory)
Generic bidirectional typing for dependent type theories
SANDWICH Seminar (Computer Laboratory)
Definitional Functoriality for Dependent (Sub)Types
SANDWICH Seminar (Computer Laboratory)
Polymorphic Subtyping with Polarisation: β Β± β
Formalisation of mathematics with interactive theorem provers
Roth numbers: Upper, lower bounds, and related constructions
β οΈ Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalizing the change of variables formula for integrals in mathlib
β οΈ Hybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalizing algebraic number theory, recent progress and future challenges
β οΈ Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
The leanest automata
β οΈ Hybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalising ErdΕs and Larson: Ordinal Partition Theory
Formalisation of mathematics with interactive theorem provers
Explaining mathematics using formalized mathematics
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalization of diagram chasing as a first-order logic in Coq
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Smooth vector bundles in Lean
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean
Formalisation of mathematics with interactive theorem provers
The Locale-Centric Approach for Formalising Mathematical Hierarchies
Formalisation of mathematics with interactive theorem provers
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL
β οΈ [CANCELLED, please check back for rescheduling]
Formalisation of mathematics with interactive theorem provers
Formalising TurΓ‘n's Graph Theorem in Isabelle/HOL
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalisation of the BalogβSzemerΓ©diβGowers Theorem in Isabelle/HOL
Formalisation of mathematics with interactive theorem provers
From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics
Formalisation of mathematics with interactive theorem provers
Some practical problems in formalising mathematics and how to solve them
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
The Liquid Tensor Experiment
Formalisation of mathematics with interactive theorem provers
How Hilbert met Isabelle: Proof Between Generations
β οΈ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalised Mathematics: Obstacles and Achievements
DPMMS Conferences
Categorical Symplectic Topology Conference
DPMMS Conferences
Number Theory and Dynamics Conference 2019
DPMMS Departmental Colloquia
Discriminants: an interplay between algebra, combinatorics and geometry
DPMMS Conferences
British Algebraic Geometry meeting (BrAG)
DPMMS Conferences
British Algebraic Geometry meeting (BrAG)
DPMMS Conferences
British Algebraic Geometry meeting (BrAG)
DPMMS Conferences
Tutte Centenary Conference
DAMTP Departmental Seminar
Theoretical Implications of the Higgs Discovery
Computer Laboratory Automated Reasoning Group Lunches
Logic programming beyond Prolog
β οΈ This is a MSR Seminar (Station Road), duplicated on the ARG list
Computer Laboratory Automated Reasoning Group Lunches
Interfacing and improving proof tools
Semantics Lunch (Computer Laboratory)
Yet more animals: dynamic linkers and debuggers
Semantics Lunch (Computer Laboratory)
ABIs, linkers and other animals
Computer Laboratory Automated Reasoning Group Lunches
CakeML: A Verified Implementation of ML
Computer Laboratory Automated Reasoning Group Lunches
A Verified Bignum Implementation in x86-64 Machine Code
Computer Laboratory Automated Reasoning Group Lunches
Mathematical practice, crowdsourcing, and social machines
Semantics Lunch (Computer Laboratory)
POPL PC workshop
Computer Laboratory Automated Reasoning Group Lunches
Some unfinished projects
Computer Laboratory Automated Reasoning Group Lunches
Looking Back at Lyrebird
Computer Laboratory Automated Reasoning Group Lunches
Verified AIG Algorithms in ACL2
Computer Laboratory Automated Reasoning Group Lunches
A Formalisation of Finite Automata in Isabelle/HOL
Semantics Lunch (Computer Laboratory)
Sigma*: Symbolic Learning of Input-Output Specifications
Semantics Lunch (Computer Laboratory)
High-Level Separation Logic for Low-Level Code
Semantics Lunch (Computer Laboratory)
Library Abstraction for C/C++ Concurrency
Semantics Lunch (Computer Laboratory)
Full Abstraction for PCF with Names
Semantics Lunch (Computer Laboratory)
A Model-Learner Pattern for Bayesian Reasoning
Semantics Lunch (Computer Laboratory)
Putting the thrill back into computing at school
Semantics Lunch (Computer Laboratory)
On distributed probabilistic strategies
Semantics Lunch (Computer Laboratory)
The Power of Parameterization in Coinductive Proof
β οΈ This will be the first Semantics Lunch of the term - please do come along (or email Peter.Sewell@cl.cam.ac.uk) with offers of talks.
Semantics Lunch (Computer Laboratory)
Containers, Comonads and Distributive Laws
Computer Laboratory Automated Reasoning Group Lunches
Semi-automatic Algorithm Synthesis (Case Study: Square Root)
Semantics Lunch (Computer Laboratory)
Ribbon Proofs for Separation Logic
Computer Laboratory Automated Reasoning Group Lunches
Diabelli and Speedith: Heterogeneous reasoning and spider diagrams
Semantics Lunch (Computer Laboratory)
A Concurrent Logical Relation
β οΈ NB: changed (again!) unusual day/time
Computer Laboratory Automated Reasoning Group Lunches
Holfoot - a separation logic tool in HOL4
Semantics Lunch (Computer Laboratory)
Virtue of certified programming with decision procedures
β οΈ NB: unusual day/time
Semantics Lunch (Computer Laboratory)
From threads to events through classical program transformations
β οΈ NB: Unusual day/time
Computer Laboratory Automated Reasoning Group Lunches
Diabelli: a framework for heterogeneous reasoning
Computer Laboratory Automated Reasoning Group Lunches
Proof-Producing Synthesis of ML from Higher-Order Logic
Computer Laboratory Automated Reasoning Group Lunches
Extending deforestation
Computer Laboratory Automated Reasoning Group Lunches
A Proposed Framework for Analysing Security Ceremonies
Semantics Lunch (Computer Laboratory)
Developing verified programs in Dafny
Computer Laboratory Automated Reasoning Group Lunches
Bottom-up formalization of the ARM architecture
Semantics Lunch (Computer Laboratory)
RESCHEDULED to 20th Feb: GPUVerify: a modular verifier for GPU kernels
Computer Laboratory Automated Reasoning Group Lunches
Explicit vs. symbolic algorithms for solving ALFP constraints
Computer Laboratory Automated Reasoning Group Lunches
Plan B: A Buffered Memory Model for Java
Semantics Lunch (Computer Laboratory)
Resource Sensitive Synchronisation Inference by Abduction
Semantics Lunch (Computer Laboratory)
Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER
Semantics Lunch (Computer Laboratory)
Stop when you are Almost-Full: Adventures in Constructive Termination
Semantics Lunch (Computer Laboratory)
Understanding POWER Multiprocessors
Computer Laboratory Automated Reasoning Group Lunches
Modular verification of preemptive OS kernels
Semantics Lunch (Computer Laboratory)
The Importance of Being Linearizable
Computer Laboratory Automated Reasoning Group Lunches
On the Strength of Owicki-Gries for Resources
Semantics Lunch (Computer Laboratory)
A Heirarchy of Mendler style Iteration/Recursion Combinators: taming recursive types with negative occurrences
Computer Laboratory Automated Reasoning Group Lunches
Discovery of Invariants through Automated Theory Formation
Semantics Lunch (Computer Laboratory)
Semantics of a DNA Strand Displacement Model
Semantics Lunch (Computer Laboratory)
Ribbon proofs for separation logic
Computer Laboratory Automated Reasoning Group Lunches
Zeno: An automated theorem prover for functional programs
Semantics Lunch (Computer Laboratory)
TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs
Semantics Lunch (Computer Laboratory)
Relating Two Semantics of Locally Scoped Names
β οΈ Note unusual day, time and place: this will be in the ARG lunch slot
Computer Laboratory Automated Reasoning Group Lunches
Nitpicking C++ Concurrency
Semantics Lunch (Computer Laboratory)
Polarisation in classical realisability and delimited control
β οΈ NOTE UNUSUAL TIME AND PLACE
Computer Laboratory Automated Reasoning Group Lunches
Work in progress: a prototype refactoring tool based on a mechanically-verified core
Computer Laboratory Automated Reasoning Group Lunches
How do I know my GPU or multicore floating point computations are correct?
Computer Laboratory Automated Reasoning Group Lunches
Separation Algebra
Computer Laboratory Automated Reasoning Group Lunches
Title to be confirmed
Semantics Lunch (Computer Laboratory)
Composable Asynchronous Events/Formal Methods for Wireless Mesh Networks
β οΈ Note unusual start time: talks at 12.50 prompt
Computer Laboratory Automated Reasoning Group Lunches
A verified runtime for a verified theorem prover
Computer Laboratory Automated Reasoning Group Lunches
Using the Cambridge ARM model to verify the concrete machine code of seL4
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Computer Laboratory Automated Reasoning Group Lunches
Validating QBF Validity in HOL4
Computer Laboratory Automated Reasoning Group Lunches
Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers
Computer Laboratory Automated Reasoning Group Lunches
Rough-and-ready proof reconstruction
Computer Laboratory Automated Reasoning Group Lunches
The Strategy Challenge in Computer Algebra
Computer Laboratory Automated Reasoning Group Lunches
Formalizing Metarouting
Computer Laboratory Automated Reasoning Group Lunches
Quantifier Heuristics in HOL4
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Semantics Lunch (Computer Laboratory)
Relaxed-Memory Concurrency and Verified Compilation / Mathematizing C++0x concurrency
Semantics Lunch (Computer Laboratory)
Logics with algebraic operators
Semantics Lunch (Computer Laboratory)
Formalizing Domains, Ultrametric Spaces and Semantics of Programming Languages
Computer Laboratory Automated Reasoning Group Lunches
Evaluating Formulas on Graphs
Semantics Lunch (Computer Laboratory)
Making Prophecies with Decision Predicates
Computer Laboratory Automated Reasoning Group Lunches
First prototype of an Isabelle/HOL-to-LeoII interface
Semantics Lunch (Computer Laboratory)
Relaxed-Memory Concurrency and Verified Compilation
Computer Laboratory Automated Reasoning Group Lunches
Mirage
Semantics Lunch (Computer Laboratory)
A Language for Mathematics
Computer Laboratory Automated Reasoning Group Lunches
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions
Semantics Lunch (Computer Laboratory)
Andrew Kennedy
β οΈ POSTPONED - no Semantics Lunch meeting this week
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Analog Designs using MetiTarski
Semantics Lunch (Computer Laboratory)
Finding best paths in difficult conditions
β οΈ (Change of speaker - this replaces Eric's talk)
Computer Laboratory Automated Reasoning Group Lunches
Bit-blasting in HOL4
Semantics Lunch (Computer Laboratory)
Separation Logic and Graphical Models
Computer Laboratory Automated Reasoning Group Lunches
A Simple and Efficient Memory Model for Concurrent Programming Languages
Semantics Lunch (Computer Laboratory)
Mathematizing C++ Concurrency
Computer Laboratory Automated Reasoning Group Lunches
Schedulability analysis of embedded real-time Java
Semantics Lunch (Computer Laboratory)
Let should not be generalised
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Semantics Lunch (Computer Laboratory)
Abstract separation algebra
Semantics Lunch (Computer Laboratory)
Concurrent abstract predicates
Semantics Lunch (Computer Laboratory)
Interoperability in a Scripted World
Semantics Lunch (Computer Laboratory)
Probabilistic languages for inference
Semantics Lunch (Computer Laboratory)
Higher order reactive programming
Semantics Lunch (Computer Laboratory)
Proving safety of asynchronous multi-core programs
Semantics Lunch (Computer Laboratory)
Hoopl: modular library for dataflow analysis/transformation
Semantics Lunch (Computer Laboratory)
Every bit counts
Computer Laboratory Automated Reasoning Group Lunches
A Mechanically Verified AIG-to-BDD Conversion Algorithm
Semantics Lunch (Computer Laboratory)
Linear maps
Computer Laboratory Automated Reasoning Group Lunches
General Binding in Nominal Isabelle 2
Computer Laboratory Automated Reasoning Group Lunches
Validating QBF Invalidity in HOL4
Computer Laboratory Automated Reasoning Group Lunches
Local Reasoning about While-Loops
Computer Laboratory Automated Reasoning Group Lunches
Verification of a copying garbage collector
Semantics Lunch (Computer Laboratory)
A polarised calculus of delimited control
Computer Laboratory Automated Reasoning Group Lunches
Title to be confirmed
β οΈ Canceled because of date clash with HCSS and workshop at MSR
Computer Laboratory Automated Reasoning Group Lunches
Formal models of ARM processors in HOL
β οΈ Presenters: Mike Gordon and Anthony Fox / This is a rehearsal of our HCSS talk on May 11
Computer Laboratory Automated Reasoning Group Lunches
From Counter Abstraction to Thread-State Cutoffs: New Techniques for Multi-Threaded Program Verification
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Semantics Lunch (Computer Laboratory)
New frontiers for Linear Temporal Logic
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Analog and Mixed Signal Designs
Semantics Lunch (Computer Laboratory)
The Thorn Programming Language: Robust Distributed Scripting
Computer Laboratory Automated Reasoning Group Lunches
Interfacing two similar HOLs
Computer Laboratory Automated Reasoning Group Lunches
Integration of SMT Solvers with ITPs - There and Back Again
Computer Laboratory Automated Reasoning Group Lunches
Verification of Multicast Protocols
Computer Laboratory Automated Reasoning Group Lunches
A New Version of Nominal Isabelle
Computer Laboratory Automated Reasoning Group Lunches
Holfoot - A separation logic tools inside HOL 4
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Computer Laboratory Automated Reasoning Group Lunches
Verified just-in-time compiler on x86
β οΈ Notice changed date
Computer Laboratory Automated Reasoning Group Lunches
jStar: Towards Practical Verification for Java
Semantics Lunch (Computer Laboratory)
Coarse-grained transactions
Computer Laboratory Automated Reasoning Group Lunches
New tools in HOL 4 - Consequence Conversions, Quantifier Heuristics, Styles
β οΈ Notice change of speaker
Semantics Lunch (Computer Laboratory)
A refinement of the state monad
Computer Laboratory Automated Reasoning Group Lunches
SMT Solvers: New Oracles for the HOL Theorem Prover
Semantics Lunch (Computer Laboratory)
Completeness for algebraic theories of local state
Computer Laboratory Automated Reasoning Group Lunches
Abstract Threads
β οΈ th orginally sheduled talk by Thomas Tuerk will probably be given next term
Semantics Lunch (Computer Laboratory)
Structural recursion with pure local names
Semantics Lunch (Computer Laboratory)
Dependent types and program equivalence
Computer Laboratory Automated Reasoning Group Lunches
A formal system for Euclidean diagrammatic reasoning
Semantics Lunch (Computer Laboratory)
Verifying malloc using RGSep and 'Explicit Stabilisation'
Computer Laboratory Automated Reasoning Group Lunches
Owicki-Gries, Thread-Modular Model-Checking, Cartesian Abstraction
Semantics Lunch (Computer Laboratory)
Locality and Footprints in Separation Logic
Computer Laboratory Automated Reasoning Group Lunches
High-Assurance(?) High-Frequency Trading
Semantics Lunch (Computer Laboratory)
F^o: Lightweight Linear F
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Semantics Lunch (Computer Laboratory)
Integration of Typed and Untyped Code in a Scripting Language
Computer Laboratory Automated Reasoning Group Lunches
Verified LISP implementations on ARM, x86 and PowerPC / A HOL Formalisation of Smallfoot
Computer Laboratory Automated Reasoning Group Lunches
Why you can't even trust HOL, and what to do about it
Semantics Lunch (Computer Laboratory)
Higher Order Actions in Deny-Guarantee
Semantics Lunch (Computer Laboratory)
Program Verification and Synthesis over Predicate Abstraction
Semantics Lunch (Computer Laboratory)
Reliable evidence: Auditability by typing
Semantics Lunch (Computer Laboratory)
A Ubiquitous Abstract Machine
Computer Laboratory Automated Reasoning Group Lunches
Solving HOL problems using FOL tools
Computer Laboratory Automated Reasoning Group Lunches
Verifying Flash Device Drivers
Semantics Lunch (Computer Laboratory)
Towards parametric direcursion: structured mixed-variant recursion with parameters
Computer Laboratory Automated Reasoning Group Lunches
Automatic Reverse Engineering for Formal Verification
Semantics Lunch (Computer Laboratory)
Scheduling meeting
Computer Laboratory Automated Reasoning Group Lunches
Free to a good home: an advertisement for the "new" HOL4 theories of probability, integration, and information. / A Heap of Problems
Computer Laboratory Automated Reasoning Group Lunches
Mechanically Proving Hoare Formulae
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Semantics Lunch (Computer Laboratory)
A unifying model for computational objects
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Centaur Technology's X86-Compatible Media Unit
Semantics Lunch (Computer Laboratory)
Strongly-typed term representations in Coq
Semantics Lunch (Computer Laboratory)
Segment logic (work in progress)
Computer Laboratory Automated Reasoning Group Lunches
A Verifiable, Executable SLR Parser
Computer Laboratory Automated Reasoning Group Lunches
A Theory of Type-directed Coercion Insertion
β οΈ Note change of date
Semantics Lunch (Computer Laboratory)
Biorthogonality, step-indexing and compiler correctness
Computer Laboratory Automated Reasoning Group Lunches
Semantics Lunch
β οΈ Canceled, semantics lunch instead
Semantics Lunch (Computer Laboratory)
Deny-guarantee reasoning
β οΈ NOTE THE UNUSUAL DAY AND VENUE. This talk is in the ARG lunch slot.
Semantics Lunch (Computer Laboratory)
Resolving inductive definitions with binders
Computer Laboratory Automated Reasoning Group Lunches
Modular verification of concurrent programs with heap
β οΈ Mike Hick's talk moved to the 17th of March
Semantics Lunch (Computer Laboratory)
A Framework for Specification, Prototyping, and Reasoning
Computer Laboratory Automated Reasoning Group Lunches
Formal power series in Isabelle/HOL
Semantics Lunch (Computer Laboratory)
Logics with Rank Operators
Computer Laboratory Automated Reasoning Group Lunches
RGSep action inference
Semantics Lunch (Computer Laboratory)
Semantics lunch organisational meeting
Computer Laboratory Automated Reasoning Group Lunches
Verifying Distributed Systems: the Operational Approach
Computer Laboratory Automated Reasoning Group Lunches
Finite Model Generation, Proof-Producing SAT Solvers, and SMT
Computer Laboratory Automated Reasoning Group Lunches
A HOL Formalisation of Smallfoot
Computer Laboratory Automated Reasoning Group Lunches
Title to be confirmed
β οΈ Canceled because of POPL
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Semantics Lunch (Computer Laboratory)
Secure Compilation of a Multi-Tier
Computer Laboratory Automated Reasoning Group Lunches
An ACL2 Tutorial
Semantics Lunch (Computer Laboratory)
Title to be confirmed
Computer Laboratory Automated Reasoning Group Lunches
The Semantics of x86-CC Multiprocessor Machine Code
Semantics Lunch (Computer Laboratory)
Convergence of path-finding
Computer Laboratory Automated Reasoning Group Lunches
Techniques for Symbolic Complexity Bounds
Semantics Lunch (Computer Laboratory)
Compiling Functional Types to Relational Specifications for Low Level Imperative Code
Computer Laboratory Automated Reasoning Group Lunches
Mechanically verified LISP interpreters
β οΈ Note unusual time
Semantics Lunch (Computer Laboratory)
Some notes on syntactic logical relations for pure System F
Computer Laboratory Automated Reasoning Group Lunches
Proving recursive programs terminating
Semantics Lunch (Computer Laboratory)
Deny-guarantee reasoning
Computer Laboratory Automated Reasoning Group Lunches
Towards Automatic Stability Analysis for Rely-Guarantee Proofs
Semantics Lunch (Computer Laboratory)
Focusing on Pattern Matching
Computer Laboratory Automated Reasoning Group Lunches
The Mechanical Formalization of Measure, Integration and Probability
Semantics Lunch (Computer Laboratory)
An Invitation to Nominal Domain Theory
Computer Laboratory Automated Reasoning Group Lunches
Applications of MetiTarski in the Verification of Control and Hybrid Systems
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Computer Laboratory Automated Reasoning Group Lunches
Formal Methods for Critical Systems
Computer Laboratory Automated Reasoning Group Lunches
Diagrammatic Reasoning in Separation Logic
Computer Laboratory Automated Reasoning Group Lunches
ACL2-Based Verification of NoC Communication Infrastructures
Computer Laboratory Automated Reasoning Group Lunches
The Relative Consistency of the Axiom of Choice, Mechanized Using Isabelle/ZF
Computer Laboratory Automated Reasoning Group Lunches
Proving Liveness Properties of Non-blocking Data Structures
Computer Laboratory Automated Reasoning Group Lunches
Proof-producing decompilation and compilation
β οΈ Room changed
Computer Laboratory Automated Reasoning Group Lunches
Proving conditional termination
Computer Laboratory Automated Reasoning Group Lunches
Applying Machine Learning to Heuristic Selection in an Automated Theorem Prover
Computer Laboratory Automated Reasoning Group Lunches
Information, Anonymity, and Proof
Computer Laboratory Automated Reasoning Group Lunches
LCF-style Propositional Simplification With BDDs and SAT Solvers
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Computer Laboratory Automated Reasoning Group Lunches
A Constraint-Programming Framework For Bounded Program Verification
Computer Laboratory Automated Reasoning Group Lunches
Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II
Computer Laboratory Automated Reasoning Group Lunches
Some "Real World" Problems in the Analog and Mixed Signal Domains
Computer Laboratory Automated Reasoning Group Lunches
An Embedding of Abstract Separation Logic in HOL
Computer Laboratory Automated Reasoning Group Lunches
A rigorous approach to networking: TCP, from implementation to protocol to service
Computer Laboratory Automated Reasoning Group Lunches
Automatic Proof for Theorems On Transcendental Functions
Computer Laboratory Automated Reasoning Group Lunches
MaLARea: a Metasystem for Automated Reasoning in Large Theories
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Computer Laboratory Automated Reasoning Group Lunches
Automatic proof of SPARK verification conditions
Computer Laboratory Automated Reasoning Group Lunches
n-bit words in HOL
Computer Laboratory Automated Reasoning Group Lunches
Proving Correctness of Secret Sharing Protocols using the Inductive Method
Computer Laboratory Automated Reasoning Group Lunches
From Program Logics to Program Analyses And Back
Computer Laboratory Automated Reasoning Group Lunches
Reasoning about Linear Systems
Computer Laboratory Automated Reasoning Group Lunches
Synthesis from Temporal Specifications
Computer Laboratory Automated Reasoning Group Lunches
A tool for verification: A decompiler from ARM to HOL
Computer Laboratory Automated Reasoning Group Lunches
A modular formalisation of finite group theory
Computer Laboratory Automated Reasoning Group Lunches
Executable Biology: Towards Computer Programs that Mimic Life
Computer Laboratory Automated Reasoning Group Lunches
Introductiory Meeting
Computer Laboratory Automated Reasoning Group Lunches
Verifying an Operating System Kernel
β οΈ Room changed
Computer Laboratory Automated Reasoning Group Lunches
Boosting Verification by Automatic Tuning of Decision Procedures
Computer Laboratory Automated Reasoning Group Lunches
Cryptanalysis with SAT - a propositional programming environment
β οΈ Room changed
Computer Laboratory Automated Reasoning Group Lunches
One-pass Tableaux for Computation Tree Logic
β οΈ Room changed
Computer Laboratory Automated Reasoning Group Lunches
Progress Report on Leo-II, an Automatic Theorem Prover for Higher-Order Logic
Computer Laboratory Automated Reasoning Group Lunches
A Deep Embedding of a Decidable Fragment of Separation Logic in HOL
Computer Laboratory Automated Reasoning Group Lunches
The ARM Cortex-M1 Architecture in Coq
Computer Laboratory Automated Reasoning Group Lunches
From QED to X-Logic, following the lead of Leibniz
Computer Laboratory Automated Reasoning Group Lunches
Connecting Partial and Total Correctness for Probabilistic Programs in HOL4
Computer Laboratory Automated Reasoning Group Lunches
A Compressing Translation from Propositional Resolution to Natural Deduction
Computer Laboratory Automated Reasoning Group Lunches
Local Reasoning for Storable Locks and Threads
Please see above for contact details for this list.