previous day
all days

View: session overviewtalk overviewside by side with other conferences

09:15-10:15 Session 88G: Invited Talk by Ulrich Berger (joint work with Tie Hou): Program Extraction in Church's Simple Theory of Types
Location: FH, CAD 1
Program extraction in Church's simple theory of types (invited talk)
SPEAKER: unknown

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.

10:15-10:45Coffee Break
10:45-12:15 Session 90AX: Contributed Talks: Extracting Parsers and Ancestral Logic
Location: FH, CAD 1
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.

Intuitionistic Ancestral Logic
SPEAKER: Liron Cohen
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.
13:00-14:30Lunch Break
14:30-16:00 Session 96AX: Contributed Talks: Proof Search and Proof Relevance
Location: FH, CAD 1
Proof-search in natural deduction calculi for IPL

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.

A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic

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.

16:00-16:30Coffee Break