General Information Invited Speakers Programme Contributing Talks Important Dates Registration 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 is organized as extra workshop (besides the three major workshops) of the trimester on "Types, Sets and Constructions" of the Hausdorff Research Institute for Mathematics (HIM), see the official announcement on the HIM site. All talks are held in HIM lecture hall, Poppelsdorfer Allee 45, Bonn.

- Hugo Herbelin: Computing with Gödel's Completeness Theorem
- Krivine, followed by Berardi and Valentini, explored in the 90's how
to compute with Gödel's completeness using "exploding models" and
A-translation. We later gave with Ilik a direct computational
formulation of Henkin's proof.

In the talk, we shall study yet another approach to compute with Gödel's completeness theorem by observing that the Kripke forcing translation of the statement of completeness is a statement of completeness with respect to Kripke semantics. Going then the other way round, looking at direct-style provability for the Kripke forcing translation the same way as classical logic can be seen as direct-style provability for the double-negation translation, we obtain a proof of Gödel's completeness with "side effects" whose computational content is to "reify" a proof of validity into a proof of derivability. - Hajime Ishihara: Constructive reverse mathematics: an introduction and recent results
- This talk presents an introduction to constructive reverse mathematics (CRM) with some recent results. The aim of CRM is to classify various theorems in intuitionistic, constructive recursive and classical mathematics by logical principles, function existence axioms and their combinations. We review some results in classical reverse mathematics (Friedman-Simpson program), and axioms of intuitionistic and constructive recursive mathematics with their consequences to motivate CRM. Then we present some results of CRM with and without countable choice, and recent results in CRM without countable choice.
- Oliver Kullmann: The Science of Brute Force
- In SAT solving we have the New and the Old, modern SAT solving versus
old-fashioned backtracking (and look-ahead). As the success of the
solution of the Pythagorean Triples Problem
`https://en.wikipedia.org/wiki/Boolean_Pythagorean_triples_problem`shows, indeed the combination of Old and New can be best in many cases, and I will discuss the landscape of these ideas. - Michael Rathjen: The ubiquity of Schütte's search trees
- Progressions of theories along paths through Kleene's $\mathcal O$,
adding the consistency of the previous theory at every successor step,
can deduce every true $\Pi^0_1$-statement. This was shown by Turing in
his 1938 thesis who called these progressions
ordinal logics . In 1962 Feferman proved the amazing theorem that progressions based on theuniform reflection principle can deduce every true arithmetic statement. In contrast to Turing's, Feferman's proof is very complicated, involving several cunning applications of self-reference via the recursion theorem.

Using Schütte's method of search trees (or decomposition trees) for ω-logic, however, one can give a rather transparent proof. If time permits, I shall present a general proof-theoretic machinery, based on search trees, for investigating statements about well-orderings from the point of view of reverse mathematics. - Giuseppe Rosolini: Quotient completions and applications
- The notion of elementary quotient completion of a Lawvere elementary doctrine introduced by Maietti and Rosolini proved to be a generalization of the notion of the exact completion of a category with finite products and weak equalizers which is a crucial step in the construction of computational models such as Hyland's Effective Topos.

We describe that completion and focus on the special class of elementary doctrines called triposes, introduced by Hyland, Johnstone, and Pitts. We characterize those triposes whose elementary quotient completion is an arithmetic quasitopos, i.e. a quasitopos equipped with a natural number object.

This suggests that the notion of elementary topos may be too strong to model computational aspects of mathematics.

- list without abstracts
- list with abstracts (for half of them also a PDF version)

Thursday July 19, 2018 9.00-10.30 Opening Invited Speaker 1: Hajime Ishihara David Cerna 10.30-11.00 coffee break 11.00-13.10 Invited Speaker 2: Hugo Herbelin Amirhossein Akbar Tabatabai Tatsuji Kawai lunch 15.15-16.00 Invited Speaker 3: Giuseppe Rosolini 16.00-16.30 coffee break 16.30-17.50 Hannes Diener & Robert Lubarsky Josef Berger & Gregor Svindland Friday July 20, 2018 9.00-10.30 Invited Speaker 4: Michael Rathjen David Natingga 10.30-11.00 coffee break 11.00-12.20 Takako Nemoto Iosif Petrakis lunch 14.30-16.00 Invited Speaker 5: Oliver Kullmann Lars Kristiansen 16.00-16.30 coffee breakThere will also be the opportunity to join the organizers for a dinner on Thursday evening at 7 p.m., in the restaurant Zum Treppchen (the reservation has been confirmed). The participants will be asked if they intend to join (everybody has to pay for herself/himself) before lunch on Thursday.

We solicit contributions in the fields of PCC, non-exhaustively
described above. Please register a contribution at the EasyChair site
for PCC 2018: `https://easychair.org/conferences/?conf=pcc20180` (please
note the trailing zero).
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 latter PDF file is not compulsory on first submission.)

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.

- Deadline for proposing a contributed talk: May 28, 2018 (AoE),
*but the submission server remained still open for some days* - Notification of acceptance: June 18, 2018

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

- Reinhard Kahle, Universidade Nova de Lisboa, Portugal
- Lars Kristiansen, University of Oslo, Norway
- Ralph Matthes, IRIT, CNRS and Univ. de Toulouse, France
- Isabel Oitavem, Universidade Nova de Lisboa, Portugal
- Peter Schuster, Univ. of Verona, Italy

- PCC 2017 was held in Göttingen, Germany, including an unveiling ceremony of a commemorative plaque for Paul Bernays on his former house.
- PCC 2016 was held in Munich, Germany, including a day-long special session to celebrate the 60th birthday of Ulrich Berger.
- PCC 2015 was held in Oslo, Norway, colocated with the Symposium on the occasion of the retirements of Herman Ruge Jervell and Dag Normann.
- PCC 2014 was held in Paris, France, colocated with TYPES 2014.
- 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:

Ralph MatthesLast modified (date in French): mer. sept. 12 14:13:58 CEST 2018