General Information Contributed Talks Program Past workshops
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 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.
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)
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.
Page maintained by:Ralph Matthes https://www.irit.fr/~Ralph.Matthes/
Last modified (date in French): ven. mai 16 16:01:35 CEST 2014