![[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
Computer Laboratory, William Gates Building, Room SS03
Contact: No managers listed
0 upcoming talks View 234 archived talks
Algorithms and Complexity Seminar
Non-Closure Properties of Read-Once Oblivious Algebraic Branching Programs
Quantum Computing Seminar
Cryptography, Distribution Verification, and Quantum Advantage
Quantum Computing Seminar
Exploiting randomness in quantum algorithms
compiler socials
Full Stack Verification of CHERI systems
Algorithms and Complexity Seminar
The Karchmer-Raz-Wigderson Conjecture
Algorithms and Complexity Seminar
Monotone Circuit Complexity of Matching
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
Quantum Computing Seminar
Learning shallow quantum circuits with many-qubit gates
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
Algorithms and Complexity Seminar
Distinct Elements in Streams and the Klee's Measure Problem
Algorithms and Complexity Seminar
The Algebraic Circuit-Based Approach to Proof Complexity
Quantum Computing Seminar
The Role of piracy in quantum proofs
Algorithms and Complexity Seminar
Zero-Knowledge in Streaming Interactive Proofs
Quantum Computing Seminar
Deniable encryption in a quantum world
Algorithms and Complexity Seminar
Dimension-free discretization inequalities with applications to low-degree learning
Algorithms and Complexity Seminar
Homomorphism Indistinguishability: Characterisations, Closure, Complexity
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
sb2743's list
Shoggoth: A Formal Foundation for Strategic Rewriting
Algorithms and Complexity Seminar
Perfect Zero-Knowledge PCPs for #P
Algorithms and Complexity Seminar
Polynomial-Time Pseudodeterministic Construction of Primes
sb2743's list
Fully in-Place Functional Programming
Women@CL Events
Women@CL Talklet Event
Computer Laboratory NetOS Group Talklets
Maru: A joint project with ATI and Imperial
Computer Laboratory NetOS Group Talklets
TBC
Computer Laboratory Security Group meeting presentations
Pico prototype
Computer Laboratory Security Group meeting presentations
Pico: user authentication for Internet of Things
Computer Laboratory Security Group meeting presentations
Informal talk about Wassenaar and/or work at our lab
Computer Laboratory Automated Reasoning Group Lunches
Interfacing and improving proof tools
Computer Laboratory Security Group meeting presentations
Discussion on AG's recent Opinion concerning the Data Retention Directive
β οΈ Note change of room to SS03 (for this day only)
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
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
Computer Laboratory Automated Reasoning Group Lunches
Semi-automatic Algorithm Synthesis (Case Study: Square Root)
Computer Laboratory Automated Reasoning Group Lunches
Diabelli and Speedith: Heterogeneous reasoning and spider diagrams
Computer Laboratory Automated Reasoning Group Lunches
Holfoot - a separation logic tool in HOL4
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
Computer Laboratory Automated Reasoning Group Lunches
Bottom-up formalization of the ARM architecture
Computer Laboratory Automated Reasoning Group Lunches
Explicit vs. symbolic algorithms for solving ALFP constraints
Computer Laboratory Automated Reasoning Group Lunches
Modular verification of preemptive OS kernels
Computer Laboratory Automated Reasoning Group Lunches
On the Strength of Owicki-Gries for Resources
Computer Laboratory Automated Reasoning Group Lunches
Discovery of Invariants through Automated Theory Formation
Computer Laboratory Automated Reasoning Group Lunches
Zeno: An automated theorem prover for functional programs
Rainbow Graphics Seminars
Predicting stereoscopic viewing comfort
Computer Laboratory Automated Reasoning Group Lunches
Nitpicking C++ Concurrency
Rainbow Interaction Seminars
Withdrawing from Exhibits: the interactional organisation of museum visits
Computer Laboratory Automated Reasoning Group Lunches
Work in progress: a prototype refactoring tool based on a mechanically-verified core
Rainbow Interaction Seminars
First-year research presentations
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
Computer Laboratory Automated Reasoning Group Lunches
A verified runtime for a verified theorem prover
Rainbow Interaction Seminars
Joint talks on technology for mental health interventions
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
Rainbow Graphics Seminars
MPhil ACS Project Progress Presentation
Computer Laboratory Automated Reasoning Group Lunches
Validating QBF Validity in HOL4
Rainbow Graphics Seminars
Work I did at the MPI Informatik
Computer Laboratory Automated Reasoning Group Lunches
Heterogeneous Proofs: Spider Diagrams meet Higher-Order Provers
Rainbow Graphics Seminars
A trip to Silicon Valley: animated movies and 3D displays
Computer Laboratory Automated Reasoning Group Lunches
Rough-and-ready proof reconstruction
Rainbow Interaction Seminars
Third Wave HCI & Gestural Interaction
Computer Laboratory Automated Reasoning Group Lunches
The Strategy Challenge in Computer Algebra
Rainbow Graphics Seminars
Title to be confirmed
Computer Laboratory Automated Reasoning Group Lunches
Formalizing Metarouting
Rainbow Graphics Seminars
Cubic Subdivision Schemes with Double Knots
Rainbow Graphics Seminars
Part II Student Project Presentation
Computer Laboratory Automated Reasoning Group Lunches
Quantifier Heuristics in HOL4
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Rainbow Interaction Seminars
Facilitating non-verbal communication with robots: synthesis and perception with applications for clinical communication
Computer Laboratory Automated Reasoning Group Lunches
Evaluating Formulas on Graphs
Rainbow Interaction Seminars
Learning and generating techno music: a machine learning approach
Computer Laboratory Automated Reasoning Group Lunches
First prototype of an Isabelle/HOL-to-LeoII interface
Rainbow Interaction Seminars
Notes on the Synthesis of Music
Computer Laboratory Automated Reasoning Group Lunches
Mirage
Rainbow Interaction Seminars
Conference summary
Computer Laboratory Automated Reasoning Group Lunches
A Formalisation of the Myhill-Nerode Theorem based on Regular Expressions
Rainbow Interaction Seminars
Sketching Language β User-Centred Design of a Wizard of Oz Prototyping Tool
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Analog Designs using MetiTarski
Rainbow Interaction Seminars
Usable Programming Language Design in Industry and Academia
Computer Laboratory Automated Reasoning Group Lunches
Bit-blasting in HOL4
Rainbow Graphics Seminars
"What I did in the summer"
Computer Laboratory Automated Reasoning Group Lunches
A Simple and Efficient Memory Model for Concurrent Programming Languages
Rainbow Interaction Seminars
Synthesizing Expressions using Facial Feature Point Tracking: How Emotion is Conveyed
Computer Laboratory Automated Reasoning Group Lunches
Schedulability analysis of embedded real-time Java
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
djg11's list
Concurrency and Communication: Lessons from the SHIM Project
β οΈ (Re-run of talk given at MSR two weeks ago)
Computer Laboratory Automated Reasoning Group Lunches
A Mechanically Verified AIG-to-BDD Conversion Algorithm
Rainbow Graphics Seminars
MPhil demos
Computer Laboratory Automated Reasoning Group Lunches
General Binding in Nominal Isabelle 2
Rainbow Interaction Seminars
Interactive music technology - demo session
Computer Laboratory Automated Reasoning Group Lunches
Validating QBF Invalidity in HOL4
Rainbow Interaction Seminars
Coded Chimera: exploring relationships between sculptural form making and biological morphogenesis through computer modeling
Computer Laboratory Automated Reasoning Group Lunches
Local Reasoning about While-Loops
Rainbow Interaction Seminars
MetaSurfacing with the Surface: experience with integrated research environments
Computer Laboratory Automated Reasoning Group Lunches
Verification of a copying garbage collector
Rainbow Graphics Seminars
Eurographics Report
Computer Laboratory Automated Reasoning Group Lunches
Title to be confirmed
β οΈ Canceled because of date clash with HCSS and workshop at MSR
Rainbow Interaction Seminars
CHI report
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
Rainbow Graphics Seminars
3DTV: past, present & future
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
Computer Laboratory Opera Group Seminars
Decentralised Event Flow Control
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Analog and Mixed Signal Designs
Rainbow Interaction Seminars
Designing technologies for support mental health interventions
Computer Laboratory Automated Reasoning Group Lunches
Interfacing two similar HOLs
Rainbow Interaction Seminars
Part II Project Presentations
Computer Laboratory Automated Reasoning Group Lunches
Integration of SMT Solvers with ITPs - There and Back Again
Rainbow Interaction Seminars
Part II Project Presentations
Computer Laboratory Automated Reasoning Group Lunches
Verification of Multicast Protocols
Rainbow Interaction Seminars
Report on ACM IUI 2010 and IEEE IHCI 2010
Computer Laboratory Automated Reasoning Group Lunches
A New Version of Nominal Isabelle
Rainbow Interaction Seminars
Subdivision surfaces and the dolphin problem
Rainbow Interaction Seminars
Collaborative control for a robotic wheelchair
Computer Laboratory Automated Reasoning Group Lunches
Holfoot - A separation logic tools inside HOL 4
Rainbow Interaction Seminars
Term Planning
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
Computer Laboratory Automated Reasoning Group Lunches
Verified just-in-time compiler on x86
β οΈ Notice changed date
Rainbow Interaction Seminars
What's in the eyes for context-awareness?
Computer Laboratory Automated Reasoning Group Lunches
jStar: Towards Practical Verification for Java
Rainbow Interaction Seminars
Supporting Virtuosity in Computer Music
Computer Laboratory Automated Reasoning Group Lunches
New tools in HOL 4 - Consequence Conversions, Quantifier Heuristics, Styles
β οΈ Notice change of speaker
Rainbow Graphics Seminars
Title to be confirmed
Computer Laboratory Automated Reasoning Group Lunches
SMT Solvers: New Oracles for the HOL Theorem Prover
Rainbow Interaction Seminars
WebSurface: an Interface for Co-located Collaborative Information Gathering
Computer Laboratory Automated Reasoning Group Lunches
Abstract Threads
β οΈ th orginally sheduled talk by Thomas Tuerk will probably be given next term
Rainbow Interaction Seminars
The Embodied Cognition and Emotion Laboratory: What We Do
Rainbow Interaction Seminars
Synchrony and Entrainment in Human Interaction
Computer Laboratory Automated Reasoning Group Lunches
A formal system for Euclidean diagrammatic reasoning
Rainbow Interaction Seminars
Crossing the digital divide, making emotional connections with digital characters
Computer Laboratory Automated Reasoning Group Lunches
Owicki-Gries, Thread-Modular Model-Checking, Cartesian Abstraction
Computer Laboratory Automated Reasoning Group Lunches
High-Assurance(?) High-Frequency Trading
Computer Laboratory Automated Reasoning Group Lunches
Introductory meeting
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
Computer Laboratory Automated Reasoning Group Lunches
Solving HOL problems using FOL tools
Computer Laboratory Automated Reasoning Group Lunches
Verifying Flash Device Drivers
Computer Laboratory Automated Reasoning Group Lunches
Automatic Reverse Engineering for Formal Verification
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
Computer Laboratory Automated Reasoning Group Lunches
Formal Verification of Centaur Technology's X86-Compatible Media Unit
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
Computer Laboratory Automated Reasoning Group Lunches
Semantics Lunch
β οΈ Canceled, semantics lunch instead
Rainbow Interaction Seminars
Design dimensions of mobile text entry
Computer Laboratory Automated Reasoning Group Lunches
Modular verification of concurrent programs with heap
β οΈ Mike Hick's talk moved to the 17th of March
Rainbow Interaction Seminars
Empathizing with Robots
Computer Laboratory Automated Reasoning Group Lunches
Formal power series in Isabelle/HOL
Computer Laboratory Automated Reasoning Group Lunches
RGSep action inference
Rainbow Graphics Seminars
Part II Student Presentations (Part 2 of 2)
Computer Laboratory Automated Reasoning Group Lunches
Verifying Distributed Systems: the Operational Approach
Rainbow Graphics Seminars
Part II Student Presentations (Part 1 of 2)
Computer Laboratory Automated Reasoning Group Lunches
Finite Model Generation, Proof-Producing SAT Solvers, and SMT
Rainbow Interaction Seminars
Multimodal Affective Inference for Driver Monitoring
Computer Laboratory Automated Reasoning Group Lunches
A HOL Formalisation of Smallfoot
Rainbow Graphics Seminars
Current Work Pitches
Computer Laboratory Automated Reasoning Group Lunches
Title to be confirmed
β οΈ Canceled because of POPL
Rainbow Graphics Seminars
Term planning
Computer Laboratory Automated Reasoning Group Lunches
Introductory Meeting
Computer Laboratory Automated Reasoning Group Lunches
An ACL2 Tutorial
Computer Laboratory Automated Reasoning Group Lunches
The Semantics of x86-CC Multiprocessor Machine Code
Computer Laboratory Automated Reasoning Group Lunches
Techniques for Symbolic Complexity Bounds
Computer Laboratory Automated Reasoning Group Lunches
Mechanically verified LISP interpreters
β οΈ Note unusual time
Computer Laboratory Automated Reasoning Group Lunches
Proving recursive programs terminating
Computer Laboratory Automated Reasoning Group Lunches
Towards Automatic Stability Analysis for Rely-Guarantee Proofs
Computer Laboratory Automated Reasoning Group Lunches
The Mechanical Formalization of Measure, Integration and Probability
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
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
Rainbow Interaction Seminars
Modelling user interfaces for special needs
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
Rainbow Interaction Seminars
Co-located Group Interaction Design
Computer Laboratory Automated Reasoning Group Lunches
An Embedding of Abstract Separation Logic in HOL
Rainbow Interaction Seminars
Designing Playful Programming β Some challenges
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
Rainbow Interaction Seminars
Presentations of part II projects
Rainbow Interaction Seminars
How to review a technical paper
Computer Laboratory Automated Reasoning Group Lunches
MaLARea: a Metasystem for Automated Reasoning in Large Theories
Rainbow Interaction Seminars
Lent Term Kickoff Meeting
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
Rainbow Interaction Seminars
Investigating Collaboration around the TableTop
Computer Laboratory Automated Reasoning Group Lunches
From Program Logics to Program Analyses And Back
Wireless Communications Team Seminars
Optimum resource allocation in MIMO systems: An information theoretic-estimation theoretic approach
Rainbow Interaction Seminars
Affective Driver Monitoring Systems
Computer Laboratory Automated Reasoning Group Lunches
Reasoning about Linear Systems
Rainbow Interaction Seminars
Designing for Telepresence: An Introduction To Physical Avatar 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
Rainbow Interaction Seminars
Detecting Affect from Non-stylised body motions
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
Rainbow Interaction Seminars
Meet Rainbow
Computer Laboratory Automated Reasoning Group Lunches
Introductiory Meeting
Rainbow Interaction Seminars
Distributed Tabletops: Supporting Remote and Mixed-Presence Tabletop Collaboration
Rainbow Interaction Seminars
Simulating HCI for all
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
Please see above for contact details for this list.