|![[Search]](http://talks.cam.ac.uk/images/search.gif?1209136071)
|![[A-Z Index]](http://talks.cam.ac.uk/images/az.gif?1209136071)
|![[Contact]](http://talks.cam.ac.uk/images/contact.gif?1209136071)
||![[University of Cambridge]](http://talks.cam.ac.uk/images/identifier2.gif?1209136071){kind=small} |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![[Talks.cam]](http://talks.cam.ac.uk/images/talkslogosmall.gif?1209136071) |
Logic and Semantics Seminar (Computer Laboratory)
Add to your list(s)
Send you e-mail reminders
Further detail
Logic and Semantics seminars are usually held at 2pm on Fridays during term time. Please contact the seminar organisers if you would like more information, would like to suggest a speaker, or would like to offer to talk yourself. Useful links:
If you have a question about this list, please contact: Jamie Vicary; nk480; mpf23; Anuj Dawar; Alan.Mycroft; Jon Sterling; pes20; Peter Sewell; Ioannis Markakis; Thibaut Benjamin. If you have a question about a specific talk, click on that talk to find its organiser. 2 upcoming talks and 324 talks in the archive. Number of quantifiers in 3-variable logic on linear orders
Axiomatization of infinity-categories
CRIS: The power of imagination in specification and verification
Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)
A selective and biased choice of techniques for building a distributed data store
Comodule representations of Second-order functionalsNote the unusual date and time.
Choice Principles in Observational Type Theory
Epimorphisms and Acyclic Types in Univalent Mathematics
Synthesis modulo oracles
When Subtyping Constraints Liberate: Polymorphic Subtype Inference And Scope Safety
Towards Secure Distributed Choreographies
Testing GPU Memory Consistency at Large
A categorical semantics for neural networks
Coherence by Normalization for Linear Multicategorical Structures
Software for Compositional Modeling
How to prove - hopefully - that polynomial time is not choiceless
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
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
The Expressive Power of CSP Quantifiers
Title to be confirmed
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
Symmetries in Reversible Programming
Title to be confirmed
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
Categorical Foundations of Gradient-Based Learning
Theorem Provers to Protect Democracy: Formally Verified Vote-Counting-Software
Comparing general definitions of type theories
A computational method for left adjointness
Towards a geometry for syntax
Enriched categories for optimal transport
A formal context for metric semantics
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
Promising ARMv8/RISC-V relaxed memory
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
A Syntactic View of Computational Adequacy
Tests and Proofs in Isabelle
Aspects of my formal development work
Automating proof by induction in Isabelle/HOL using domain-specific languages
Formal Foundations for Provably Safe Web Components
A duality theoretic view on limits of finite structures
Cerberus C semantics & pointer provenance
Computation via Substructures
Quantum things 3 - Resources and Co-resources
Modular Relaxed Dependencies in Weak Memory Concurrency
Quantum Things 2 - The quantum monad on relational structures
Quantum Things 1 - Monads, comonads, and resource-limited computation
Local reasoning for robust observational equivalence
Verification of Cyber-Physical Systems: Temporal Properties and Airplane Collision Avoidance
Retrofitting Purity with Comonads and Capabilities
Hardness magnification near state-of-the-art lower bounds
An Overview of the Flix Programming Language
Resource-oriented programming with graded modal types
Uncertainty is hope: towards a unified foundation of gradual typing
Push versus Pull-Based Loop Fusion in Query Engines
Stacked Borrows: An Aliasing Model for Rust
Excel Formulae: a PL perspective
Linear Capabilities: an overview
Linear capabilities for fully abstract compilation of separation-logic-verified code
StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities
A domain theory for statistical probabilistic programming
Project Everest: towards a verified TLS ecosystem
Verifying Concurrent Search Structure Templates
Lower bound for arithmetic circuits via Hankel matrix
Quasi-polynomial solutions for parity games and other problems
Beyond Polarity: Towards A Multi-Discipline Intermediate Language with Sharing
Graphical Conjunctive Queries
Automated Full-Stack Memory Model Verification with the Check suite
Types and Safety of Lock-free Data Structures
The direct approach to evaluation order
Compositional Compiler Verification for a Multi-Language World
From global to local state in game semantics via the sequoid
Quantitative equational reasoning
Scheduling Tasks for Reconfigurable Architecture
Lecture 3: Logic for Program Development, Verification and Implementation.
One Hierarchy Spawns Another: Graph Deconstructions and the Complexity Classification of Conjunctive Queries
Left Exact Modalities in Type Theory
Modular Algorithm Analysis
Lightweight verification of separate compilation
Lecture 2: Algebraic Theory of Program Transformation
Atomicity Abstractions in Relaxed Memory Architectures
Computer Laboratory Programming Research Group Seminar Energy Efficient Compilation of Irregular Task-Parallel Loops
Logic Programming, Semantics, and a Bit of Cleverness
A Geometric Theory of Program Testing.
Effective Stateless Model Checking for C/C++ Concurrency
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
Reasoning beyond data-race freedom
Designing Verifiable Cache Coherence Protocols
Lightweight verification of separate compilationNB: rescheduled from 2017/09/22
Event Correlation with Algebraic Effects
A promising semantics for relaxed-memory concurrency
Semantics of Full Ground References
Applications of Finite Model Theory in Graph Isomorphism Testing and Propositional Proof Complexity
Interleaved scope for games and automata
Disjoint Semirings for Fractional Permissions**NOTE NON-STANDARD DAY AND ROOM BOOKING**
Concurrent Kleene Algebras and Pomset Languages
What does the Future of Programming Look Like?
Higher Categorical Structures, Type-Theoretically
Diagrammatic Operational Semantics for Digital Circuits
Verified Characteristic Formulae for CakeML
A monad for full ground reference cells
Genus, Numerics and Architectural Level OptimisationJoint Logic and Semantics and Computer Architecture Seminar
One-Dimensional Higher Inductive Types
Polymorphism, subtyping and type inference in MLsub
A categorical perspective on type refinement systems
Cantor meets Scott: Domain-Theoretic Foundations for Probabilistic Network Programming
A compositional account of Herbrand's theorem via concurrent gamesNOTE NON-STANDARD ROOM BOOKING
Fencing off Go: Liveness and Safety for Channel-based Programming
Context Equivalences and Metrics in Probabilistic Lambda-Calculi
An Algebraic Combinatorial Approach to the Abstract Syntax of Opetopic Structures
On Proofs of Equality as Paths
Analysing Goedel’s T by means of ordinal assignment and collapsingNOTE NON-STANDARD ROOM BOOKING
Making Reactive Programs Function
A new verified compiler backend for CakeML**NOTE NON-STANDARD DATE, TIME, AND ROOM**
Classical Linear Logic considered as a programming language
A Verified CompCert Front-End for a Memory Model supporting Pointer Arithmetic and Uninitialised Data
Practical Statically-checked Deterministic Parallelism
Automatically comparing memory consistency models
Programming and Proving with Concurrent Resources
Optimising star-convex functions
Automated Reasoning and AI for Large Formal Mathematics
Certified automated theorem proving for types
The C standard formalized in Coq, what's next?
A rational reconstruction of homogeneous meta-programming
Logical dependence via functional dependence
Generating Gradual Typing Systems with the Gradualizer
Comprehensive Parametric Polymorphism
THIS TALK HAS BEEN CANCELLED/POSTPONEDTHIS TALK HAS BEEN CANCELLED/POSTPONED
A call-by-value realizability model for PMLNOTE UNUSUAL VENUE
Excuse My Extrusion
Identity types in Algebraic Model StructuresNOTE UNUSUAL VENUE This is the second seminar this week.
What is an Algorithm?NOTE UNUSUAL TIME, DAY, AND VENUE. There are two seminars this week (Tuesday and Friday)
Effects as sessions, sessions as effectsNOTE UNUSUAL VENUE
Interacting Hopf monoids: the algebra of signal flow diagramsNOTE UNUSUAL VENUE
Dependent Types and Fibred Computational Effects
Graphical linear algebra and applications
A continuation passing translation for functional session types
Typed realizability for first-order classical analysis
Online Space Complexity
Global Realisations of Local Specifications
Heat kernels in graphs: A journey from random walks to geometry, and back
Consistency of Quine's NF using nominal techniques
From Communicating Machines to Graphical Choreographies
Generic Computational Models
Locally Finite Constraint Satisfaction Problems
Linear numeral systems
Game Semantics for Interface Middleweight Java
New reasoning techniques for monoidal algebras
Rigid Graphs for Adaptive Networks, with Data
Transition systems over games
Senescent Ground Tree Rewrite Systems
Verification of quantum protocols using Coq
An Algorithmic Metatheorem for Directed Treewidth
Micro-Policies: A Framework for Tag-Based Security Monitors
Backward Analysis via Over-Approximate Abstraction and Under-Approximate Subtraction
Why Isn’t Verification Standard Practice?
Modeling a Practical Combination of Delimited Continuations, Exceptions, Dynamic-Wind Guards, Dynamic Binding, and Stack Inspection
On-the-fly garbage collection: issues and opportunities
Representing conditional independence in probabilistic programming
Automating reasoning tasks for separation logic
An algebraic theory of type-and-effect systems
Relational Programming in miniKanren
Decision Problems for Linear Recurrence Sequences
Language based web security: the operational semantics approach
Weighted relational models of typed lambda-calculi
Simple, efficient, sound-and-complete combinator parsing for all context-free grammars, using an oracle.
**TALK POSTPONED**
Fibrational Parametricity
Descriptive set theory and Computation theory
An overview of nominal algebra, lattice, representation and dualities for computer science foundations
**Cancelled** Logic of Hybrid Games
A few lessons that I learnt about interprocedural program analyses
Multiparty session types and their application in large distributed systems
Barrier Invariants : a Shared State Abstraction for Data-dependent GPU Kernels >
Semigroups with low difficulty word problem
Malware Analysis with Tree Automata Inference
Cyclic Abduction of Inductive Termination Preconditions
Halo: From Haskell to Logic through Denotational Semantics
Abstraction and Invariance for Algebraically Indexed Types
Preservation under Substructures modulo Bounded CoresNote special date and location (GC22)
Bounds on proof size and distributive encryptionNote that this talk will be in FW26 rather than the usual room.
Safe Recursive Set Functions
MELL in a free compact closure
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
Expressiveness of real-time temporal logics
On modal definability of first-order formulas with many free variables and its application to conjunctive query answering in description logics
Iterative algorithms and Sherali-Adams linear programming relaxations of graph isomorphism
Layered Fixed Point Logic
Algebra unifies Calculi of programming
Nash Equilibrium, Bekic's Lemma and Bar Recursion
Almost always blue trees and bar induction
Parameterized Complexity of some Problems in Concurrency and Verification
Parallel Assertions for Debugging Parallel Programs
Lightweight Monadic Programming in ML
The Complexity of #CSP
Isomorphisms of types in the presence of higher-order references
Domination When the Stars Are Out – An algorithmization of Chudnovsky’s and Seymour’s Structure Theorem for Claw-Free Graphs
Bisimulation and Model-Checking for Partial Order Models of Concurrency
Approximating Labelled Markov Processes by Averaging
Kleisli Arrows of Outrageous Fortune
Selection functions everywhere
Modular Reasoning for Deterministic Parallelism
Automatic reduction of differential semantics for protein-protein interaction networks, by abstract interpretation
Towards Automatic Resource Consumption CertificationNote unusual time (11am) and room (SS03)
A Framework for Incremental Modelling and Verification of On-Chip Protocols and Its Application to PCI ExpressNote the unusual time (13:00)
Characterizations of the Expressive Power of Logics over Trees
Mini Courses in Theoretical Computer Science Mini course on proof theory (Part 3)
Mini Courses in Theoretical Computer Science Mini course on proof theory (Part 2)
Mini Courses in Theoretical Computer Science Mini course on proof theory (Part 1)
Scalars & probabilities, monads & categories
The Scott model of Linear Logic is the extensional collapse of its relational model
Algebraic Theories over Nominal Sets
Wednesday Seminars - Department of Computer Science and Technology From Separation Logic to Systems Code
Declassification Policy Inference
Undecidability of propositional separation logic and its neighbours
Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
The Hybrid Systems Jigsaw: Bringing Together Computer Science, Dynamical Systems and Control Engineering.
The Microcosm Principle and Coalgebraic Modeling of Component Calculi
Wednesday Seminars - Department of Computer Science and Technology Serializability Enforcement for Concurrent ML
A Theory of Indirection via Approximation
NO LOGIC AND SEMANTICS SEMINAR TODAYFW11 FW26 not available today
A Canonical Local Representation of Binding
Explicit Stabilisation for Rely-Guarantee reasoning
Inductive-recursive definitions
Safety of program transformations in shared-memory concurrencyNOTE UNUSUAL DAY AND TIME. There are two seminars this week, one on Wednesday, one on Friday.
Focalisation and Classical Realisability
TALK CANCELLED: An overview of structural corecursionTHIS TALK HAS BEEN POSTPONED. We hope to reschedule for later in the term.
Structurally Recursive Descent Parsing
Deciding Boolean BI (via Display Logic)
A game for a neutral approach to provability in MALL
Equideductive logic and CCCs with subspacesNOTE UNUSUAL DAY.
Mini Courses in Theoretical Computer Science Call-by-push-value (part 2)This is the second part of a two-part series
Mini Courses in Theoretical Computer Science Call-by-push-value (part 1)This is the first part of a two-part series. Part 2 is on Wed 4th Feb.
Nondeterminism: many questions and (maybe) some answers
Dynamics, robustness and fragility of trustNOTE THE UNUSUAL TIME
Polynomial functors
Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types
Wednesday Seminars - Department of Computer Science and Technology Practical Dynamic Software Updating for C
Classical BI (A Logic for Reasoning About Dualising Resource)
Nominal terms and one-and-a-half level Curry-Howard
The interpretation of intuitionistic type theory in locally cartesian closed categories: an intuitionistic approach
Event structure semantics of the pi-calculus
Extensional rewriting with sums
Eriskay: a programming language based on game semantics.
Verification Based on Algebra and Automated Deduction
A language extension for provably safe exception handling
Keep Off The Grass: Locking the Right Path for Atomicity
On Scalable Shape Analysis
A completeness proof for bisimulation in the pi-calculus using IsabelleNote the unusual day.
Logics for Coalgebras
Category Theory and the Philosophy of Language
Separation Logic Semantics for Communicating Processes
Pointer Safety and Graph Grammars
Model theoretic tools for deciding boundedness of fixed points
Logical Reasoning for Higher-Order Functions with Local State
The Java Memory Model - the Good, the Bad and the Ugly
A unified model of class invariant verification frameworks
Cyclic Proofs of Program Termination in Separation Logic
Valiant's theory
An Executable Model of the JVM in Coq
Infinite-State System Verification via Tree Automata
When While is a Security Risk
Relational parametricity for computational effects.
Stone duality for bitopological spaces
Verification Across Intellectual Property Boundaries
A Logic of Reachable Patterns in Linked Data-Structures
Verifying Object-Invariants in Spec#
Fine-grained concurrency with separation logic(joint work with Kalpesh Kapoor and Kamal Lodaya)
A logical approach to data provenance.
Bialgebras and modal logic
Reasoning about Code Pointers (Separation Logic for Higher-Order Store)
A structural proof of the soundness of rely/guarantee rules
Logical equivalence for subtyping object and recursive types.
Collection and Contra-collection in Mathematics
Please see above for contact details for this list. |
Other listsTrust and Cloud Computing Cambridge University Heraldic and Genealogical SocietyOther talksThe Anne McLaren Lecture: CRISPR-Cas Gene Editing: Biology, Technology and Ethics Reading and Panel Discussion with Emilia Smechowski CANCELLED DUE TO STRIKE ACTION Concentrated, “pulsed” axial glacier flow: structural glaciological evidence from Kvíárjökull in SE Iceland Investigation into appropriate statistical models for the analysis and visualisation of data captured in clinical trials using wearable sensors Thermodynamics de-mystified? /Thermodynamics without Ansätze? Towards bulk extension of near-horizon geometries The frequency of ‘America’ in America 'Honouring Giulio Regeni: a plea for research in risky environments' An SU(3) variant of instanton homology for webs Kiwi Scientific Acceleration on FPGA |
Lauri Hella (Univeristy of Tampere).
Friday 21 March 2025, 14:00-15:00