=Paper=
{{Paper
|id=Vol-1949/ICTCSpaper16
|storemode=property
|title= A Congruence Relation for Restructuring Classical Terms
|pdfUrl=https://ceur-ws.org/Vol-1949/ICTCSpaper16.pdf
|volume=Vol-1949
|authors=Dragisa Zunic,Pierre Lescanne
|dblpUrl=https://dblp.org/rec/conf/ictcs/ZunicL17
}}
== A Congruence Relation for Restructuring Classical Terms==
https://ceur-ws.org/Vol-1949/ICTCSpaper16.pdf
A congruence relation for restructuring
classical terms
Dragiša Žunić1 and Pierre Lescanne2
1
Carnegie Mellon University in Qatar
2
Laboratoire de l’Informatique du Parallélisme, LIP
Ecole Normale Supérieure de Lyon, France
Abstract. We present a congruence relation on sequent-style classical
proofs which identifies proofs up to trivial rule permutation. The study
is performed in the framework of ∗X calculus which provides a Curry-
Howard correspondence for classical logic (with explicit structural rules)
ensuring that proofs can be seen as terms and proof transformation as
computation. Congruence equations provide an explicit account for clas-
sifying proofs (terms) which are syntactically different but essentially
the same. We are able to prove that there is always a representative of a
congruence class which enables computation at the top level.
1 Introduction
For a long time it was considered not possible to give constructive semantics
to classical logic, but only to intuitionistic and linear logic. Recent works have
shown that this is actually possible if one gives up on the principle that the
computational semantics is a confluent rewrite system.
In this work we study the essence of classical proofs by means of specifying its
unessential content. Namely we present a list of congruence rules specifying which
syntactically different proofs/terms should be considered the same. Moreover,
this congruence relation enables us to pick a representative of a congruence class
so that the cut elimination can continue at the top level. This is done in the
framework of ∗X calculus - a higher order rewrite system designed to provide a
Curry-Howard correspondence with the sequent system G1 [13] for classical logic
(presented in Fig. 2). This system is characterized by the presence of structural
rules weakening and contraction and it is very close to the original formulation
by Gentzen [5].
2 Related work
The first computational interpretation of classical logic relying on sequents was
presented by Curien and Herbelin in [4] and in [8], while a direct correspondence
with a standard sequent formulation of classical logic, with the intent of captur-
ing its computational content in full richness (although with implicit structural
rules), was presented by Urban in [14] and by Bierman and Urban in [15]. This
research further lead to the formulation of X calculus [11, 2] which was a base
to introduce explicit control over erasure and duplication by featuring explicit
structural rules weakening and contraction, yielding the ∗X calculus [18, 6]. This
kind of conservative calculus extension had been studied in the intuitionistic
framework by Kesner and Lengrand [9]. Indeed there is a certain analogy in
going from λx [1] (featuring explicit substitution) towards λlxr [9] (explicit sub-
stitution, erasure and duplication) in the natural deduction setting, and going
from X to ∗X in the classical sequent calculus setting.
3 The calculus ∗X
Intuitively when we speak about ∗X -terms we speak about classical proofs for-
malized in the sequent calculus with explicit structural rules weakening and
contraction. Terms are built from names. This concept differs essentially from
the one applied in λ-calculus, where variable is the basic notion. The difference
lies in the fact that a variable can be substituted by an arbitrary term, while
a name can be only renamed (that is, substituted by another name). In our
calculus the renaming is explicit, which means that it is expressed within the
language itself and is not defined in the meta-theory. The notation of using hats
over names has been borrowed from Principia Mathematica [17] and is used to
denote the binding of a name.
Definition 1. The syntax of ∗X -calculus3 is presented in Fig. 1, where x, y, z...
range over an infinite set of in-names and α, β, γ... range over an infinite set of
out-names.
P, Q ::= hx.αi capsule (axiom rule)
b P βb . α
| x exporter (ritht arrow-introduction)
| Pα b [x] yb Q importer (left arrow-introduction)
| Pα b †x bQ cut (cut)
| x P left-eraser (left weakening)
| P α right-eraser (right weakening)
| z < xybbhP ] left-duplicator (left contraction)
α
| [P iβb >γ right-duplicator (right contraction)
b
Fig. 1. The syntax of ∗X
Although we distinguish two categories of names (in-names and out-names)
they will usually be referred to simply as names. There are eight constructors
introduced in the syntax, whose names suggest their computational role.
3
We consider only the implicational fragment here.
Definition 2. We define free names and principal names of a term R, written
f n(R) and pn(R), respectively, in the following way:
R f n(R) pn(R)
hx.αi x, α x, α
xb P βb . α f n(P )\{x, β} ∪ α α
Pα b [x] yb Q f n(P ) ∪ f n(Q)\{α, y} ∪ x x
Pα b †x bQ f n(P ) ∪ f n(Q)\{α, x} none
x P f n(P ) ∪ x x
P α f n(P ) ∪ α α
x< xxc
c
1
2
hP ] f n(P )\{x1 , x2 } ∪ x x
α
[P iαc2 >α
c1
f n(P )\{α1 , α2 } ∪ α α
A name which is not free is called a bound name. The notion of a principal
name describes a free name that appears at the top level in the structure of term.
We will use P α and Qx to emphasize that P and Q have α and x as principal
names, respectively.
Our consideration of principal names is motivated by the nature of cut oper-
ation, which always refers to a pair of free names (an out-name and an in-name)
- one in each corresponding term - and binds them. If these names are at the top
level (accessible) then the cut elimination proceeds in one of its essential steps.
However this research is concerned by static aspects only (dealing with proof
structure), but it most certainly attempts to lay the foundation for revealing the
computational essence as well.
In the ∗X calculus we consider only linear terms. We say that a term is
linear if every name has at most one free occurrence and every binder does bind
an actual occurrence of a name (and therefore only one). We use the standard
definition of linear terms, see [18] on page 43. We will specify the notions of
context, subterm and immediate subterm in order to efficiently work with the
structure of terms.
Definition 3. The contexts are formally defined as follows:
C{ } ::= {} | b { } βb . α
x
| { }α
b [x] yb Q | Pα b [x] yb { }
| { }b
α†x bQ | Pαb †x b{ }
| x {} | {} α
α
| z < xybbh{ }] | [{ }iβb >γ
b
| C{C{ }}
Informally, a context is a term with a hole which can accept another term.
Therefore C{P } denotes placing the term P in the context C{ }.
Definition 4. A term Q is a subterm of a term P , denoted as Q 4 P if there is
a context C{ } such that P = C{Q} (the symbol = stands for syntactic equality.).
It is easy to show that the subterm relation is reflexive, antisymmetric and
transitive (i.e., is an order).
Definition 5. A term Q is an immediate subterm of P if P = C{Q} and
6 C 0 {C 00 { }}, C{ } =
C{ } = 6 { }.
4 The type assignment system
Given a set T of basic types, a type is given by A, B ::= A ∈ T | A → B.
Expressions of the form P : · Γ ` ∆ are used to present the type assignment,
where P is an ∗X term and Γ, ∆ are contexts whose domains consist of free in-
names and out-names of P , respectively4 . Comma in the expression Γ, Γ 0 stands
for the set union.
Definition 6. We say that a term P is typable if there exist contexts Γ and ∆
such that P : · Γ ` ∆ is derivable in the system of rules given by Fig. 3.
Γ ` A, ∆ Γ 0 , B ` ∆0 Γ, A ` B, ∆
(L→) (R→)
0 0
Γ, Γ , A → B ` ∆, ∆ Γ ` A → B, ∆
Γ ` A, ∆ Γ 0 , A ` ∆0
(ax) (cut)
A`A Γ, Γ 0 ` ∆, ∆0
Γ `∆ Γ `∆
(weak-L) (weak-R)
Γ, A ` ∆ Γ ` A, ∆
Γ, A, A ` ∆ Γ ` A, A, ∆
(cont-L) (cont-R)
Γ, A ` ∆ Γ ` A, ∆
Fig. 2. Sequent system G1 for classical logic
Reduction rules are numerous as they capture the richness and complexity
of classical cut elimination, and very fine-grained due to the presence of explicit
terms for erasure and duplication. For details see [18].
5 The congruence relation
This section presents a congruence relation on terms, denoted ≡, which is rep-
resented by a list of equations5 . The congruence relation induced by these rules
4
Technically contexts are sets of pairs (name, formula); if we forget about labels and
consider only type, we are going back to Gentzen’s classical system G1 (Fig. 2),
where contexts are multisets of formulas.
5
The list is partial due to limited space. A complete list of congruence rules can be
found in [18].
(ax)
hx.αi : · x :A ` α :A
P : · Γ ` α :A, ∆ Q : · Γ 0 , y :B ` ∆0 P : · Γ, x :A ` α :B, ∆
(L→) (R→)
0 0
b [x] yb Q : · Γ, Γ , x :A → B ` ∆, ∆
Pα x b . β : · Γ ` β :A → B, ∆
bP α
P : · Γ ` α :A, ∆ Q : · Γ 0 , x :A ` ∆0
(cut)
bQ : · Γ, Γ 0 ` ∆, ∆0
b †x
Pα
P :· Γ ` ∆ P :· Γ ` ∆
(weak-L) (weak-R)
x P : · Γ, x :A ` ∆ P α : · Γ ` α :A, ∆
P : · Γ, x :A, y :A ` ∆ P : · Γ ` α :A, β : A, ∆
(cont-L) α
(cont-R)
z < xybbhP ] : · Γ, z :A ` ∆ [P iβb >γ : · Γ ` γ :A, ∆
b
Fig. 3. The type system for ∗X
is a reflexive, symmetric and transitive relation closed under any context. These
rules define explicitly and in an intuitive way which syntactically different terms
should be considered the same. The key property of this congruence relation is
that, given a cut term, it offers a representative of a congruence class so that
the computation (cut elimination) continues at the top level (see Theorem 1).
The diagrammatic representation is assigned to every congruence rule to
strengthen the reader’s intuition (a formal study of the diagrammatic calculus,
which can be derived from the term calculus presented here, is in the domain of
future work). A label is assigned to every congruence rule, and thus each rule is
declared as: name : P ≡ Q.
exporter-importer
(1) γ y (2) γ y
x P β I Q P I
x
Q β
E E
α z z α
ei1 : xb (P γb [z] yb Q) βb . α ≡ (b
x P βb . α) γ
b [z] yb Q with x, β ∈ f n(P )
.
ei2 : xb (P γb [z] yb Q) β α ≡ P γb [z] yb (b
b x Q βb . α) with x, β ∈ f n(Q)
exporter-cut
(1) γ y (2) γ y
x P β Q P x Q β
E E
α α
ec1 : xb (P γb † ybQ) βb . α ≡ (b
x P βb . α)b
γ † ybQ with x, β ∈ f n(P )
.
ec2 : xb (P γb † ybQ) β α ≡ P γb † yb(b
b x Q βb . α) with x, β ∈ f n(Q)
importer-importer
(1) (2) (3)
t α
R α y Q β t P
β I
P I I
R I y
P α y Q Q β t
R
I I
x
z
x x
z z
ii1 : (P α t R ≡ (P βb [z] b
b [x] yb Q) βb [z] b t R) αb [x] yb Q with α, β ∈ f n(P )
ii2 : (P αb [x] yb Q) β [z] b
b tR ≡ P α b [x] yb (Q βb [z] b
t R) with y, β ∈ f n(Q)
ii3 : (Q βb [z] b
t R) ≡ Q βb [z] b t (P α
b [x] yb R) with y, t ∈ f n(R)
cut-cut
(1) (2) (3)
y α
β
R P α x Q β y
R P x
P α x Q Q β y
R
cc1 : (P α
b †xbQ)βb † ybR ≡ (P βb † ybR)b
α †x bQ with α, β ∈ f n(P )
cc2 : (P α
b †xbQ)βb † ybR ≡ P α
b †x b(Qβb † ybR) with x, β ∈ f n(Q)
cc3 : P α
b †xb(Qβb † ybR) ≡ Qβb † yb(P α
b †xbR) with x, y ∈ f n(R)
cut-importer
(1) (2)
β
z
R P α
I
y Q β z
R
α y
P I
Q
x
x
ci1 : b [x] yb Q)βb † zbR ≡ (P βb † zbR) α
(P α b [x] yb Q with α, β ∈ f n(P )
ci2 : b [x] yb Q)βb † zbR ≡ P α
(P α b [x] yb (Qβb † zbR) with y, β ∈ f n(Q)
(3) (4)
α x β z α
P Q I R P x
β z
Q I
R
y
y
ci3 : P α
b †x
b(Q βb [y] zb R) ≡ (P α
b †x bQ) βb [y] zb R with x, β ∈ f n(Q)
ci4 : P α b(Q βb [y] zb R) ≡ Q βb [y] zb (P α
b †x b †x
bR) with x, z ∈ f n(R)
cut-contraction
(1) (2)
x1 x1
x x
x2 x2
P α y Q P α y Q
cct 1 : x< xxc
c2
b † ybQ] ≡ (x< xxc
1 hP α
c
1 hP ])b
2
α † ybQ with x1 , x2 ∈ f n(P )
x
cct 2 : x< xc2 hP α
c1
b † yb(x< xxc
b † ybQ] ≡ P α c
1
2
hQ]) with x1 , x2 ∈ f n(Q), y 6= x
(3) (4)
α1 α1
α α
α2
P β y Q P β y Q α2
cct 3 : [P βb † ybQiααc1
c2
α
>α ≡ ([P i 1 >α)β
c
α
c2
b † ybQ with α1 , α2 ∈ f n(P ), α 6= β
cct 4 : [P βb † ybQiαc12 >α ≡ P βb † yb([Qiααc
αc
c2 >α)
1
with α1 , α2 ∈ f n(Q)
weak-general
(1) (2)
x C P C P α
wg1 : x (C{P }) ≡ C{x P } x∈
/ f n(C{P })
wg2 : (C{P }) α ≡ C{P α} α∈
/ f n(C{P })
The relation ≡ induces congruence classes on terms. We use cl(P ) to denote the
congruence class of a term P with respect to the relation ≡. Notice that each
congruence class has finitely many terms, and thus finitely many possibilities to
select a representative of a class.
Congruence rules satisfy some standard properties such as preservation of free
names (interface preservation, as in Lafont’s interaction nets [10]) and preserva-
tion of types.
It has been argued in [12] that two sequent proofs induce the same proof net
if and only if one can be obtained from the other by a sequence of transpositions
of independent rules, without giving details about these operations. We proceed
further as we have presented explicitly how this transposition is done at the static
level. This detailed study, presented here in the framework of ∗X calculus, will
enable the search for the essence of computational aspect as well, by considering
reduction as reducing modulo congruence relation.
In what follows we show that the congruence rules allow us to perform restruc-
turing of ∗X -terms (i.e. sequent proofs), so that the cut-names (names bound
by a cut operation) are brought to the top level. Take for example an arbitrary
∗
X -term of the form:
Pαb †x bQ
The name α might not be directly accessible (that is, α is maybe not principal
name for P ). Furthermore, this might hold for both names involved in the cut, α
and x, which are possibly deep inside the structure of their corresponding terms.
We prove that it is possible to transform the above term using congruence rules
defined in the previous section6 - to:
C{P α α bQx }
b †x
where C is a context, and α and x are principal names of P α 4 P and Qx 4 Q,
respectively. In other words we can always pick at least one representative of a
congruence class cl(P αb †xbQ), which allows us to continue the computation at
the top level.
In what follows we first formulate two lemmas which focus on a single cut-
name (either x or α) at a time, followed by the main theorem which addresses
both cut-names. In proving the results we will use the transitivity of 4 relation:
If P 4 Q and Q 4 R then P 4 R.
Lemma 1 (Left-restructuring). For every term of the form P α b †xbQ, there
exists a context C and a term P α , where α is a principal name for P α and
P α 4 P , such that
Pα bQ ≡ C{P α α
b †x b †x
bQ}
Proof. By induction on the structure of P and case analysis.
• The base case is when α is a principal name for P . Then we have P α = P
and C = { }.
• Assume that the property holds for the immediate subterms of P . The pos-
sible cases for P are
1. P = yb M βb . γ, γ 6= α
2. P = M βb [y] zb N
3. P = M βb † ybN
β
P = x< xxc
1
c
4.&5. c
1
2
hM ] and P = [M iβc2 >β, β 6= α
6.&7. P = x M and P = M α, β 6= α
We analyze the first 3 cases7 :
6
For the cases we prove here the set of congruence rules presented is sufficient. Pre-
senting a complete proof would require to use all congruence rules.
7
Due to a limited space.
ec1
y M βb . γ)b
1. (b α†x
bQ ≡ yb (M α bQ) βb . γ
b †x
i.h.
≡ yb (C 0 {M α α bQ}) βb . γ
b †x
α
, C{M α b †xbQ},
with C{ } = yb (C 0 { }) βb . γ
2. (a) Case α ∈ M.
ci1 i.h.
α†x
(M βb [y] zb N )b bQ ≡ (M α bQ) βb [y] zb N ≡ (C 0 {M α α
b †x b †x
bQ}) βb [y] zb N
, C{M α α
b †x
bQ}, with C{ } = (C 0 { }) βb [y] zb N
(b) Case α ∈ N.
ci2 i.h.
α†x
(M βb [y] zb N )b bQ ≡ (M α bQ) βb [y] zb N ≡ (C 0 {M α α
b †x b †x
bQ}) βb [y] zb N
, C{M α α
b †x
bQ}, with C{ } = M βb [y] zb (C 0 { })
3. (a) Case α ∈ M.
cc1
(M βb † ybN )b
α†x
bQ ≡ (M α
b †x
bQ)βb † ybN
i.h.
≡ (C 0 {M α α
b †x
bQ})βb † ybN
α
, C{M α b †xbQ},
with C{ } = (C 0 { })βb † ybN
(b) Case α ∈ N.
cc2
(M βb † ybN )b
α†x
bQ ≡ M βb † yb(N α
b †x
bQ)
i.h.
≡ M βb † yb(C 0 {N α α
b †x
bQ})
, C{N α αb †x bQ},
with C{ } = M βb † yb(C 0 { })
The proof goes similarly for other cases.
Lemma 2 (Right-restructuring). For every term of the form P α b†xbQ, there
exists a context C and a term Qx , whose principal name is x and Qx 4 Q, such
that
b †x
Pα bQ ≡ C{P α b †x bQx }
Proof. Similarly as previous lemma, by induction on the structure of Q and case
analysis.
The following theorem confirms that the top level cut evaluation is complete,
in a sense that there always exists a representative of a congruence class which
enables cut evaluation at the top level relative to its cut-names.
It also shows that in the presence of congruence rules we do not need prop-
agation rules. Propagation rules in the ∗X calculus can be seen as means to
perform restructuring of terms. However their existence blurs the core part of
classical computation, and at the same time don’t enable restructuring of normal
forms (terms that do not contain cuts).
b†x
Theorem 1. For every term of the form P α bQ there exists a context C and
terms P α and Qx whose principal names are α, x respectively, and P α 4 P ,
Qx 4 Q, such that
bQ ≡ C{P α α
b †x
Pα bQx }
b †x
Proof. By using the two previous lemmas, we construct the proof as follows:
Lem. 1
b †x
Pα bQ ≡ C1 {P α α
b †x
bQ}
Lem. 2
≡ C1 {C2 {P α α bQx }}
b †x
, C 0 {P α α bQx },
b †x with C 0 { } = C1 {C2 { }}
And thus we are done.
6 Basic properties of ≡
The congruence relation describes the way to perform restructuring of terms
and thus an important property is preservation of free names. Second important
property is type preservation, which ensures that term-restructuring defined by
≡ can be seen as proof-transformation.
Theorem 2 (Free names preservation). If P, Q are ∗X -terms, then the fol-
lowing holds: If P ≡ Q then f n(P ) = f n(Q)
Proof. The property can be checked by treating carefully each rule.
Theorem 3 (Type preservation). Let S be an ∗X -term and Γ, ∆ contexts.
Then the following holds: If S : · Γ ` ∆ and S ≡ S 0 , then S 0 : · Γ ` ∆
Proof. The proof goes by checking that the property holds for equations induc-
ing ≡. We first write the typing derivation for the term on the left-hand side,
and then for the term on the right-hand side of the equation. We prove several
non-trivial cases.
• Observe the first rule of exporter-importer group of rules:
ei1
x b [z] yb Q) βb . α ≡ (b
b (P γ x P βb . α) γ
b [z] yb Q, with x, β ∈ f n(P ), x 6= z. On
the one hand we have:
P : · Γ, x : A ` β : B, γ : C, ∆ Q : · Γ 0 , y : D ` ∆0
(→ L)
Pγ
b [z] yb Q : · Γ, Γ 0 , x : A, z : C → D ` β : B, ∆, ∆0
(→ R)
0 0
x b [z] yb Q) βb . α
b (P γ : · Γ, Γ , z : C → D ` α : A → B, ∆, ∆
On the other hand,
P : · Γ, x : A ` β : B, γ : C, ∆
(→ R)
b P βb . α
x : · Γ ` α : A → B, γ : C, ∆ Q : · Γ 0 , y : D ` ∆0
(→ L)
x P βb . α) γ
(b b [z] yb Q : · Γ, Γ 0 , z : C → D ` α : A → B, ∆, ∆0
The proof goes similarly for the other cases.
7 Conclusion and future work
We presented a detailed account of a possible step forward, towards the unveiling
of the essential content of sequent classical proofs. This is done by declaring
which syntactically different terms should be considered the same, i.e., by means
of congruence rules which induce a congruence relation on terms.
The framework for this is classical logic formalized in a standard sequent
system with explicit structural rules, namely weakening and contraction. Indeed
it was necessary to have all the details, structural as well as logical, to be able
to state what are the unessential aspects and thus extract the essence in a
systematic way.
Clearly this is a base for studying the operational semantics towards defining
a system with only the essential reduction rules, where reducing is reducing mod-
ulo congruence relation. The congruence relation is proved to satisfy the minimal
requirement of free names preservation, as well as that of type preservation.
It is also possible to define a translation, call it D, from terms to diagrams
in a natural way, inductively on the structure of terms (basic study is given
in [18]). A similar approach was taken in [9], when interpreting intuitionistic
λlxr-terms (featuring explicit weakening and contraction) into proof-nets [7]. It
is reasonable to expect the translation D to satisfy
– P1 ≡ P2 then D(P1 ) = D(P2 )
D D
– P1 → P2 then D(P1 ) → D(P2 )
D
where P1 and P2 are ∗X -terms, and where → is a suitable reduction relation on
diagrams. However this should be carefully studied and belongs in the domain
of future work.
Moreover, in terms of future work, this computational model may be relevant
in relation to process session types and concurrency, as recent studies have shown
that both linear intuitionistic [3] and linear classical logic [16], have a natural
interpretation as protocols for concurrent process communication.
Acknowledgments
This paper was made possible by NPRP 7-988-1-178 from the Qatar National
Research Fund (a member of Qatar Foundation). The statements made herein
are solely the responsibility of the authors.
References
1. Barbanera, F., Berardi, S.: A Symmetric Lambda Calculus for ”Classical” Program
Extraction, TACS, pp. 495-515, 1994.
2. van Bakel, S., Lengrand, S. and Lescanne, P.: The language X : circuits, computa-
tion and Classical Logic, Proc. 9th Italian Conf. on Theoretical Computer Science,
vol. 3701, pp. 81-96, 2005.
3. Caires, L., Pfenning, F.: Session Types as Intuitionistic Linear Propositions, CON-
COUR 2010, Lecture Notes in Computer Science, 6269 (2010), pp. 222–236.
4. Curien P.-L., Herbelin, H.: The duality of computation. In: Proc. 5 th ACM SIG-
PLAN Int. Conf. on Functional Programming (ICFP’00). ACM, 2000, pp. 233–243.
5. Gentzen, G., Untersuchungen über das logische Schließen. Math. 39, (1935) 176–
210.
6. Ghilezan, S., Lescanne, P, and Žunić, D.: Computational interpretation of classical
logic with explicit structural rules, draft.
7. Girard, J.-Y.: A new constructive logic: classical logic, Mathematical Structures in
Computer Science, 1-3 (1991), pp. 255–296.
8. Herbelin, H.: C’est maintenant qu’on calcule, au cœur de la dualité, Université
Paris XI ( Habilitation à diriger les recherches), 2005.
9. Kesner, D., Lengrand, S.: Resource operators for lambda-calculus, Information and
Computation, vol. 205, pp. 419-473, 2007.
10. Lafont, Y.: Interaction nets. Proceedings of the 17th ACM symposium on Principles
of programming languages, POPL, ACM Press, pp. 99–108, 1990.
11. Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the clas-
sical sequent calculus, Electronic Notes in Theoretical Computer Science, 86-4
(2003), pp. 714–730.
12. Robinson, E.: Proof Nets for Classical Logic, Journal of Logic and Computation,
13-5 (2003), pp. 777–797.
13. Troelstra, A. S., Schwichtenberg, H.: Basic Proof Theory, Cambridge University
Press, 1996.
14. Urban, C.: Classical Logic and Computation, University of Cambridge (Ph.D. the-
sis), 2000.
15. Urban, C., Bierman, G. M.: Strong normalisation of cut-elimination in classical
logic. Fundamenta Informaticae 45 (1-2) (2001), 123–155, (appeared also at TLCA
in 1999).
16. Wadler, P.: Propositions as Sessions, Proceedings of the 17th ACM SIGPLAN
international conference on Functional programming, ACM SIGPLAN Notices,
47-9 (2012), pp. 273–286.
17. Whitehead, A. N., Russell, B.: Principia Mathematica 2nd Ed., Cambridge Uni-
versity Press, 1925.
18. Žunić, D.: Computing With Sequent and Diagrams in Classical Logic - Calculi
*X , c X and dX , Ph.D. thesis, ENS Lyon, France, 2007. URL: https://tel.
archives-ouvertes.fr/tel-00265549