Proof, Computation, Complexity 2014

General Information

Aims and Scope

The aim of PCC is to stimulate research in proof theory, computation, and complexity, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in computer science, as well as new developments in proof theory motivated by computer science demands. Specific areas of interest are (non-exhaustively listed) foundations for specification and programming languages, logical methods in specification and program development including program extraction from proofs, type theory, new developments in structural proof theory, and implicit computational complexity.

The context

The workshop has been rescheduled to fit better with affordable tickets on Friday. Instead of possibly Thursday afternoon (May 15) and the full Friday (May 16), the planning is now as follows.

Programme

Thursday May 15 (Institut Henri Poincaré, ground floor, amphitheatre Hermite)
10:40-11:10 arrival, visit at registration desk to pick up badge, etc.
11:10-12:10 (joint session with TYPES)
            Andy Pitts (University of Cambridge)
            Nominal sets and dependent type theory
12:10-14:00 lunch (joint with TYPES, 10 minutes walking distance from IHP in Ministry of Higher Education and Research)
14:00-14:05 opening of PCC (second floor of IHP, Room 201, PCC in parallel with TYPES until coffee break)
14:05-14:45 Anupam Das (INRIA and LIX, Ecole Polytechnique)
            Towards a Bounded Arithmetic for Analytic Deep Inference
14:45-15:25 Susumu Yamasaki (Okayama University, Japan)
            Structures to Generate Implementable Action Sequences and their Compositions for Semiring
15:25-15:55 coffee break (10 minutes later than for TYPES)
15:55-16:35 Lev Gordeev (Tuebingen University, Ghent University): Toward optimal encoding of terms and proofs
16:35-17:15 Lars Kristiansen (University of Oslo): How to state and prove Gödel's 1st Incompleteness Theorem - a glance at a new textbook on mathematical logic and computability theory
17:15-17:55 Rene Gazzari (University of Tübingen): Occurrences
18:00 building closes 

Friday May 16 (Institut Henri Poincaré, ground floor, amphitheatre Hermite)
 9:30-10:10 Stéphane Graham-Lengrand (LIX, CNRS and École Polytechnique)
            Structuring proofs with decision procedure calls & applications to SMT-solving
10:20-11:00 Ulrik Buchholtz (University of Bern)
            Survey of Systems of Strength H(1)
11:00-11:30 coffee break
11:30-12:10 Paul Shafer (Ghent University)
            Every non-zero honest elementary degree has the cupping property
12:15-12:55 Ralph Matthes (IRIT, CNRS and Univ. de Toulouse): A finitary analysis of reductive proof search
lunch starting effectively 13:15 (outside IHP, same as the day before)

PCC steering committee

• Reinhard Kahle, Universidade Nova de Lisboa, Portugal
• Lars Kristiansen, University of Oslo, Norway

Program Committee PCC 2014

• Stéphane Graham-Lengrand, LIX, CNRS and École Polytechnique, France
• Reinhard Kahle, Universidade Nova de Lisboa, Portugal (co-chair)
• Lars Kristiansen, University of Oslo, Norway
• Ralph Matthes, IRIT, CNRS and Univ. de Toulouse, France (co-chair)
• Isabel Oitavem, Universidade Nova de Lisboa and CMAF, UL, Portugal

Contributed talks

• Ulrik Buchholtz (University of Bern): Survey of Systems of Strength H(1)
• Anupam Das (INRIA and LIX, Ecole Polytechnique): Towards a Bounded Arithmetic for Analytic Deep Inference
• Rene Gazzari (University of Tübingen): Occurrences
• Lev Gordeev (Tuebingen University, Ghent University): Toward optimal encoding of terms and proofs
• Paul Shafer (Ghent University): Every non-zero honest elementary degree has the cupping property
• Susumu Yamasaki (Okayama University, Japan): Structures to Generate Implementable Action Sequences and their Compositions for Semiring

Submission information was

We solicit contributions in the fields of PCC, non-exhaustively described above. Please register a contribution at the EasyChair site for PCC 2014. This consists in a title, a short text-only abstract and the PDF file of a LaTeX abstract that fits on one page in format A4.

The abstracts should allow the organizers to see if the talks fit with PCC 2014, to group the talks into sessions, to see if the extension to Thursday afternoon is justified by the quality of the submissions, etc. Even a short abstract can give a good view of the proposed contribution. A formula in the right place may stand for several sentences.

PCC is intended to be a lively forum for presenting and discussing recent work. Progress on a not yet satisfactorily solved problem may well be worth presenting - in particular if the discussions during the workshop might lead towards a solution.

Important Dates

• Deadline for proposing a contributed talk: Monday, March 3, 2014
• Notification of acceptance: Tuesday, April 1st, 2014 - was delayed until April 13
• Early registration (through TYPES 2014): deadline April 19

Past PCC workshops

• PCC 2013 was held in Toulouse, France, colocated with TYPES 2013.
• PCC 2012 was held in Copenhagen, Denmark.
• PCC 2011 was held in Ghent, Belgium.
• PCC 2010 was held in Bern, Switzerland.
• PCC 2009 was held at LORIA - Nancy, France.
• PCC 2008 was held in Oslo, Norway.
• PCC 2007 was held in Swansea, Wales, colocated with the British Mathematical Colloquium 2007.
• PCC 2006 was held in Ilmenau, Germany.
• PCC 2005 was held in Lisbon as affiliated Workshop to ICALP'05.
• PCC 2004 was held in Dresden in conjunction with the Summer School on Proof Theory and Automated Theorem Proving.
• PCC 2003 was held in Dresden, in conjunction with the Summer School on Proof Theory, Computation, and Complexity.
• PCC 2002 was held in Tübingen.

Page maintained by:

Last modified (date in French): ven. mai 16 16:01:35 CEST 2014