Proof, Computation, Complexity 2014

Thirteenth International Workshop

May 15-16, 2014, Paris, France

General Information    Contributed Talks    Program    Past workshops   

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

PCC 2014 is organized as a satellite event of TYPES 2014, to take place at the Institut Henri Poincaré in the heart of Paris. Registration for PCC 2014 is through the TYPES 2014 site for a low fee that covers mostly coffee and lunch breaks (early registration fees apply only until April 19).

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.


Every talk was scheduled for 40 minutes, including discussion and change of speaker.
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

Program Committee PCC 2014

Contributed talks

Accepted talks in alphabetic order.

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

Past PCC workshops

Page maintained by:

Ralph Matthes

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