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.
20092010

Wednesday 2nd September 2009, 14:00, Robert Recorde Room
Robin Adams (Royal Holloway, University of London)
Proof and definition in logic and type theory

Thursday 15th October 2009, 14:00, Robert Recorde Room
Ana Cavalcanti (York)
Talk in the Algebraic Specification Seminar: Circus: Z and CSP for refinement

Thursday 22nd October 2009, 14:00, Far134 (Access grid room)
Yoshiki Kinoshita (AIST Japan)
Joint talk with Bath University: Landau in Agda

Thursday 29th October 2009, 14:00  17:00, Robert Recorde Room
Speakers: Dirk Pattinson, Yoshiki Kinoshita, John Power (Imperial College, AIST Japan, Bath University)
4th Wessex Theory Seminar

Thursday 5th November 2009, 14:00, Robert Recorde Room
Robin Milner (University of Cambridge)
Talk in the Computer Science Colloquium

Thursday 12th November 2009, 14:00, Far134 (Video Conferencing Room)
Martin Brain (Bath University)
Future Directions in Logic Programming

Thursday 19th November 2009, 14:00, Robert Recorde Room
Ursula Martin (Queen Mary)
Talk in the Computer Science Colloquium

Thursday 3rd December 2009, 14:00, Far134 (Video conferencing room)
Rob Arthan (Lemma 1 Ltd/Queen Mary)
Decision Problems in Geometry and Analysis

Thursday 10th December 2009, 14:00, Far134 (Video conferencing room)
Jens Blanck (Swansea)
Canonical effective subalgebras of classical algebras as constructive metric completions

Thursday 11th February 2010, 14:00, Far134 (Video Conferencing Room)
Fredrik Nordvall Forsberg (Swansea)
Inductiveinductive definitions

Thursday 4th March 2010, 14:00, Video conferencing room  Far 134
Ulrich Berger (Swansea University)
Program Extraction From Proofs: Induction and Coinduction

Thursday 11th March 2010, 14:00, Far134 (Video Conferencing Room)
Nathan Bowler (Cambridge)
Joint talk with Bath University: Multicategories as a tool for building categories of games

Thursday 18th March 2010, 14:00, Video Conferencing Room  Far134
Nguyen Van Tang (AIST Japan)
A Hybrid Approach to Verify A Train Fare Calculation System Using Testing and Theorem Proving.

Tuesday 13th April 2010, 14:00, Board Room
Thomas Strahm (Bern)
Two unfoldings of finitist arithmetic

Thursday 15th April 2010, 11:0017:00, Board Room
Research Meeting with Makoto Takeyama and Kinoshita Yoshiki, AIST Japan

Tuesday 20th April 2010, 14:00, Board Room
Marcin Jurdzinski (Warwick University)
Lemke's algorithm for discounted games

Thursday 22nd April 2010, 14:00, Far134 (Video Conferencing Room)
Alan Frisch (York)
Joint talk with Bath University: The Rules of Modelling Automatic Generation of Constraint Programs

Thursday 6th May 2010, 14:15, Video Conferencing Room  Far134
Oliver Kullmann (Swansea)
Exact Ramsey theory: GreenTao numbers and SAT

Thursday 20th May 2010, 14:00, Video Conferencing Room  Far134
Anton Setzer (Swansea)
Combining Automated and Interactive Theorem Proving in Agda

Thursday 27th May 2010, 14:00, Video Conferencing Room  Far134
Dirk Pattinson (Imperial College)
Global Caching for Coalgebraic Description Logics

Thursday 1st July 2010, 14:00, Video Conferencing Room  Far134
Jim Laird (Bath)
Game Semantics for a Generic Programming Language

Thursday 22nd July 2010, 14:00, Robert Recorde Room
Cesare Tinelli (University of Iowa)
SMTbased model checking of data flow programs

Thursday 5th August 2010, 14:00, Robert Recorde Room
Sylvain Dailler (Lyon, currently Internship Swansea)
Program extraction using real arithmetic in Coq.

Thursday 12th August 2010, 14:00, Robert Recorde Room
Syllvain Dailler (Lyon, currently Internship Swansea)
Program extraction using real arithmetic in Coq (Part II)