Two talks in the ICE-TCS seminar series
Luís Pinto and José Espírito Santo
This Thursday, 1st of September, we will have two talks (around 45 minutes each) in the ICE-TCS seminar series, given by José Espírito Santo and Luís Pinto, both from the University of Minho. The seminar takes place in room M109 at 14:00.
Luís Pinto will talk about Coinductive proof search for intuitionistic propositional logic.
José Espírito Santo will talk about Russell-Prawitz translation and atomic polymorphism.
The coinductive approach to proof search we present is based on three main ideas: (i) the Curry-Howard paradigm of representation of proofs (by typed lambda-terms) is extended to solutions of proof-search problems (a solution is a run of the proof search process that does not fail to apply bottom-up an inference rule, so it may be an infinite object); (ii) two typed lambda-calculi, one obtained by a conductive reading of the grammar of proof terms (acting as the universe for the mathematical definition of proof search concepts), the other by enriching the grammar of proof terms with a formal fixed-point operator to represent cyclic behaviour (acting as the finitary setting where algorithmic counterparts of those concepts can be found); (iii) formal (finite) sums are employed throughout to represent choice points, so not only single solutions but even entire solution spaces are represented, both coinductively and finitarily. In this seminar we will illustrate this approach for intuitionistic implication, including applications to inhabitation and counting problems in simply-typed lambda-calculus (e.g., results ensuring uniqueness of inhabitants related to coherence in category theory), and briefly overview an extension of the approach to polarized intuitionistic logic, which allows to obtain results about proof search for full intuitionistic propositional logic. Joint work with José Espírito Santo and Ralph Matthes.
We analyze the Russell-Prawitz encoding of intuitionistic disjunction by means of second-order quantification. At the level of proofs, the translation, in its simplest form, employs unrestricted universal instantiation. In recent years, attention has been devoted to alternatives which employ instantiation with atomic formulas only. We compare the various alternatives with the help of an auxiliary conversion that eliminates certain patterns of non-atomic instantiation. In the comparison, the telling case is the translation of commutative conversions: if one wants a strict simulation, then one needs the possibility of converting "at run time" a unrestricted universal instantiation - instead of having all universal instantiations employed in the translation forced to be atomic "at compile time". Joint work with Gilda Ferreira.
