Theory Group

Past activities

(2011, January - December)

2 Dec
(15:00)
QMUL
BR4.01
Joint Queen Mary/Imperial Seminar
Florian Zuleger (TU Vienna)
Bound Analysis of Imperative Programs with the Size-change Abstraction
28 Sept
(15:00)
QMUL
BR4.02
Joint Queen Mary/Imperial Seminar
Joel Ouaknine (Oxford University)
A Survey of Classical and Real-Time Verification
7 Sept
(15:00)
QMUL
BR4.02
Joint Queen Mary/Imperial Seminar
Thomas Powell (QMUL)
System T and the Product of Selection Functions
27 June
(15:00)
QMUL Joint Queen Mary/Imperial Seminar
Mikoláš Janota (INESC-ID, Lisboa)
Abstraction-Based Algorithm for 2QBF
23 June
(14:00)
QMUL
BR4.02
Joint Queen Mary/Imperial Seminar
Tony Hoare
In Praise of Algebra
15 June
(15:00)
QMUL
BR4.02
Joint Queen Mary/Imperial Seminar
Mark Josephs (University of Warwick)
Processes through the Looking Glass: Reflections on an Algebra for Delay-Insensitive Circuits
6 June
(15:00)
QMUL
BR3.01
Joint Queen Mary/Imperial Seminar
Kenneth McMillan (Microsoft Research)
Coming to Grips with Complexity in Computer-Aided Verification
18 May
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Cristian Cadar (Imperial College)
Dynamic Symbolic Execution for Software Testing and Bug Finding
13 May
(14:00)
QMUL
BR4.01
Joint Queen Mary/Imperial Seminar
Christoph Haase (University of Oxford)
Deciding Entailment in SL with Possibly-empty Lists is Polytime
27 Apr
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Jade Alglave (University of Oxford)
Fences in Weak Memory Models
21 Apr
(14:30)
QMUL
BR 3.2
(AKA CS 338)
Joint Queen Mary/Imperial Seminar
Aquinas Hobor (National University of Singapore)
A Theory of Termination via Indirection
18 Apr
(11:00)
QMUL
BR 4.1
(AKA CS 445)
Joint Queen Mary/Imperial Seminar
Aditya Nori (MSR India)
Guessing Program Annotations with Probabilistic Inference
16 Mar
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Michael Benedikt (University of Oxford)
Revealing the Logic of the Hidden Web
9 Feb
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Ankur Taly (Stanford University)
Language-based Isolation of Untrusted JavaScript
26 Jan
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Ricardo Dias (Universidade Nova de Lisboa, Portugal)
Using Separation Logic to Detect Snapshot Isolation Anomalies in Software Transactional Memory

(2010, January - December)

1 Dec
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Daniel Koernlein (London School of Economics)
An Application of Proof Mining to Functional Analysis
17 Nov
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Ranjit Jhala (University of California, San Diego)
Software Verification via Liquid Types
27 Oct
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Prakash Panangaden (McGill University, Canada)
Epistemic Strategies and Games on Concurrent Processes
13 Oct
(15:00)
QMUL
CS4.02
(AKA BR4.02)
Joint Queen Mary/Imperial Seminar
Samson Abramsky (Oxford University)
Relational Hidden Variables and Non-Locality
8 Sep
(14:00)
QMUL
CS3.02
(AKA BR3.02)
Joint Queen Mary/Imperial Seminar
Kohei Suenaga (Universidade de Lisboa, Portugal)
Fractional Ownerships for Safe Memory Deallocation
12 Aug
(15:00)
QMUL
Francis Bancroft
3.15
Joint Queen Mary/Imperial Seminar
Gerwin Klein (National ICT Australia)
A Formally Verified OS Kernel. Now What?
7 Jul
(14:00)
QMUL
ITL
top floor
Joint Queen Mary/Imperial Seminar
Tom Chothia (University of Birmingham)
Calculating Information Leakage in Continuous Domains
14 Jun
(14:00)
QMUL
CS
3.01
Joint Queen Mary/Imperial Seminar
Andrew D. Gordon (Microsoft Research Cambridge)
Semantic Subtyping with an SMT Solver
2 Jun
(15:00)
QMUL
CS
4.01
Joint Queen Mary/Imperial Seminar
Kirill Bogdanov (The University of Sheffield)
Reverse Engineering and Testing
13 May
(11:00)
QMUL
CS
3.02
Joint Queen Mary/Imperial Seminar
Mircea-Dan Hernest (Ecole Polytechnique, France)
Modal Functional Interpretation
5 May
(15:00)
QMUL
CS
3.02
Joint Queen Mary/Imperial Seminar
Alastair Donaldson (Oxford University)
Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
22 Apr
(14:00)
QMUL
ITL
top floor
Joint Queen Mary/Imperial Seminar
Nir Piterman (Imperial College)
p-Automata: New Foundations for Discrete-Time Probabilistic Verification
31 Mar
(15:00)
QMUL
CS
3.02
Joint Queen Mary/Imperial Seminar
Andy King (Portcullis Computer Security Limited)
Automatic Abstraction for Congruences -- A Story of Beauty and the Beast
15 Mar
(14:00)
QMUL
ITL
top floor
Joint Queen Mary/Imperial Seminar
Sofiene Tahar (Concordia University)
Formal Probabilistic and Statistical Analysis using Higher-Order Logic
3 Mar
(15:00)
QMUL
CS
3.02
Joint Queen Mary/Imperial Seminar
Alison Pease (University of Edinburgh)
The Role of Axiomatisation in Mathematical Discovery

