PSC 2014 ABSTRACTS: PAPERS WITH ABSTRACTS

ABSTRACT. Recently, Abel and others have proposed a type system, in which coinductive types are programmed by means of observations. We investigate category theoretical and topological properties of an observational equivalence on terms, which arises naturally in this type system. Moreover, we introduce a proof system, allowing us to verify proofs of observational equivalence.

ABSTRACT. We report here on current work towards an effective proof (with explicit bounds) of Podelski and Rybalchenko Termination Theorem [1]. Our long-term project is to obtain a priori-bounds for the termination of computer programs, and compare these with bounds obtained via other intuitionistic proofs of the Termination Theorem.

References

1. Andreas Podelski and Andrey Rybalchenko. Transition invariants. In LICS, pages 32-41, 2004.

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. In the PDF file.

ABSTRACT. We present a unifying categorical approach, based on Joyal’s completeness theorem, that proves constructive completeness theorems for classical and intuitionistic first order logic, as well as for the coherent fragment. We show that the notion of exploding structure introduced by Veldman in 1976 is adequate for certain fragments of first-order logic, and that Veldman’s modified Kripke semantics arises, as a consequence, as the semantics of a suitable sheaf topos. The proof, as that of Veldman’s, makes essential use of the Fan theorem, since we show that these completeness theorems are in fact equivalent to it. This raises the question of how far one can get in proving completeness constructively but without using the Fan theorem. We prove that the disjunction-free fragment is constructively complete without appealing to it, and also without placing restrictions on the decidability of the theories and the size of the language, while the latter is a fundamental constraint in the general case when working in intuitionistic set theory. Along the way, we show that the completeness of Kripke semantics for the disjunction free fragment is equivalent, over intuitionistic Zermelo-Fraenkel set theory, to the Law of Excluded Middle.

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. We define a simply typed lambda calculus with positive recursive types in which we study the less well-known Scott encoding of data types. Scott data types have "case distinction" as a basic feature. We shed a different light on the Scott data types, by viewing the different cases as "continuations". As Scott data types do not have iteration (or recursion) built in, we add as primitives a "call-by-name iterator" and a "call-by-value iterator" with appropriate reduction rules. We show that the calculus is strongly normalizing.

ABSTRACT. We give a short computational proof derived from Henkin's proof of Gödel’s completeness theorem.

ABSTRACT. \documentclass{llncs}

\title{A joint logic of problems and propositions, a modified BHK-interpretation and proof-relevant topological models of intuitionistic logic} \author{Sergey A. Melikhov} \institute{Steklov Mathematical Institute (Moscow)}

\usepackage{amscd,amsmath,amssymb,verbatim} \usepackage{stmaryrd} \usepackage{cmll}

\begin{document}

\maketitle

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: \begin{itemize} \item The only new connectives $\wn$ and $\oc$ of QHC induce a Galois connection (i.e., a pair of adjoint functors) between the Lindenbaum algebras of QH and QC, regarded as posets.

\item Kolmogorov's double negation translation of propositions into problems extends to a retraction of QHC onto QH.

\item G\"odel's provability translation of problems into modal propositions extends to a retraction of QHC onto its QC+($\wn\oc$) fragment, which can be identified with the modal logic QS4. \end{itemize}

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 {\it 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-L\"of). 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 L\"auchli; as well as with (iii) our sheaf-valued models.

\end{document}

ABSTRACT. We introduce the explicit counterparts and prove realization theorem for bimodal logics, describing communication of two agents in case when knowledge (belief) of both agents is described by one of the logics $\mathsf{K}$, $\mathsf{T}$ or $\mathsf{K4}$. The agents may interact by either adopting or verifying each others knowledge; interaction can be either one-way or two-ways.