ABSTRACT. In 1940 Church introduced a system of higher-order logic formulated as a simply typed lambda-calculus with base types i for individuals and o for propositions. In this system logical connectives and quantifiers appear as constants. One of the attractions of this system is the fact that it is on the one hand rather expressive, allowing the formalization of large parts of mathematics, and on the other hand very simple and convenient to handle formally. A variant of Church's theory is the logical basis for the system Isabelle/HOL and it also plays a role in the development of Martin-Loef Type Theory and the latest developments in Homotopy Type Theory

Church's theory was originally formulated with classical logic and a choice operator. If one uses intuitionistic logic instead, drops choice and adds monotone (co)inductive definitions, on obtains a system that, though impredicative, has a clear computational meaning. One can make this precise by a realizability interpretation combined with a theorem for witness-extraction. I will present this system, demonstrate its usefulness by means of examples and discuss its status from a constructive respectively classical point of view.

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.

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.

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.