(2009, January - December)

20 Nov
(14:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Derek Dreyer (Max Planck Institute for Software Systems, Germany)
A Modal Logic for Equational Reasoning in ML-Like Languages
18 Nov
(15:00)
QMUL
CS
3.02
Joint Queen Mary/Imperial Seminar
Jens Krinke (King's College London)
Information Flow Control with Program Dependence Graphs
12 Oct
(16:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Bart Jacobs (Katholieke Universiteit Leuven)
Verifying fine-grained concurrent algorithms with VeriFast
15 Sep
(13:30)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Jorge Perez (University of Bologna)
On the Expressiveness of Forwarding in Higher-Order Communication
13 Aug
(14:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Paulo Oliva (Queen Mary Univesity of London)
On Selection Functions and Generalised Quantifiers
12 Aug
(14:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Jaime Gaspar (Technische Universitat Darmstadt)
A logical view at Tao's finitization of principles in analysis
22 Jul
(13:30)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Vasco Vasconcelos (University of Lisbon)
Session type systems as linear type systems
25 Jun
(15:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Dimitris Mostrous (Imperial College)
Session Types for Higher-order Mobile Processes: Asynchronous Communication Subtyping and Linear Typing
17 Jun
(15:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Ben Moszkowski (De Montfort University)
A Unifying Analytical Framework for Discrete, Linear Time
3 Jun
(15:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Jeremy Singer (University of Manchester)
Intelligent Thread-level Speculation
13 May
(15:30)
QMUL
CS
446
Joint Queen Mary/Imperial Seminar
John Shawe-Taylor (University College London)
PAC Bayes Analysis: Background and Applications
20 Apr
(14:00)
QMUL
CS
445
Joint Queen Mary/Imperial Seminar
Stephen Magill (Carnegie Mellon University)
Automatic Numeric Abstractions for Heap-Manipulating Programs
1 Apr
(15:30)
QMUL
CS
446
Joint Queen Mary/Imperial Seminar
David Parker (Oxford University)
Verification of Probabilistic Software
31 Mar
(14:00)
QMUL
CS
445
Joint Queen Mary/Imperial Seminar
John C. Reynolds (Carnegie Mellon University)
Readable Proofs in Hoare Logic (and Separation Logic)
4 Mar
(15:30)
QMUL
CS
446
Joint Queen Mary/Imperial Seminar
Zoubin Ghahramani (University of Cambridge)
Recent directions in nonparametric Bayesian machine learning
13 Feb
(11:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Tamara Rezk (INRIA Sophia Antipolis-Mediterranee)
A Compiler for Security
21 Jan
(15:30)
QMUL
CS
446
Joint Queen Mary/Imperial Seminar
Mike Laurence (Goldsmiths, University of London)
Introduction to Program Schemas with applications to Program Slicing
15 Jan
(14:00)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Jeffrey Sarnat (Yale University)
A new consistency proof for intuitionistic inductive definitions
using the lexicographic path ordering

(2008, June - December)

15 Dec
(15:30h)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
Aslan Askarov (University of Gothenburg)
Tight Enforcement of Flexible Information-Release Policies for Dynamic Languages
4 Dec
(16:00h)
QMUL
ITL
top floor
Joint Queen Mary/Imperial Seminar
Eric Koskinen (University of Cambridge)
Techniques for Symbolic Complexity Bounds
3 Dec
(15:30h)
QMUL
CS/446

Joint Queen Mary/Imperial Seminar
Alexander Kurz (University of Leicester)
Pi-Calculus in Logical Form
19 Nov
(15:30h)
QMUL
CS/446

Joint Queen Mary/Imperial Seminar
Pierre-Malo Denielou (INRIA Rocquencourt)
Protocol Synthesis and Verification for Secure Sessions
27 Oct
(11:00h)
QMUL
Biology
3.15
Joint Queen Mary/Imperial Seminar
John C. Reynolds (Carnegie Mellon University)
Readable Formal Proofs
17 Sep
(14:00h)
QMUL
Francis Bancroft
FB1.02.6
Joint Queen Mary/Imperial Seminar
Lawrence C. Paulson (University of Cambridge)
MetiTarski: A Resolution-Based Prover for the Special Functions
6 Aug
(15:30h)
QMUL
Francis Bancroft
FB327
Joint Queen Mary/Imperial Seminar
Liqian Chen (Ecole Normale Superieure/National Laboratory for Parallel and Distributed Processing, Changsha, China)
A Sound Floating-Point Polyhedra Abstract Domain
5 Aug
(15:30h)
QMUL
Francis Bancroft
FB327
Joint Queen Mary/Imperial Seminar
Julien Bertrane (Ecole Normale Superieure)
Reduced Product of Abstract Domains for the Static Analysis of Properties of Imperfectly-clocked Synchronous Systems
30 Jul
(15:30h)
QMUL
Francis Bancroft
FB327
Joint Queen Mary/Imperial Seminar
Dana N. Xu (University of Cambridge)
Static Contract Checking for Haskell
02 Jul
(15:30h)
QMUL
ITL
top floor
Joint Queen Mary/Imperial Seminar
Elena Troubitsyna (Abo Akademi University)
Talk on Formal development of fault tolerant systems by refinement
18 Jun
(15:30h)
QMUL
CS/338
Joint Queen Mary/Imperial Seminar
Sam Staton (University of Cambridge)
General structural operational semantics through categorical logic

(2008, January - May)

28 May
(10:30h)
QMUL
CS/338
Joint Queen Mary/Imperial Seminar
Martin Escardo (University of Birmingham)
Infinite sets that admit exhaustive search in finite time
27-29 May
(14:00h)
Imperial
TBA
Joint Queen Mary/Imperial Seminar
Byron Cook (Microsoft Research Cambridge)
Proving termination and liveness of programs
21 May
(15:30h)
QMUL
CS/338
Joint Queen Mary/Imperial Seminar
Stefano Berardi (Torino University)
Classical proofs as processes
15 May
(14:00h)
Imperial
145
Joint Queen Mary/Imperial Seminar
Alessio Guglielmi (University of Bath)
Deep inference, proof identity and proof complexity
02 Apr
(15:30h)
QMUL
CS/446
Lab Tea
Federico Aschieri
Strong normalization for intersection types sytem
19 Mar
(15:00h)
QMUL
CS/446
Distinguished Seminar
Prof. Robert Gaizauskas (University of Sheffield)
From questions to queries: Issues in the interpretation of questions
12 Mar
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Antonino Salibra (Universita Ca Foscari di Venezia)
From Universal Algebra to Lambda Calculus and Back
27 Feb
(15:30h)
QMUL
CS/446
Lab Tea
Matthew Huntbach
A computation model using single-assignment single-writer variables with back-communication
13 Feb
(15:30h)
QMUL
CS/446
Lab Tea
Pasquale Malacaria & Han Chen
Lagrangian multipliers and their use in computing maximum leakage in various computational systems
06 Feb
(15:00h)
QMUL
CS/446
Distinguished Seminar
Prof. Kerstin Dautenhahn (University of Hertfordshire)
Can we benefit from robotic helpers?
30 Jan
(15:00h)
QMUL
CS/446
Distinguished Seminar
Prof. Andrew Zisserman (University of Oxford)
Google like search of image databases and videos
23 Jan
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Matthew Parkinson (Cambridge University)
Verifing OO Programs the good, the bad, and the ugly
16 Jan
(15:00h)
QMUL
CS/446
Distinguished Seminar
Prof. Wendy Hall (University of Southampton)
Towards a Science of the Web

(2007, June - December)

19th Dec
(15:00h)
Imperial
Huxley Blg.
Room 207
Joint Queen Mary/Imperial Seminar
Simon Kramer (LIX-Ecole Polytechnique)
Towards Interactive Belief, Knowledge, and Provability: Possible Application to Zero-Knowledge Proofs
12th Dec
(15:30h)
QMUL
CS/446
Lab Tea
Marco Carbone
Structured Communication-Centred Programming for Web Services
28th Nov
(15:00h)
QMUL
CS/446
Distinguished Seminar
John Tucker (Swansea University)
Computability and experimental procedures applied to physical systems
21st Nov
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Julian Bradfield (Edinburgh University)
How user-friendly is independence-friendly logic?
14th Nov
(15:00h)
Maths
Lec. Th.
Distinguished Seminar
Nigel Shadbolt (University of Southampton)
From Science on the Web to a Web of Science
7th Nov
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Francesco Tiezzi (University of Florence)
COWS: a Calculus for Orchestration of Web Services
31st Oct
(15:00h)
QMUL
CS/446
Distinguished Seminar
David Hogg (University of Leeds)
Reasoning about visual scenes
24th Oct
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Samuel Mimram (Université Paris Diderot / Paris 7)
Asynchronous games: Innocence without alternation
17th Oct
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Paul Levy (University of Birmingham)
Nondeterminism: many questions and (maybe) some answers
3rd Oct
(15:30h)
QMUL
CS/446
Lab Tea
Jonathan Heusser
Measuring Insecurity of Programs
19th Sept
(16:00h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Neel Krishnaswami (Carnegie Mellon University)
Verifying the Subject Observer Pattern with Higher Order Separation Logic
12th Sept
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Steven Le Comber (QMUL, Biology Department)
Bees and the travelling salesman problem: how tiny brains solve complex cognitive tasks
27th June
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Nathaniel Charlton (Imperial College)
TBA

(2007, January - May)

16th May
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Mark Ryan (University of Birmingham)
Multi-party contract signing: a roller-coaster ride
11th Apr
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Guy McCusker (University of Bath)
A games model of bunched implications
7th Mar
(15:00h)
QMUL
CS/446
Distinguished Seminar
Yvonne Rogers (Open University)
Beyond the desktop and the vision of calm computing:
A critique of the emerging field of UbiComp
14th Mar
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Jose Montoya (School of Biological and Chemical Sciences, QMUL)
Ecological Networks: The Complexity and Fragility of Ecosystems
21st Mar
(15:00h)
QMUL
CS/446
Distinguished Seminar
Nigel Smart (University of Bristol)
Cryptography: The art of knowing nothing
6th Feb
(16:00h)
QMUL
ITL top
floor
Joint Queen Mary/Imperial Seminar
Tom Kelsey (University of St Andrews)
Large-scale enumeration strategies using GAP and Minion
12th Feb
(15:00h)
Imperial
Studio A
Joint Queen Mary/Imperial Seminar
Daniele Gorla (Univ. di Roma "La Sapienza")
On the Relative Expressive Power of Calculi for Mobility
14th Feb
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Mehrnoosh Sadrzadeh (University of Southampton)
Semantics for Information Update
21st Feb
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Ana Cavalcanti (University of York)
Test-data Generation by Proof
17th Jan
(15:00h)
QMUL
CS/446
Distinguished Seminar
Dr Ewan Birney (European Bioinformatics Institute - EBI)
Part of the Women in Innovation and Invention Workshop
31st Jan
(15:00h)
QMUL
CS/446
Distinguished Seminar
Prof Jon Crowcroft (University of Cambridge)
Network Architecture Research Considerations or The Internet Conspiracy

(2006, December)

12th Dec
(15:00h)
Imperial
Huxley
308
Joint Queen Mary/Imperial Seminar
Claudio Guidi (IMT Lucca)
Formalizing languages for Service Oriented Computing

(2006, November)

1st Nov
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Christian Urban (TU Munich, Germany)
Inductions in the Nominal Datatype Package or
How Not to be Intimidated by the Variable Convention
8th Nov
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Thomas Forster (Cambridge University)
Is Propositional Calculus expressible in a Kleene-Regular Language?
15th Nov
(15:00h)
QMUL
CS/446
Distinguished Seminar
Igor Aleksander (Imperial College)
Conscious Machines: Fiction or Fact
21th Nov
(14:00h)
Imperial
Huxley
344A
Joint Queen Mary/Imperial Seminar
Mohammad Reza Mousavi (Eindhoven University of Technology)
Reconciling Operational and Epistemic Approaches to Protocol Verification
22th Nov
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Marcelo Fiore (Cambridge University)
Differentiation in Models of Intuitionistic Linear Logic with Commutative Bialgebra Structure
23th Nov
(13:00h)
Imperial
Huxley
Studio B
Joint Queen Mary/Imperial Seminar
Roberto Guanciale and Daniele Strollo (IMT Lucca)
A type-based coordination calculus of signals
29th Nov
(15:00h)
QMUL
Octagon
Distinguished Seminar
Gillian Arnold (IBM)
Part of the Women in Innovation and Invention Workshop

(2006, October)

4th Oct
(15:00h)
QMUL
CS/446
Distinguished Seminar
Byron Cook (Microsoft Research, Cambridge)
Automatic Formal Verification for Operating Systems Code
11th Oct
(15:30h)
QMUL
CS/446
Joint Queen Mary/Imperial Seminar
Mark Jerrum (Queen Mary, University of London)
Approximating the Tutte polynomial: a status report
18th Oct
(15:00h)
QMUL
CS/446
Distinguished Seminar
Barry Smith (Birkbeck College)
Speech Sounds and the Direct Meeting of Minds
25th Oct
(10:00h)
King's
College
London Theory Day
Programme can be found here

(2006, September)

13th Sept
(15:30h)
Imperial
Huxley Bldg.
Studio A
Joint Queen Mary/Imperial Seminar
Silvia Crafa (Università di Padova)
P-Congruences as Non-Interference for the pi-calculus
18th Sept
(10:30h)
BCS
London
Theory Group Away Day
Programme

(2006, July)

19th July
(16:00h)
QMUL
ITL top
floor
Joint Queen Mary/Imperial Seminar
Dan Guica (University of Birmingham)
Geometry of Synthesis: A structural approach to VLSI design

(2006, June)

7th June
(15:30h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Sebastian Nanz (Imperial College)
Specification and Security Analysis of Mobile Ad-Hoc Networks

(2006, May)

3rd May
(15:30h)
QMUL
Math Lec
Theatre
Distinguished Seminars
Prof. Moshe Vardi (Rice University)
And Logic Begat Computer Science: When Giants Roamed the Earth
22nd May
(15:00h)
QMUL
CS338
Distinguished Seminars
Dr. Matt Jones (Future Interaction Thecnology Lab)
Navigation by Music

(2006, April)

5th Apr
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Randy Pollak (Edinburgh University)
Reasoning about languages with bindings: can we do it yet?
11th Apr
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Graham White
24th Apr
(all day)
Imperial
Studio A
London Theory Day
Organiser: Philippa Gardner (Imperial College)
Invited speaker: Andrew Appel (Princeton University)

(2006, March)

1st Mar
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Prof. Lawrence Paulson (Cambridge University)
Integrating Interactive and Automatic Theorem Provers: Status and Prospects
14th Mar
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Ursula Martin
22nd Mar
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof. Chris Reed (Faculty of Law & Social Science, QMUL)
The Not So Free For All - websites, online resources and the role of law
23rd Mar
(15:00h)
Imperial
Huxley Bld
Studio A
Joint Queen Mary/Imperial Seminar
Dino Distefano (Queen Mary College)
A Local Heap Analysis based on Separation Logic
28th Mar
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Paul Curzon

(2006, February)

1st Feb
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Rob Arthan (Lemma 1 Ltd.)
34/100 (and counting)
8th Feb
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof. Herbert H. Clark (Stanford University)
Rational ways of talking
22nd Feb
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof. Keith van Rijsbergen (University of Glasgow)
Information Retrieval, its geometry and logic
28th Feb
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Pasquale Malacaria

(2006, January)

11th Jan
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof. Philip Dawid (UCL)
Object-Oriented Bayesian Networks for Forensic Identification
17th Jan
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Paulo Oliva
31st Jan
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Max Kanovitch

(2005, December)

1st Dec
(15:00h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Alberto Momigliano (University of Edinburgh)
A program logic for resources and its application to optimisation validation
7th Dec
(16:00h)
QMUL
CS445
Joint Queen Mary/Imperial Seminar
Murdoch Gabbay (King's College London)
Fraenkel-Mostowski Techniques: a NEW model of freshness and  abstraction
13th Dec
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Matthew Huntbach
14th Dec
(15:00h)
Imperial
Studio A
Joint Queen Mary/Imperial Seminar
Emilio Tuosto (University of Leicester)
Modelling and using Application-Level QoS

(2005, November)

2nd Nov
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof Back Ralph-Johan (Abo Akademi University, Finland)
Invariant Based Programming
9th Nov
(15:50h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Emmanuel Beffara (CNRS, Paris)
Concurrent models for linear logic
15th Nov
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Peter O'Hearn
16th Nov
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof Alexandra Poulovassilis (Birkbeck College, University of London)
Data Integration by Bi-Directional Schema Transformation Rules
30th Nov
(15:30h)
QMUL
CS338
Distinguished Seminars
Prof Andrew Blake, FRS, FRng (Microsoft Research, Cambridge)
Video Segmentation by Fusion of Colour, Contrast and Stereo

(2005, October)

5th Oct
(15:30h)
Maths Lect
Theatre
Distinguished Seminars
Prof Kevin Warwick (Dept of Cybernetics, University of Reading)
Hybrid Intelligence: Combining Human and Machine Brains
12th Oct
(15:30h)
QMUL
CS445
Joint Queen Mary/Imperial Seminar
Agi Kurucz (King's College)
Undecidability of two-variable intuitionistic and modal predicate logics
18th Oct
(13:00h)
QMUL
Tea Room
Lab Lunches
Speaker: Martin Berger
19th Oct
(15:30h)
QMUL
CS446
Distinguished Seminars
Prof Peter Johnson (University of Bath)
From interactive to collaborative systems - the breakdowns, challenges and hopes
25th Oct
(15:00h)
Imperial
studio A
Joint Queen Mary/Imperial Seminar
Sarah Thompson (CPRG, Computer Laboratory, University of Cambridge)
An Abstract Interpretation-based Semantics for Radiation-Hard Asynchronous Circuits
26th Oct
(15:30h)
QMUL
CS445
Joint Queen Mary/Imperial Seminar
Peter Mosses (University of Wales, Swansea)
Modular Structural Operational Semantics

(2005, September)

19th, 20th
September
Newnham
College

QM Theory Group Away Day

21st Sept
(15:30h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Alex Ahern (Imperial College)
Java RMI with Explicit Code Mobility
30th Sept
(16:00h)
Imperial
Huxley 308
Joint Queen Mary/Imperial Seminar
Alley Stoughton (Kansas State University)
Experimenting with Formal Languages using Forlan

(2005, August)

26th Aug Oxford NETCA workshop
Verification and Theorem Proving for Continuous Systems
30th Aug
(14:00h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Cesar Munoz (National Institute of Aerospace)
Real Number Calculations and Interval Analysis in PVS

(2005, July)

6th Jul
(15:30h)
Imperial
TBA
Joint Queen Mary/Imperial Seminar
Luca Viganò (ETH, Zürich)
Automated tools for the security verification of internet protocols

(2005, June)

15th Jun
(15:30h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Gareth Stoyle (Cambridge University)
Dynamic Software Updates

(2005, May)

3rd May
(14:00h)
QMUL
CS446

Control, Dynamics and Logic Seminar
Wolfram Just (School of Mathematical Science, QMUL)
Time-delayed feedback control of chaos: a global perspective
4th May
(15:30h)
Imperial
Huxley 311
Joint Queen Mary/Imperial Seminar
Adrian Francalanza (University of Sussex)
Failure and Fault Tolerance in a Distributed Pi-Calculus
10th May
(14:00h)
QMUL
CS446
Control, Dynamics and Logic Seminar
Alexei Pavlov (Eindhoven University of Technology)
Convergent systems: linear thinking for nonlinear systems
11th May
(11:00h)
QMUL
CS338
Departmental Seminar
Andrew Moore
Towards Accurate Network-Traffic Characterization
11th May
(14:00h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Joshua Guttman
Skeletons and Their Shapes
16th May
(15:30h)
Imperial
Huxley 311
Joint Queen Mary/Imperial Seminar
Peter Selinger (University of Ottawa)
Towards a Quantum Programming Languages
17th May
(14:00h)
QMUL
CS446
Control, Dynamics and Logic Seminar
Henri Huijberts (Engineering Department, QMUL)
Linear controllers for the stabilisation of unknown steady states of chaotic systems
18th May
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Andrew Kennedy (Microsoft Research)
Untrustworthy Programming Language
25th May
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Peter Welch (University of Kent)
Communicating Mobile Processes

(2005, April)

7th Apr
(14:00h)
QMUL
ITL MF
Reading Group
Proof Carrying Code
by George Necula
12th Apr
(13:00h)
QMUL
Tea room
Lab Lunch
Pasquale Malacaria
Non-interference and independence of random variables
11-15 Apr


Birmingham
PhD Summer School
Midlands Graduate School
Department is funding L&S PhD students
18th Apr
(15:00h)
QMUL
CS446
IMC / Theory Seminar
Antonio Cerone (The University of Queensland)
Formal Analysis of Human-Computer Interaction using Model-checking
20th Apr
(9h--5h)
King's
London Theory Day
Theory groups from QM, Imperial and King's (programme here)
26th Apr
(13:00h)
QMUL
Tea room
Lab Lunch
Thomas Forster
De-linearising Ehrenfeucht-Mostowski
28th Apr
(14:00h)
QMUL
ITL MF
Reading Group
Organizer: Max Kanovich
28th Apr
(15:30h)
QMUL
CS446
Joint Queen Mary/Imperial Seminar
Jean-Christophe Filliâtre (Université Paris Sud)
Verifying C and Java programs

(2005, March)

1st Mar
(13:00h)
QMUL
Tea room
Lab Lunch
Graham White
1st Mar
(14:00h)
QMUL
PH602
Distinguished EE Seminars
John Mashey
Summarizing Benchmarks in no Mean Feat
2nd Mar
(15:30h)
QMUL
CS446
Distinguished Seminars
Dr Ann Blandford (UCL Interaction Centre)
The digital library and the user: understanding usability, acceptability and design
3rd Mar
(11:00h)
QMUL
CS337
Joint Queen Mary/Imperial Seminar
Jesus Almansa (BRICS)
Embedding the Universal Composability framework into PPC
3rd Mar
(14:00h)
QMUL
ITL MF
Reading Group
Local Reasoning about the Programs that Alter Data Structures
by Peter O'Hearn, John Reynolds and Hongseok Yang
9th Mar
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Ulrich Berger (University of Swansea)
The role of continuity in the computational interpretation of classical proofs
10th Mar
(14:00h)
QMUL
ITL MF
Reading Group
The Direct Simulation of Minsky Machines in Linear Logic
Max Kanovich
15th Mar
(13:00h)
QMUL
CS337
Lab Lunch
Guest Sofiène Tahar
16th Mar
(15:30h)
QMUL
Distinguished Seminars
Prof Chris Chapman (Southampton University)
Getting the full benefits from risk management processes
17th Mar
(14:00h)
QMUL
ITL MF
Reading Group
Girard's System F
23rd Mar
QMUL
NETCA Networks day
Afternoon of seminars
Topic: Mathematics for Networks

(2005, February)

2nd Feb
(15:30h)
QMUL
CS447
Distinguished Seminars
Tom Melham (University of Oxford)
Practical Formal Verification at an Industrial Scale
9th Feb
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Eike Ritter (University of Birmingham)
A Games Model for Classical Proofs
10th Feb
(15:30h)
QMUL
ITL MF
Reading Group
Geometry of Interaction
by Jean-Yves Girard
16th Feb
(15:30h)
QMUL
CS447
Distinguished Seminars
Luc Steel (Sony Computer Science Laboratory)
The Origins of Language and Meaning
17th Feb
(15:30h)
QMUL
ITL MF
Reading Group
Types, Abstraction and Parametric Polymorphism
by John Reynolds
22nd Feb
(14:00h)
QMUL
ITL GF
Control, Dynamics and Logic Seminar
Stephen Pollock (Department of Economics, QMUL)
Comparative Economic Cycles
23rd Feb
(15:30h)
QMUL
CS338
Joint Queen Mary/Imperial Seminar
Fred Barnes (University of Kent)
occam-pi and RMoX
24th Feb
(15:30h)
Imperial
room 418
Joint Queen Mary/Imperial Seminar
Tom Chothia (École Polytechnique)
Guessing Attacks in the pi-calculus, with a Computational Justification
24-25 Feb
(10am-5pm)
QMUL
4th Annual Postgraduate Conference
(further info here)


Pre-2004 Seminars

Eike Ritter - A Games Model for Classical Proofs
Prof Hai Zhuge - Introduction to China Knowledge Grid and Semantic Grid Research
Theodore Hong (Imperial) - Experiences with the Freenet Peer-to-Peer Information Publishing Network
Barry Jay (University of Technology, Sydney) The pattern calculus
Maribel Fernandez (KCL) - Explicit Substitutions without Alpha-Conversion
Byron Cook (Microsoft Research) Theorem proving in SLAM
Phil Scott (Ottawa) - Geometry of Interaction and the Dynamics of Proofs
Carsten Fuhrmann (Bath) - On the Geometry of Interaction for Classical Logic
Ian Mackie (King's College, London) - Geometry of Interaction Machine (10 years on)
Daniele Varacca (ENS Paris) - Semantic Subtyping for the pi-calculus
Bob Coecke (Oxford) -Probabilities in Abstract Quantum Mechanics
Alessandra Di Pierro (Pisa) - Probabilistic program analysis for quantitative reasoning about security properties
Franck van Breugel (York) - Behavioural Pseudometrics
Herbert Wiklicky (Imperial) - Operator Algebras and the Semantics of Probabilistic Languages
David Teller (ENS Lyon) - The Pi-Calculus, Finalisation and Garbage Collection
Jim Royer (Syracuse) - Adventures in Higher-Type Complexity
Richard Bornat (Middlesex) - Permissions and Concurrency: A breakthrough
Matthew Parkinson(Cambridge) -  When separation logic met Java
Masahito Hasegawa (Kyoto) - On a complete axiomatization of delimited continuations
Olivier Danvy (BRICS) - A Rational Deconstruction of Landin's SECD Machine
Prakash Panangaden (McGill) - Quantum Predicate Transformers
Martin Berger (QMUL) - Genericity and the Pi-Calculus
Catuscia Palamidessi (Inria Future/LIX) The probabilistic asynchronous pi-calculus
Joe Hurd (Oxford) - Probabilistic Guarded Commands Mechanized in HOL
David Schmidt (Kansas State) - Extending over-approximating models: an introduction to mixed models and separation logic
Neil Evans (Royal Holloway) - Verifying Security Protocols: Tailoring the Rank Function Approach for Tool Support
Olivier Laurent (CNRS/Paris VII) Polarized proof-nets for the lambda-mu calculus
Ian Stark (Edinburgh) - Free-algebra models for the pi-calculus
Dan Ghica (Oxford) - Angelic Semantics of Fine-Grained Concurrency
Christie Bolton (Oxford) - On the refinement of state-based and event-based models
Dominic Duggen (Stevens Institute) - Type-Based Distributed Access Control
Mariongiola Dezani (Turin) - A  calculus with bounded capacities
Michael Huth (Imperial) - Robust models for generalized model checking
Vasco Vasconcelos (Lisbon) - Session types for inter-process communication
Claudia Faggian (Cambridge) - Ludics: dynamics and interactive observability
Robin Milner (Cambridge) - tba
Gavin Lowe (Oxford) - On Distributed Security Transactions that use Secure Transport Protocols
Richard Jones (Kent) - Beyond the Beltway
Conor McBride (Durham) - Leibniz and the Zipper
Geoff Sharman (IBM UK) - What is transaction processing and why is it important?
Marta Kwiatkowska (Birmingham) - PRISM: Probabilistic Symbolic Model Checker
Russ Harmer (Paris) - Doing dataflow in PCF
Margarita Korovina (Aarhus) - Fixed Points on Abstract Structures without the Equality Test
Abbas Edalat (Imperial) - Domain Theory and Differential Calculus
Greg Pytel (Imperial) - Fragmented Database Management Systems
Andrzej Murawski (Oxford) - On program equivalence in Idealized Algol
Peter Johnstone (Cambridge) - How to survive without complements
Bill Rounds (Univ. of Michigan) - The phi-calculus, an extension of the pi-calculus to hybrid systems
Carsten Fuehrmann (Bath) - Varieties of Effects
Riccardo Pucella (Cornell) - Security Protocol Analysis and Algorithmic Knowledge
Prahlad Sampath (Teamphone) - Modelling multi-agent reactive systems
John Reynolds (CMU) - Separation Logic: A Logic for Shared Mutable Data Structures
Steve Schneider (Royal Holloway) - Non-interference, may testing, and compositionality
Luca Cardelli (Microsoft Research) - Spatial Logics for Distributed Systems
Martin Otto (Swansea) - Bisimulation, Unravellings, Covers
Javier Esparza (Edinburgh) - Model checking pushdown processes
Thorsten Altenkirch (Nottingham) - Generic Programming Within Dependently Typed Programming
Uwe Nestmann (EPFL Lausanne) - Modeling Consensus in a Process Calculus
Mark Steedman (CogSci Edinburgh) - Temporality in AI Planning and Natural Language Semantics
Tim Harris (Cambridge) - Lock-free data structures
Ant Rowstron (Microsoft Research) - Flour Power: From PAST to present
Hayo Thielecke (Birmingham) - Comparing Control Constructs by Double-barrelled CPS
Michael Rathjen (Leeds) - The Axiom of Choice in Constructive Set Theory
Andy Gordon (Microsoft Research) - Types and effects for asymmetric cryptographic protocols
Nick Benton (Microsoft Research) - Modern Concurrency Abstractions for C#
Federico Crazzolara (Cambridge) - Events in Security Protocols
Uday Reddy (Birmingham) - Polymorphic types and parametric limits
Richard Stallman (FSF) - Copyright vs Community in the Age of Computer Networks (not a JTS)
Jon Crowcroft (Cambridge) - What "We" Got Wrong with IP
Cedric Fournet (Microsoft Research ) - Stack Inspection: Theory and Variants
Herbert Wiklicky (Imperial) - Confidentiality: Searching for the Hole in the Bucket?
Giuseppe Longo (CNRS , ENS) - On the proofs of some unprovable propositions
Ken Moody   Cambridge) - OASIS:  Architecture, Model and Implementation
Iain Phillips (Imperial) - CCS with Priority Guards
Massimo Merro (Sussex) - Bisimulation Congruences in Safe Ambients
Peter Sewell (University of Cambridge) - The UDP Calculus: Rigorous Semantics for Real Networking
Nobuko Yoshida (Leicester) - Strong Normalisation in the pi-Calculus
Andy Pitts (Cambridge) - Nominal Logic:  A First Order Theory of Names and Binding
Marcelo Fiore (University of Cambridge) - Semantic Analysis of Definability and Normalisation for Typed Lambda Calculi
Alex Simpson (Edinburgh) -  Relating toposes and first-order set theories and Verifying Temporal Properties Using Explicit Approximations: Completeness for Context-free Processes
Jim Laird (Sussex) - Fully abstract bidomain models of the lambda-calculus
Martin Hofmann (LMU Munich) - Read Only Types and Functional In-place Update
Philipa Gardner  (Imperial College) - A Process Logic for Querying  Graphs
John Reynolds  (CMU) - Further Reasoning About Shared Mutable Data Structure
Keye Martin (Oxford) - The unification of metric spaces and domains
Stephen Brookes (CMU) - Transfer Principles for Reasoning about Concurrent Programs
Kohei Honda (QMUL) - Sequentiality and the Pi-Calculus    
Roberto Giacobazzi (Univ. of Verona) - Abstract domains in 3D: completeness and refinements in static program analysis and abstract model checking
Richard Evans (Lionhead) - AI in Computer Games: The Use of AI Techniques in Black & White
Pasquale Malacaria (QMW) - Security via Insecurity
Jan Juerjens  (Oxford) -
Don Syme (Microsoft Research) - Some .NET Framework Research at MSR Cambridge
Thomas Ball and Sriram K. Rajamani (Microsoft Research) - Automatically Validating Temporal Safety Properties of Interfaces
Bernhard Reus (Sussex) - A Hoare-Calculus for an OO-language
Samson Abramsky (Oxford) - Sequentiality vs. Concurrency in Games and Logic
Peter O'Hearn (QMW) - Local Reasoning about Shared Mutable Data Structure
Cedric Fournet (Microsoft Research) - Mobile Values, New Names, and Secure Communications
Thomas Forster (University of Cambridge) - Better-Quasi-Orderings and Coinduction
Luke Ong (Oxford) - A Polytime-Complete Functional Language based on Light Logic
Lucian Wischik (University of Cambridge) - Explicit fusions, and a distributed implementation of the pi calculus
Anindya Banerjee (Stevens IT) - Semantics-based Design and Correctness of Control-flow Analysis-based Program Transformations
Eric Goubault  (CEA) - Geometric semantics for the analysis of concurrent and distributed software
Peter Sewell (University of Cambridge) - Modules, Abstract Types, and Distributed Versioning
Alberto Momigliano (Leicester) - Elimination of Negation in a Logical Framework
Andy Gordon (Microsoft Research) - Authenticity by Typing in Security Protocols
Simon Peyton-Jones (Microsoft Research) - C--: a portable assembly language that supports garbage collection
Benjamin Pierce (UPenn) - Advanced Module Systems: a Guide for the Perplexed and Regular Expression Types for XML
Cristiano Calcagno (Universita di Genova and QMW) - Stratified Operational Semantics for Safety and Correctness of Region Calculus
Herbert Wiklicky   (Imperial College) - The Semantics of Quantum Computation
Sophia Drossopoulou (Imperial College) - Towards an abstract model of Java dynamic linking and verification
Pawel Wojciechowski (EPFL Lausanne) - Language and Communication Infrastructure Design for Mobile Computation
Steve Vickers  ( Open University) - Generalized topological spaces: not enough opens, so you use sheaves
Dieter Spreen (UG Siegen) - The largest Cartesian closed category of domains, considered constructively
Bjorn Victor (Uppsala University) - The Fusion calculus, Solos, and their graphical representation
Pat Hill (Leeds) - Proving Properties of Logic Programs
Yoshiki Kinoshita (ETL, Osaka) - On Completeness in Refinement
Julian Bradfield   Edinburgh) - Fixpoints, Games and Arithmetic
Jim Laird ( Sussex) - A fully abstract semantics of locally bound exceptions
Matthew Hennessy (Sussex) - Information flow vs. resource access in the asynchronous pi-calculus
Russ Harmer (Paris VII) - Probabilistic Game Semantics
Cliff Jones (Newcastle) - Dependability and Formal Methods
Giuseppe Longo   CNRS, ENS) - The geometric intelligibility of space and the foundation of mathematical knowledge
Andrei Sabelfeld (Chalmers) - PER Model of Secure Information Flow
Rod Burstall   Edinburgh) - A proof tool for teaching Natural Deduction and Induction
Greg Restall (Macquarie) - Quantifiers in Frames for Substructural Logics
Maribel Fernandez (ENS) -   A calculus for interaction nets  
Ian Mackie ( LIX, Ecole Polytechnique) - Closed reductions in the lambda calculus
Adrian Mathias (Universidad de Los Andes) - The Strength of Mac Lane Set Theory
Robin Hirsch (UCL) - Logic: by quantifiers or by algebra
James Harland   RMIT) - Programming languages for linear logic
Jean-Pierre Talpin (IRISA) - A theory of hierarchic transition systems
Gian Luca Cattani (Cambridge) - Weak Bisimulation and Open Maps
P. N. Benton (Microsoft Research) - Monads, Effects and Transformations
Randy Pollack  (Durham / Edinburgh) - Names, binding and substitution
Marta Kwiatkowska   Birmingham) - Symbolic Probabilistic Model Checking
Furio Honsell  ( Udine) - Pre-logical relations
John Reynolds (CMU ) - Reasoning about shared mutable data structure
Andy Gordon   Microsoft Research) - Mobile Ambients
Simone Martini (Udine) - Complexity of optimal sharing in Elementary linear logic
Radha Jagadeesan   Loyola, Chicago) - Continuous Markov processes --- Approximations and metrics
David Nowak  (IRISA-Rennes) - Synchronous Structures
Jeremy Gunawardena (HP BRIMS) - Digital circuits and nonexpansive maps
Colin Stirling (Edinburgh) - The joys of bisimulation
Andy Pitts (Cambridge) - A New Approach to Abstract Syntax Involving Binders
Andrew Moran (Chalmers) - Erratic Fudgets: A Semantic Theory for an Embedded Coordination Language
Simon Peyton-Jones (Microsoft Research) A semantics for imprecise exceptions
Marcelo Fiore (Sussex) - Abstract syntax and variable binding
Tony Hoare (Oxford) - A trace model of pointers and objects
Paul Levy (Queen Mary) - Call by Push Value
Nik Swoboda (Indiana and ATR) - Observation: Understanding how information can be extracted from diagrams
Stephen Read (St Andrews) - Truthmakers and the Disjunction Thesis
Martin Hofmann (Edinburgh) - Semantical analysis of higher-order abstract syntax
Juan Bicarregui (Imperial / Rutherford) - Formal Methods - The truth is out there
Mike Gordon   Cambridge) - 21 Years of Hardware Verification
S. S. Wainer (Leeds) - Proof Theory and Computational Complexity
Christian Urban (Cambridge) - Strong Normalisation of Cut-Elimination in Classical Logic
Steven Vickers (Imperial) - Topical Categories of Domains
Anna Ingolfsdottir (Aalborg) - Towards Verified Lazy Implementation of Concurrent Value-Passing Languages