## (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) |

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