Proof, Computation, Complexity 2018
Seventeenth International Workshop
July 19-20, 2018, Bonn, Germany
last-minute changes to programme (none has been rescheduled), programme ends earlier on Thursday
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
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.
Most participants will have arrangements with the HIM. We will therefore refrain from giving further indications.
in alphabetic order
- 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
- 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
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
the uniform 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.
The accepted contributed talks:
Thursday July 19, 2018
Invited Speaker 1: Hajime Ishihara
10.30-11.00 coffee break
11.00-13.10 Invited Speaker 2: Hugo Herbelin
Amirhossein Akbar Tabatabai
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
10.30-11.00 coffee break
11.00-12.20 Takako Nemoto
14.30-16.00 Invited Speaker 5: Oliver Kullmann
16.00-16.30 coffee break
There 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
There is no specific registration procedure, and no registration fee will be charged - the coffee breaks are taken care of by the HIM. Lunches and dinners have to be organized by the participants individually, however, there is a suggestion for dinner on Thursday, see above.
PCC steering committee
Program Committee PCC 2018
- 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
Reinhard Kahle, Ralph Matthes, and Peter Schuster
Past PCC workshops
- 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.
was held in Dresden in conjunction with the Summer School on Proof Theory and Automated Theorem Proving.
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): mer. sept. 12 14:13:58 CEST 2018