# Vivek Nigam’s PhD Thesis [pdf] [presentation]

**Exploiting non-canonicity in the sequent calculus**

*Thesis Advisor:* Dale Miller

Prepared at LIX, Ecole Polytechnique, PARSIFAL team.

Public defense at 14:30 on 18 September 2009.

Location: Amphi Lagarrigue – Ecole Polytechnique, Palaiseau, France

Instructions on how to reach Ecole Polytechnique can be found here.

You can find here a video where I am declared *Docteur*.

**Jury**

Jean-Marc Andreoli - Reviewer

Iliano Cervesato

Roy Dyckhoff - Reviewer

Ian Mackie

Damiano Mazza

Dale Miller - Advisor

Elaine Pimentel

## Abstract

Although logic and proof theory have been successfully used
as a framework for the specification of computation systems, there is
still an important gap between the systems that logic can capture and
the systems used in practice. This thesis attempts to reduce this gap
by exploiting, in the context of the computation-as-proof-search paradigm, two non-canonical aspects
of sequent calculus, namely the *polarity assignment in focused proofs* and
the *linear logic exponentials*. We exploit these aspects in three
different domains of computer science: tabled deduction, logical
frameworks, and algorithmic specifications.

This thesis provides a proof theoretic explanation for tabled
deduction by exploiting the fact that in intuitionistic logic atoms can
be assigned arbitrary polarity. A table is a partially ordered set of formulas and is incorporated into a proof
via multicut derivations. Here, we consider two cases: the first case is when tables contain only *finite successes* and the second
case is when tables may also contain *finite failures*. We propose a focused proof system for each one of these cases and show that, in some
subsets of logic, the only proofs and open derivations available in these systems are those that do not attempt to
reprove tabled formulas. We illustrate these results with some examples, such as simulation, winning strategies, and let polymorphism
typechecking.

We show that linear logic can be used as a
general framework for encoding proof systems for minimal,
intuitionistic, and classical logics. First, we demonstrate
that with a *single* linear logic theory, one can
faithfully account for natural deduction (normal and non-normal),
sequent calculus (with and without cut), natural
deduction with general elimination rules, free
deduction and tableaux proof systems by using logical
equivalences and different polarity assignments to meta-level literals.
Then we exploit the fact that linear logic exponentials are not
canonical and propose linear logic theories that faithfully encode
different proof systems; for example, a multi-conclusion system
for intuitionistic logic and several focusing proof
systems.

The last contribution of this thesis investigates what type of
algorithms can be expressed by using linear logic’s non-canonical
exponentials. In
particular, we use different exponentials to “locate” multisets of
data, and then we show that focused proof search can be precisely
linked to a simple algorithmic specification language that contains
while-loops, conditionals, and insertion into and deletion from
multisets. Finally, we illustrate this result with several graph
algorithms, such as *Dijkstra’s algorithm* for finding
the shortest distances in a positively weighted graph and an algorithm
for checking if a graph is bipartite.

**Lambda-Prolog Codes**

Let-polymorphism typechecking – Example 3.38: [sig] [mod]

Bag Examples – Chapter 7: [sig] [mod]