View: session overviewtalk overviewside by side with other conferences

10:45 | Extracting Monadic Parsers from Proofs SPEAKER: Alison Jones ABSTRACT. This talk outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using a modified realisability interpretation, we extract provably correct and terminating programs from formal proofs. If the proof system is proven to be correct, then any extracted program is guaranteed to be so. By extracting parsers, we can ensure that they are correct, complete and terminating for any input. The work is ongoing, and is being carried out in the interactive proof system Minlog. |

11:30 | Intuitionistic Ancestral Logic SPEAKER: Liron Cohen ABSTRACT. We define pure intuitionistic Ancestral Logic (iAL), extending pure intuitionistic First-Order Logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL given by its realizer for transitive closure, TC. We derive this operator from the natural type theoretic definition of TC using intersection.
We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further show that iAL subsumes Kleene Algebras with tests and thus serves as a natural programming logic for proving properties of program schemes. We also extract schemes from proofs that iAL specifications are solvable. |

14:30 | Proof-search in natural deduction calculi for IPL SPEAKER: Camillo Fiorentini ABSTRACT. We address the problem of proof-search in the natural deduction calculus Ni for intuitionistic propositional logic (IPL). Our aim is to improve the usual n\"aive proof-search procedure where introduction rules are applied upwards and elimination rules downwards. In particular, we introduce Nbu, a sequent-style variant of Ni and we show that its derivations can be reduced in $\theta$-NF, a normal form (stronger than the usual one) where applications of $\lor E$ and $\to I$ satisfy additional conditions involving an evaluation relation $\theta$. This limits the application of such rules in proof-search and restricts the search space. |

15:15 | A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic SPEAKER: Sergey Melikhov ABSTRACT. In a 1985 commentary to his collected works, Kolmogorov remarked that his 1932 paper ("Zur Deutung der intuitionistischen Logik") "was written in hope that with time, the logic of solution of problems will become a permanent part of [a standard] course of logic. Creation of a unified logical apparatus dealing with objects of two types - propositions and problems - was intended." We describe such a formal system, QHC, which is a conservative extension of both the intuitionistic predicate calculus, QH, and the classical predicate calculus, QC. Moreover: - The only new connectives ? and ! of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC, regarded as posets. - Kolmogorov's double negation translation of propositions into problems extends to a retraction of QHC onto QH. - Goedel's provability translation of problems into modal propositions extends to a retraction of QHC onto its QC+(?!) fragment, which can be identified with the modal logic QS4. This leads to a new paradigm that views intuitionistic logic not as an alternative to classical logic that criminalizes some of its principles, but as an extension package that upgrades classical logic without removing it. The purpose of the upgrade is proof-relevance, or "categorification"; thus, if the classical conjunction and disjunction are to be modeled by intersection and union (of sets), the intuitionistic conjunction and disjunction will be modeled by product and disjoint union (of sheaves of sets). More formally, we describe a family of sheaf-valued models of QH, inspired by dependent type theory (not to be confused with the well-known open set-valued sheaf models of QH), which can be regarded as proof-relevant analogues of classical topological models of Tarski et al., and which extend to models of QHC. We also give an interpretation of some of these models in terms of stable solutions of algebraic equations; this can be seen as a proof-relevant counterpart of Novikov's classical interpretation of some Tarski models in terms of weighting of masses. The new paradigm also suggests a rethink of the Brouwer-Heyting-Kolmogorov interpretation of QH. Traditional ways to understand intuitionistic logic (semantically) have been rooted either in philosophy - with emphasis on the development of knowledge (Brouwer, Heyting, Kripke) or in computer science - with emphasis on effective operations (Kleene, Markov, Martin-Loef). Our "modified BHK interpretation" is rooted in the usual mathematical ideas of canonicity and stability; it emphasizes simply the order of quantifiers, developing Kolmogorov's original approach. This interpretation is compatible with two complete classes models of QH: (i) Tarski topological models and (ii) set-theoretic models of Medvedev-Skvortsov and Laeuchli; as well as with (iii) our sheaf-valued models. |