The aim of PCC is to stimulate research in proof theory, computation, and complexity from a mathematical perspective, focusing on issues which combine logical and computational aspects. Topics may include applications of formal inference systems in mathematics and computer science, as well as new developments in proof theory motivated by mathematical and computer science demands. Specific areas of interest are (non-exhaustively listed) proof theory, 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 a one-week workshop at the Institut Mittag-Leffler of the Royal Swedish Academy of Sciences, see also the workshop web pages at Institut Mittag-Leffler.
Monday: Ralph Matthes: Some aspects of coinductive proof search in intuitionistic propositional logic Michael Rathjen: Geometric Theories, AC, and constructivity [better consult the author's personal page] Luís Pinto: Modal embeddings and calling paradigms [slides not available] Matthias Baaz: Analytic calculi for quantifier macros based on locally unsound rules Jan Bydzovsky: Consistency of circuit lower bounds with the Cook`s theory PV [slides not available] Sam Sanders: Plato and the foundations of mathematics [slides not available] Tuesday: Ulrich Kohlenbach: The Lion and Man Game and Proof Mining Andrei Sipos: The finitary content of sunny nonexpansive retractions Sonia Marin: Justification logic for modal logics on an intuitionistic base [slides not available] Lars Kristiansen: On Subercursive Representability of Irrational Numbers: Best Approximations, Contractions Maps and Continued Fractions [slides not available] Juvenal Murwanashyaka: On First-Order Bit Theory [slides not available] Federico Aschieri: Towards a concurrent lambda calculus (via linear logic) [slides not available] Wednesday: Bahareh Afshari: Direct interpolation for modal mu-calculus Graham Leigh: Past validities Alessio Guglielmi: Two Design Questions (web link to author-maintained page) Mattias Granberg Olsson: Partial conservativity for fix-point theories over Heyting arithmetic [blackboard talk] Paulo Guilherme Santos: A Computational Account Of Simplicity With A View Towards Hilbert’s 24th Problem [slides not available] Gerhard Jäger: The Power of Beta [slides not available] Anupam Das: From QBFs to MALL and back via focussing - Fragments of MALL for each level of the polynomial hierarchy Thursday: Hugo Herbelin: A unified logical structure to the axiom of choice, bar induction and some of their relatives Ugo Dal Lago: On Type Systems For Probabilistic Termination (web link to author-maintained page) Isabel Oitavem: The polynomial hierarchy of time [slides not available] Friday: Paulo Oliva: On “Approximate” Variants of Functional Interpretations Andrew Lewis-Smith: A Kripke Semantics for IŁL Erik Palmgren: From type theory to setoids and back: a setoid model of extensional Martin-Löf type theory
Page maintained by:
Ralph Matthes https://www.irit.fr/~Ralph.Matthes/Last modified (date in French): ven. sept. 13 15:17:35 CEST 2019