Proof, Computation, Complexity 2018

Seventeenth International Workshop

July 19-20, 2018, Bonn, Germany

General Information    Invited Speakers    Programme    Contributing Talks    Important Dates    Registration    Past workshops   


News

last-minute changes to programme (none has been rescheduled), programme ends earlier on Thursday

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.

Venue

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.

Accommodation

Most participants will have arrangements with the HIM. We will therefore refrain from giving further indications.

Invited speakers

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 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 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.

Programme

The accepted contributed talks: 
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 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.

Contributing talks

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.

Important Dates

Registration

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.

Committees

PCC steering committee

Program Committee PCC 2018

Organizing Committee

Reinhard Kahle, Ralph Matthes, and Peter Schuster

Past PCC workshops



Page maintained by:

Ralph Matthes
https://www.irit.fr/~Ralph.Matthes/

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