Computer Science Proof, Complexity and Verification Seminar Series
The idea for the PCV Seminar Series grew amongst members of our theory group who felt a need for a platform to present our work in the area of Proof Theory, Complexity Theory and Program Verification. It is intended to be a high level research seminar where we can discuss latest ideas and results, as well as address technical issues, and are able to invite speakers from outside.
In the beginning of 2005, this idea turned into the PCV Seminar.
Organizers so far have been Markus Michelbrink (see here for talks organised by him), Will Harwood, Klaus Aehlig, and Monika Seisenberger. From January 2010 on, Fredrik Nordvall Forsberg and Matthew Gwynne organise the seminar.
20102011

Thursday 14th October 2010, 14:00, Far134 (Video Conferencing Room)
Pierre Clairambault (University of Bath)
The Biequivalence of Locally Cartesian Closed Categories and MartinLöf Type Theory with Pi, Sigma, and Extensional Identity Types

Thursday 28th October 2010, 14:00, Board Room
John Power (Bath University)
Coalgebraic Semantics for Parallel Derivation Strategies in Logic Programming

Thursday 4th November 2010, 14:00, Robert Recorde Room
No talk due to 9th Wessex Theory Seminar

Thursday 11th November 2010, 14:00, Far134 (Video Conferencing Room)
Chris Broadbent (Oxford)
Collapsible Pushdown Graphs and FirstOrder Logic  Navigating the fringe of decidability

Tuesday 23rd November 2010, 14:00, Robert Recorde Room
Paulo Oliva (Queen Mary)
The Theory of Selection Functions

Thursday 25th November 2010, ,
No talk. Level 1 Away day

Thursday 2nd December 2010, 9am  3pm, Board Room
Model checking workshop

Thursday 9th December 2010, 14:00, Far134 (Video Conferencing Room)
Alessio Guglielmi (University of Bath)
Removing Syntax from Proof Theory

Monday 17th January 2011, 11:00, Robert Recorde Room
Jan Pich (Charles University in Prague)
NisanWigderson generators in proof systems with forms of interpolation

Thursday 10th February 2011, 14:00, Video Conferencing Room  Far 134
Berndt Muller (University of Glamorgan)
The ModelChecking Problem for ResourceBounded Logics

Thursday 24th February 2011, 14:00, Far134 (Video Conferencing Room)
Martin Churchill (University of Bath)
Imperative Programs as Proofs via Game Semantics

Thursday 31st March 2011, 14:00, Far134 (Video Conferencing Room)
Isabel Oitavem (Lisboa)
Recursiontheoretic characterization of FPH

Thursday 31st March 2011, 14:45, Far134 (Video Conferencing Room)
Reinhard Kahle (Lisboa)
An applicative recursion scheme for FPH

Thursday 5th May 2011, 14:00, Far134 (Video Conferencing Room)
Matthew Gwynne (Swansea University)
On the hardness of (satisfiable) conjunctive normal forms

Thursday 12th May 2011, 14:00, Far134 (Video Conferencing Room)
Andy King (Kent)
Automatic Abstraction for Congruences: A Story of Beauty and the Beast