Peter Sewell

Name:	Peter Sewell
Affiliation:	University of Cambridge
E-mail:	(only provided to users who are logged into talks.cam)
Last login:	15 Jun 2024, 11:33 a.m.

Public lists managed by Peter Sewell

• Logic and Semantics Seminar (Computer Laboratory)
• Semantics Lunch (Computer Laboratory)

Talks given by Peter Sewell

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 Peter Sewell

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

• Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)
• Lightweight verification of separate compilation
• Algebraic Principles for Program Verification and Refinement Tools
• Kneecap: model-based generation and analysis of network traffic
• The CH2O project: making sense of the C standard
• Yet more animals: dynamic linkers and debuggers
• ABIs, linkers and other animals
• POPL PC workshop
• Sigma*: Symbolic Learning of Input-Output Specifications
• High-Level Separation Logic for Low-Level Code
• Library Abstraction for C/C++ Concurrency
• Full Abstraction for PCF with Names
• A Model-Learner Pattern for Bayesian Reasoning
• Putting the thrill back into computing at school
• On distributed probabilistic strategies
• The Power of Parameterization in Coinductive Proof
• Containers, Comonads and Distributive Laws
• Ribbon Proofs for Separation Logic
• CerCo --- Certified Complexity
• A Concurrent Logical Relation
• Virtue of certified programming with decision procedures
• From threads to events through classical program transformations
• Developing verified programs in Dafny
• RESCHEDULED to 20th Feb: GPUVerify: a modular verifier for GPU kernels
• Resource Sensitive Synchronisation Inference by Abduction
• Clarifying and Compiling C/C++ Concurrency: from C++11 to POWER
• Stop when you are Almost-Full: Adventures in Constructive Termination
• Understanding POWER Multiprocessors
• The Importance of Being Linearizable
• A Heirarchy of Mendler style Iteration/Recursion Combinators: taming recursive types with negative occurrences
• Semantics of a DNA Strand Displacement Model
• Ribbon proofs for separation logic
• TOPL: A Language for Specifying Safety Temporal Properties of Object-Oriented Programs
• Relating Two Semantics of Locally Scoped Names
• Polarisation in classical realisability and delimited control
• Composable Asynchronous Events/Formal Methods for Wireless Mesh Networks
• Relaxed-Memory Concurrency and Verified Compilation / Mathematizing C++0x concurrency
• Making Prophecies with Decision Predicates
• Finding best paths in difficult conditions