to filter out duplicates and identify interactive and concrete execution (the latter
being able to exactly simulate abstract execution);

* links with logic programming have not been properly defined although briefly discussed in Section 53. Execution is related to the resolution operator and stellar resolution is related to the semantics of logic programs (which attracted a lot of hype in the 90s). No formal links have been established. Interestingly, there are works of Wolfgang Bibel<fnref n="6" /> such as the “connection method” [Bib13] which has been related to proof-structures with Bertram Fronhöfer’s paper in honour of Wolfgang Bibel [Fro00]. There may also be things to say about constraint programming (stellar resolution is a system of constraints) and Andrew’s refutation by matings [And76];

* there is not yet any alternative definition for λ-calculus with stellar resolution. When I talked about transcendental syntax with Lionel Vaux, he told me that it would be interesting to have a definition of untyped λ-calculus without going through an encoding using proof-structures. I tried to encode the Krivine Abstract Machine in Section 57 but I did not prove that the encoding is faithful and correctly simulate it. When I tried, I was under the impression that it was possible to define λ-calculus directly by encoding its term graph and using the mechanisms of stellar resolution (variable and constants) to simulate explicit substitutions;

* there is no computationally faithful definition of circuits in stellar resolution (cf. Section 58). Circuits (for instance boolean circuits) compute from inputs to outputs. In particular, the result of a gate can only be computed when its two inputs are defined. However, nothing specify this synchronised flow of computation in constellations. I thought of something like associating elements of an ordered set to rays but it was not a very natural thing to do (moreover, regular constellations become special case of those extended constellations with ordered rays);

* there is no complexity analysis for constellations. Some answers may be found in works on the complexity of logic programs [DEGV01]. The complexity of term unification is already well-documented but the execution of constellations raise new questions of complexity. In particular, the shape of terms in constellations has a direct influence on complexity. There may be formal links between class of shapes and complexity classes;

* there is no termination analysis for constellations. I tried to use works in programming logic [NGSKDS07] to state results but I omitted it since it was not complete nor useful for the results of this thesis. The idea was to use an analysis of dependency graphs to assert whether a constellation is terminating or not. The argument would rely on usual termination proofs of term rewriting theory [BN98, Section 2.3] by looking for size-decreasing cycles, a technique also used in functional programming [LJBA01];

<footnote n="6">⁶Who is explicitly mentioned in several recent articles on deep inference [GG07, Brü04, Gug].</footnote>
* in Section 63, I defined some ideas of “stellar compression” in order to minimise constellations. However, since constellations can be seen as generalised automata, it may be possible to define more advanced simplification techniques and have a notion of “minimal constellation” w.r.t. some behaviour;

* there is a lack of proofs regarding exponentials in stellar resolution and a lack of evidences regarding the ability of stellar resolution to define interesting exotic exponentials (Girard's expansive are only sketched from Girard's original presentation);

* although I tried to explain Girard's notion of truth in Section 79, there is currently no serious purpose for it and there is no technical use case for an “axiom-free” Peano arithmetic. It is mostly interesting for philosophical purposes but may find some applications if one explores the subject;

* the interpretation of predicate calculus has only been roughly sketched in Section 84 and there is still a lot of work to do in order to achieve a full formalisation of it.

§87.3 **Extensions of stellar resolution.** Since the beginning of my thesis, Thomas Seiller and I thought about extending stellar resolution with coefficients (something already present in Seiller's work on interaction graphs and graphings). Personally, I had chemical reactions and Markov chains in mind and even tried to generalise stellar resolution using chemical models (without succeeding). Constellations can be seen as atoms or molecules interacting with each other to produce a reaction. After discussing with Seiller, we remarked that there was two possible distinct extensions:

* putting coefficients on stars. Fusion between stars then applies a monoid multiplication on coefficients. We would then have stars and constellations weighted in some given monoid. It corresponds to a generalisation of Seiller's weights on interaction graphs [Sei12a]. Girard also had similar ideas in his second article on transcendental syntax [Gir16b];

* another idea was to put coefficients on the edges of dependency graphs so that the sum of coefficients related to a ray is equal to 1. The point is that for each ray, there is some probability to connect to another specific ray. This is reminiscent of chemical reactions. In that case, coefficients are associated with pairs of rays.

The two extensions are actually compatible and generalise the stellar resolution defined in this thesis.

§87.4 **A new version of proof-nets.** An idea of Seiller was to use ideas of transcendental syntax to develop a sort of correction of proof-nets which would overcome the known problems of the theory of proof-nets (regarding local and global mechanisms appearing with exponentials and additives). It is true that it is not completely clear what a “good” proof-net should be. I personally do not support this direction since I believe that constellations are the next form of proof-nets and that they *are* what proof-nets
should be (one may say that I am avoiding the problem). Hence, stellar resolution
should define logic by themselves without trying to look for connexions or updates of
the original theory of proof-nets (which may be forgotten).

§87.5 **Parallel and concurrent computation.** Stellar resolution is an asynchronous and parallel model of computation. Parallel computation for term unification is a subject which has been explored quite a lot [HM89, Sib05, Kit91, VS84], probably because of the hype around logic programming in the 90s. An interesting direction is to connect stellar resolution to known works in parallel and concurrent computation. During my thesis, I had two ideas in mind which were left without conclusion:

* with Julien Marquet, we tried to think about an encoding of Lafont's interaction nets and in particular interaction combinators;

* with Félix Castro, we tried to think about an encoding of π-calculus. I wanted stellar resolution to replace process calculi by seeing how it could simulate some of them. However, it was less trivial than expected because of the name handling of π-calculus.

Both these ideas were not worth the time and efforts and I had other priorities so nothing
has been realised so far. There are also subjective rays that I believe to be connected
to synchronised computation and mechanisms of concurrent programming but I was
never able to reach a conclusion (mostly because this consideration came very late in
my thesis).

§87.6 **Generalised token machine.** One well-known application of the geometry of interaction is the token machine or interaction abstract machine (cf. Section 36). Since transcendental syntax extends and generalise the geometry of interaction, it is a natural direction to look for a generalised token machine. There are already such generalised machines in the literature [CC23, DLTY17, CVV21] but no link has been established so far. The idea of a generalised token machine is something which appeared very early in my thesis but which has finally been replaced by concrete and interactive execution (which came way later). The idea of what I called the “stellar machine” is that dependency graphs could be seen as an automaton. We put “tokens” (associated with a family, in order to represent the different diagrams being constructed) which travel through the dependency graph. At each step, a unification problem is solved by adding equations related to the traversed edges. A lot of non-trivial mechanisms have to be considered: non-determinism, colliding tokens/families etc. It seems to me that the treatment of those mechanisms may be similar to what is done in Chardonnet’s works [CVV21].

§87.7 **Verified computation.** Transcendental syntax connects logic with the program testing of computer science. Correctness tests are seen as analysing the shape of constellations in order to assert that they have some computational behaviour. Although it makes sense, I never gave examples of verified computation. One could think of properties on automata or circuits, for instance. Automata would be encoded as constellations but also tests enduring that an automaton is part of some class of automata. Automata themselves
can be seen as finite tests asserting the membership of words in some language. There
might also be connexion with model checking since constellations can be seen as sort of
labelled transition systems.

§87.8 **Discrete complex systems and dynamical systems.** Seiller and I independently remarked that stellar resolution could be seen as a sort of tile system. I discovered Wang tiles at a summer school for young researchers in computer science (EJCIM) and Seiller had already heard about abstract tile assembly models before. At some point, while learning about tile systems, I had the hope of generalising stellar resolution with discrete dynamical systems (I tried to discuss with Benjamin Hellouin but without success) or models of complex system theory. It was very vague but I wanted to know if notions such as chaos and attractors had some sort of logical meaning. I did not have the mathematical background to seriously consider this direction.

§87.9 **Ludics.** This is something which I almost completely omitted in this thesis. Ludics can be seen as a abstraction of sequent calculus whereas geometry of interaction is an abstraction of proof-structures. In an informal with Seiller, we discussed about encoding ludics with stellar resolution so that transcendental syntax would subsumes both ludics and geometry of interaction. An idea was to put an order on constellations to internalise the sequentialisation of logical rules. This may be related to my idea of order and synchronisation for subjective rays. Moreover, I also discussed with Carlos Olarte and he told me that the control of constellations in epidictic (which may also be related to synchronisation/order in computation) reminded him of focalisation which appears in ludics but also in proof-search for linear logic.

§87.10 **Deep inference.** Deep inference [Gug, Brü04, GG07] is a very recent theory of logic which provides an abstraction of sequent calculus which is distinct from both ludics and geometry of interaction. It is an alternative new culture of logic. There is currently no research about how deep inference is different or close to transcendental syntax. After discussing with Pablo Donato and Adrien Ragot about the link between deep inference and transcendental syntax, I was under the (vague) impression that sequent calculi could be seen as recipes for the construction/generation of constellations/programs.

§87.11 **Descriptive complexity.** Connexions between transcendental syntax and computa-
tional complexity is really something I would like to see as I believe complexity problems
are related to logic (once we have a more mature notion of logic – in my opinion logic
is related to the shape of things and their computational potential). There are already
works connecting ideas of geometry of interaction with implicit computational complex-
ity (ICC) [Sei20a, BP99, AS16b] and transcendental syntax may provide results in this
direction. However, I also hope for a new reading of descriptive complexity since types
(either from the Usine or Usage point of view) have a *descriptive function*. They as-
sert some computational potentiality. Can we characterise computational complexity
classes by tests/behaviours? Constellations which can be typed in predicate calculus
and second-order logic (and thus have a specific shape) would theoretically correspond
to programs of complexity class P and NP [Imm12, Imm86].
§87.12 **The nature of programs and algorithms.** There is an article of Gurevich which asks what is an algorithm [Gur12]. Although seemingly innocent, this is a rather profound question. There is currently no satisfying formal definition of algorithm or even of a program. Thomas Seiller already discussed this matter several times in few talks. The subject also led to the ANR project "La géométrie des algorithmes" (GoA) coordinated by Alberto Naibo. Seiller tries to answer the question with his graphings but I believe the question could also be tackled only with stellar resolution which captures classical computation pretty well. As discussed in Section 19, algorithms may be seen as specifications. In our cases, it corresponds a Usine interpretation (since we would like finite checking that the programs is an implementation of some algorithm). Now, what is a *sequential* algorithm? I do not have an answer but I believe that we should have some sort of "sequential formulas" satisfied by sequential programs. Instead of extending the notion of test or program/constellation with ad-hoc external constructions, I rather believe in extending the "shapes" of constellations (plurality of individuals), so that it generalises the stellar resolution of this thesis.

§87.13 **Open proof assistant.** An idea which I find exciting but also vague for the moment. Proof assistants such as Coq relies on one specific system, for instance the calculus of inductive constructions which corresponds to some $\lambda$-calculus. No matter how convenient or inconvenient it is, we are limited to one logic and one model of computation to encode properties and models of computation (automata, circuits, programs etc). Using transcendental syntax, the core is minimal and boils down to the unification algorithm which is well-known and simple. Everything else is constructed within the language itself. In particular, typing, which is essential in proof assistants, is given by tests. A logic generates tests with formula labels (representing properties to be shown). Hence, several logic can coexist. Logical systems become sort of libraries/modules as in programming. Proving is not bound to a specific logic such as intuitionistic logic. Certainty relies on tests known/proven to be adequate (this cannot be directly proven in the system itself). Whether such an "open" proof assistant is good or not is still an open question. One may argue that functional systems are sufficient/convenient for most purposes. Anyway, potential proof assistants based on stellar resolution should not be understood as a potential replacement of other proof assistants but as another type of proof assistant.

§87.14 **Epidictic language as a script language for macros.** The epidictic is what allows stellar resolution to constructs closed systems. Such closed systems makes reasoning more efficient and "axiomatic" but also makes possible quantification (since the world is closed, I can make assumption of the shape of the possible objects on which I quantify). Typically, imagine that you would like to work with $\lambda$-calculus in stellar resolution. It would be too tedious and prone to errors to write the corresponding constellations and tests for each formulas each time. It actually took me a long time to figure out what could be a concrete realisation of Girard's epidictic. It is only late in my thesis that I considered that it could be... a macro system. The primitive system is stellar resolution which is very flexible and everything else is just syntactic sugar with complex macros. For instance, we would have a way to construct formulas as syntactic labels but also
macros to inductively associate formulas with test-constellations.

§87.15 **A realist thesis?**. I am not a philosopher at all and have absolutely no background in philosophy but during my thesis I had the hope that transcendental syntax would raise insights regarding scientific/semantic realism and essentialism in logic. If an “existentialist” approach to logic (as Girard calls it) consists in forgetting all primitive definitions so that types/formulas would be reconstructed from computational individuals, then it looks like transcendental syntax is a bit more than just an existentialist approach to logic. Transcendental syntax adds a Usine interpretation which was not present in lucidics nor geometry of interaction. This interpretation shows that “the primitive shapes of things matters” and in particular that it is possible to anticipate the behaviour of individuals from their shape. I might be mistaking but it seems to me that the shape (of computational objects) becomes a *primitive essence* in this case. However, we know that behaviours cannot always be fully characterised by finite tests, hence this anticipation is indeed limited. There is also the problem of whether mathematical (or logical) entities exist in an external reality, independently of us. It seems to me that computational monist testing is a process of “reality-discovery” producing responses which are then interpreted/formatted by us. Although the medium of interaction (whether it is stellar resolution or something else) is relative/chosen, syntactic interactions occurring in mathematics says things about how reality is structured. This may explain the relevance of mathematics over the “real world” (and in particular the fact that mathematics says things about physics, thus allowing us to construct reliable bridges or reliable programs).

## 88 Limits of the current presentation of transcendental syntax

§88.1 **A too open theory.** Transcendental syntax is like a computational sandbox for logic. It is an alternative point of view on logic (like deep inference). Because it is so free, it also lacks direction. As shown in the previous section, there is a lot of potential applications but it remains to filter out the most interesting and relevant ones. Transcendental syntax is still a very speculative and experimental subject for the moment.

§88.2 **Complexity issues.** Concrete execution which is the implementable version of abstract execution (the more “semantical” or “denotational” way to evaluate constellations) has a horrible complexity. We constantly have to compute graph isomorphism which is known to be a difficult problem. We have no choice but to exclude concrete execution from real-world applications. Only interactive execution (which could be refined into a token machine) is left. Although no complexity results have been stated, it seems that the complexity of constellations representing some computational objects (automata, circuits, ...) is faithful to the original complexity of the model. All additional complexity added with constellations correspond to term unifications. Another problem of complexity related to logic is that the most natural correctness criterion is the Danos-Regnier correctness which is known to have an exponential complexity (there are $2^n$ tests for $n$ par hyperedges). It is currently not known if other more efficient correctness criterion can be
easily and efficiently implemented in stellar resolution. It may be the case that adding
an “epidictic layer” makes computation more efficient (we only look at external opaque
interactions without considering the underlying micro-computational mechanisms – this
is the point of axiomatic theories).

§88.3 **Limitation to classical computation.** The presentation of transcendental syntax in this thesis is obviously limited to classical computation. However, this is not an absolute limitation of transcendental syntax itself. Constellations could be extended with coefficients in order to interpret probabilistic or quantum computation (Chardonnet uses a token machine with complex coefficients). However, it is unsure that doing so would provide an interesting non-classical model of computation (when compared to models which purpose is to be relevant for non-classical computation).

§88.4 **Another blind spot.** As explained by Girard in the end of his third article on transcendental syntax [Gir18b], transcendental syntax still cannot give a “transcendental” status to type judgement appearing in (Martin-Löf) type theory. Moreover, there are also new works such as the so-called Homotopic Type Theory (HTT) with a new treatment of equality. There is also deep inference. Although all these theories speak about logic, they looks distinct from transcendental syntax. For the time being, transcendental syntax is not able to provide comments, analysis nor comparisons. Transcendental syntax, at least in its current form, does not look as universal as some would like it to be.

§88.5 **A materialist conception of logic.** After discussing with Baptiste Chanus and other people about transcendental syntax, Baptiste stated that despite the appearances of transcendental syntax and the hope of some people to see something more fundamental or universal than other conceptions of logic, transcendental syntax was, after all, a computational point of view of logic, hence a logical paradigm among other ones. It is true that transcendental syntax is deeply dependent of some material entities of a computational nature and that it does not take into account the social nature of the logical activity. In transcendental syntax, there is a strong belief that computation explains the whole logical activity. Whether it is right or wrong, this is out of my field of expertise. But if you still want to hear about my current belief, the natural and social aspect of logic may not be incompatible. There is the natural layer of stellar resolution, on which logical constructions can be made then the social/cultural layer correspond to the epidictic which corresponds to systems put over stellar resolution.
# Appendix A

## Mathematical conventions

### A.1 General notations

◇ **Definition (:=) and equality (=)** I write $A := B$ when A is defined as B. It should not be mistaken with the equality $A = B$ saying that A and B are already defined and equal. It is similar to the difference between $=$ (affectation) and $==$ (boolean equality) in some programming languages such as the C language.

◇ **Confer/conferatur (cf.)** Used as reference to another thing (latin). For instance “cf. A” means that we can refer to A in case we want more information.

◇ **Domain of a function** Let $f: A \to B$ a function over sets. We define $\text{dom}(f) := A$, called the *domain* of $f$.

◇ **Exempli gratia (e.g.)** For example (latin).

◇ **Id est (i.e.)** That is (latin).

◇ **Images of a function** Let $f: A \to B$ a function over sets. We define $\text{img}(f) := B$, called the set of *images* of $f$.

◇ **Projections** Let $p = (a_1, ..., a_n)$ be a tuple. We define $\pi_i(p) = a_i$ as the $i$-nth projection of $p$.

◇ **Respectively (resp.)**

◇ **Sequence** By sequence, I mean a tuple $(a_1, ..., a_n)$ but more generally, it is defined as an indexed family indexed by natural numbers (see Appendix A.2 below).

◇ **With respects to (w.r.t.)**
## A.2 Set theory

### Elementary set theory

§A.2.1 **Definition (Cartesian product).** The cartesian product of two sets A and B is defined by $A \times B := \{(a, b) | a \in A, b \in B\}$.

§A.2.2 **Definition (Disjoint sets).** Two sets A and B are disjoint if and only if $A \cap B = \emptyset$.

§A.2.3 **Definition (Disjoint union).** Let A and B be two sets. Their disjoint union is defined by the set $A \uplus B := \{(a, 0) | a \in A\} \cup \{(b, 1) | b \in B\}$.

§A.2.4 **Example.** Let $A = \{a, b, c\}$ and $B = \{c, d\}$. We have

$$A \uplus B = \{(a, 0), (b, 0), (c, 0), (c, 1), (d, 1)\}.$$

Notice that the element $c \in A$ is distinguished from the element $c \in B$ by their associated index $i \in \{0, 1\}$.

When two sets are disjoint, we can omit the indexes 0 and 1 in their disjoint union since there is no ambiguity.

§A.2.5 **Definition (Powerset).** The powerset of a set S is defined by $P(S) := \{S' | S' \subseteq S\}$.

§A.2.6 **Definition (Function application on sets).** Let $f : S \to S'$ be a function over two sets S and S'. If $S = \{a_1, ..., a_n\}$ then the application of f on S is defined by $f(S) = \{f(a_1), ..., f(a_n)\}$.

§A.2.7 **Definition (Predicate associated to a set).** Let $P(x_1, ..., x_n)$ be a predicate with variables $x_1, ..., x_n$.

§A.2.8 **Definition (Generalised union).** We define a generalised iterative union by

$$\bigcup_{i=n}^{n} := \emptyset \qquad \bigcup_{i=k}^{n} E_i := E_k \cup \bigcup_{i=k+1}^{n} E_i \quad \text{when } (k < n)$$

for sets $E_k, ..., E_n$, a counter $i$ starting with $i = k$ and stopping at $i = n$.

We also define the alternative notations: $\bigcup_{k \le i \le n} E_i := \bigcup_{i=k}^{n} E_i$.

Let $P(x, S)$ be a predicate over a variable $x$ and a set $S$ ($x \in S$ and $S' \subseteq S$ are such predicates), and $E$ an expression denoting a set where the variable $x$ occurs. We define the following expression of generalised union over a predicate $P(x, S)$ on $E$:

$$\bigcup_{P(x, \emptyset)} E := \emptyset \qquad \bigcup_{P(x, \{e\} \cup S)} E := \{x := e\} E \cup \bigcup_{P(x, S)} E$$
We define the following notation for repeated generalised unions:

$$ \bigcup_{B_1, \dots, B_n}^{A} E := \bigcup_{B_1}^{A} \dots \bigcup_{B_n}^{A} E $$

## Multisets

A multiset is a set in which a same element can appear several times. It is defined by a set and a map relating each elements of the set to its number of occurrence (called multiplicity).

§A.2.9 **Definition (Multiset).** A multiset is a pair $(S, \text{nbOcc})$ of a set $S$ and a total function $\text{nbOcc} : S \to \mathbb{N}$.

We use the notation $[a_1, \dots, a_n]$ for finite multisets in which repetitions explicitly appear.

§A.2.10 **Example.** Let $S := \{a, b, c\}$. We can define the multiset $(S, \text{nbOcc})$ such that $\text{nbOcc}(a) = 1$, $\text{nbOcc}(b) = 2$ and $\text{nbOcc}(c) = 3$. This multiset can be written $[a, b, b, c, c, c]$.

§A.2.11 **Definition (Multiset induced by a set).** Let $S$ be a set. It induces a multiset $\text{multiset}(S) := (S, \text{nbOcc})$ with $\text{nbOcc}(e) = 1$ for all $e \in S$.

§A.2.12 **Definition (Multiset union).** Let $(A, \text{nbOcc}_A)$ and $(B, \text{nbOcc}_B)$ be two multisets. Their union $A \cup B$ is defined by the multiset $(A \cup B, \text{nbOcc}_{A \cup B})$ such that

$$ \text{nbOcc}_{A \cup B}(e) = \text{nbOcc}_A(e) + \text{nbOcc}_B(e). $$

§A.2.13 **Example.** If we have two multisets $A = [a, b, b]$ and $B = [b, b]$, then their union is $(\{a, b\}, \text{nbOcc}_{A \cup B})$ with $\text{nbOcc}_{A \cup B}(a) = 1$ and $\text{nbOcc}_{A \cup B}(b) = 4$. The union can be written $[a, b, b, b, b]$.

## Indexed families

Indexed families is an alternative definition for ordered multisets which I find more convenient. Instead of associating elements to a multiplicity, we start from a set of indexes and associate an element to each index.

§A.2.14 **Definition (Indexed family).** An indexed family over $I$ is given by a tuple $(S, I, \text{get})$ of a set $S$, a set of indexes $I$ and an index function $\text{get} : I \to S$.

Indexed families with natural numbers as set of indexes correspond to sequences in mathematics and to arrays in programming.
§A.2.15 **Example.** We define an indexed family $(S, I, \text{get})$ with $S = \{a, b\}$, $N = \{0, 1, 2, 3\}$ and $\text{get}(0) = a$, $\text{get}(1) = a$, $\text{get}(2) = b$, $\text{get}(3) = a$. It corresponds to the array $\begin{bmatrix} 0 & 1 & 2 & 3 \\ a & a & b & a \end{bmatrix}$ where positions are given on the top with the corresponding integer index and the associated element on the bottom.

§A.2.16 **Notation.** Let $\varphi = (S, I, \text{get})$ be an indexed family. To make the notation closer to arrays in programming, we define the notation $\varphi[i] := \text{get}(i)$ for $i \in I$.

§A.2.17 **Definition** (Disjoint union of indexed families). Let $\varphi_1 = (S_1, I_1, \text{get}_1)$ and $\varphi_2 = (S_2, I_2, \text{get}_2)$ be two indexed families. Their disjoint union $\varphi_1 \uplus \varphi_2$ is the indexed family $(S_1 \uplus S_2, I_{\varphi_1} \uplus I_{\varphi_2}, \text{get}_1 \uplus \text{get}_2)$ with $\text{get}_1 \uplus \text{get}_2 : I_{\varphi_1} \uplus I_{\varphi_2} \to S_1 \uplus S_2$ defined by $(\text{get}_1 \uplus \text{get}_2)(i) = \text{get}_k(i)$ when $i \in I_{\varphi_k}$ and $k \in \{1, 2\}$.

## A.3 Language theory

§A.3.1 **Definition** (Alphabet and word). An *alphabet* is a set of elements called *symbols*. A *word* over an alphabet $\Sigma$ is an ordered sequence of symbols of $\Sigma$.

There is a distinguished symbol $\varepsilon$ called *empty symbol*.

We often omit parentheses when writing words, i.e. we write *abc* instead of $(a, b, c)$.

§A.3.2 **Example.** If $\Sigma = \{a, b, c\}$ then $a, aaaaa, acccb, aaabab$ are words over $\Sigma$.

§A.3.3 **Definition.** The *concatenation* of words is defined as follows:

* $\varepsilon \cdot w := w$ and $w \cdot \varepsilon := w$;

* $(a_1, ..., a_n) \cdot (b_1, ..., b_m) := (a_1, ..., a_n, b_1, ..., b_m)$.

§A.3.4 **Definition** (Kleene closure). Let $\Sigma$ be an alphabet, its *Kleene closure* written $\Sigma^*$ is the set satisfying the following requirements:

* $\varepsilon \in \Sigma^*$

* if $c \in \Sigma$, then $c \in \Sigma^*$;

* if $w \in \Sigma^*$ and $w' \in \Sigma^*$ then $w \cdot w' \in \Sigma^*$;

§A.3.5 **Example.** If $\Sigma = \{a, b, c\}$ then $\{\varepsilon, a, b, c, aa, bb, cc, aaa, bbb, ccc, aba, abc, bac\} \subset \Sigma^*$.

§A.3.6 **Definition** (Notation). Let $a_1, ..., a_n$ be symbols of some alphabet $\Sigma$. The set of notations over the notation generators $a_1, ..., a_n$ is the set $N$ satisfying the following requirements:

* $\{a_1, ..., a_n\} \subset N$;
• if $a \in N$ and $x \in N$ then $a' \in N$, $a_x \in N$ and $a^x \in N$.

§A.3.7 **Example.** The set of notations over $\{a\}$ contains $a, a', a'', a'''$, $a_1, a_2, a_3, a^1, a^2$ and $a^3$.

§A.3.8 **Definition** (Backus-Naur Form grammars). The expression

$$A_1, \dots, A_n ::= \quad B_1 | \dots | B_m \quad \text{set } C \quad \text{(D)}$$

corresponds to a notation for Backus-Naur Form (BNF) grammars. It says that the category or type called *D*, denoted by the set *C*, has elements represented by symbols $A_1, \dots, A_n$ and constructed from one of the expressions in $B_1, \dots, B_n$ (the vertical bar | is then a disjunction of cases). The denotation *D* can be omitted.

We consider that all symbols of the set of notations over $\{A_1, \dots, A_n\}$ can be used to represent elements of the set *C*.

It happens that some $A_i$ occurs in some $B_i$ and in this case, we have an *inductive type*.

§A.3.9 **Example.** Some typical examples are booleans, natural numbers, lists (parametrised by another type for elements) and trees (parametrised by another type for the content of nodes):

```
a, b, c ::= 0 | 1                      set Bool             (Booleans)
n, m, k, l ::= 0 | s(n)                   set Nat              (Natural numbers)
l ::= [] | e :: l with e ∈ A           set List[A]          (Lists)
t, t₁, t₂ ::= ∅ | (t₁, e, t₂) with e ∈ A  set Tree[A]           (Trees)
```
# Appendix B

## Term unification

§B.0.1 Terms are used to represent statements. In this section, we are interested in solving equations $t \stackrel{?}{=} u$ between terms by searching for a way to replace variables by other terms in order to make $t$ and $u$ equal. Equations between terms are usually attributed to Robinson [R+65] but Herbrand [Her30] already studied term unification before in the context of his investigations on mathematical equations and proof theory.

§B.0.2 We refer the reader to the article of Lassez et al. [LMM88] for more details which are often omitted in the literature or Baader et al. [BN98] for a broader view.

### B.1 Elementary definitions

§B.1.1 In this appendix I use a generalisation of term unification which is in not standard. In my definition of unification, I consider a binary relation $\prec$ over function symbols which tells us when two symbols are compatible. This will allows us to be more general when considering equations between terms.

§B.1.2 **Definition (Signature).** A signature $\mathcal{S} = (V, F, \mathbf{ar}, \prec)$ consists of a countable set $V$ of variables, a countable set $F$ of function symbols whose arities are given by $\mathbf{ar} : F \to \mathbf{N}$ and a binary relation $\prec: F \times F$.

§B.1.3 **Convention.** In usual term unification theory and this appendix, we consider that $f \prec g$ if and only if $f = g$.

§B.1.4 **Definition (First-order terms).** The set of (first-order) terms $\mathbf{Term}(\mathcal{S})$ over a signature $\mathcal{S} = (V, F, \mathbf{ar}, \prec)$ is inductively defined by the following grammar:

$$ a, b, c, d, t, u, v, w ::= \left| \begin{array}{l} X \\ f(t_1, \dots, t_n) \end{array} \right. \quad \text{for } X \in V, f \in F, \mathbf{ar}(f) = n \quad \text{set } \mathbf{Term}(\mathcal{S}) \quad \text{(Terms)} $$
§B.1.5 **Definition** (Set of variables). The set of variables of a term is defined inductively as follows:

$$ vars(X) = \{X\} (\text{for } X \in V) \qquad vars(f(t_1, ..., t_n)) = \bigcup_{1 \le i \le n} vars(t_i) $$

§B.1.6 **Example.** Let $\mathbb{S} := (V, F, \mathbf{ar}, \prec)$ be a signature such that $V = \{X, Y\}$, $F = \{c, f, g\}$ and $\mathbf{ar}(c) = 0$, $\mathbf{ar}(f) = 1$, $\mathbf{ar}(g) = 2$. We can construct the following terms (among others): $c, X, Y, Z, f(c), f(X), g(c, c), g(X, Y), f(g(c, c)), g(f(X), f(f(Y)))$.

§B.1.7 **Definition** (Substitution). A *substitution* is a function $\theta : V \to \text{Term}(\mathbb{S})$. Substitutions are extended from variables to terms by

$$ \theta(f(u_1, ..., u_k)) = f(\theta(u_1), ..., \theta(u_k)). $$

The application $\theta(t)$ of a substitution $\theta$ on a term $t$ can also be written $\theta t$. Substitutions will sometimes we explicitly written with a list of associations $\{X_1 \mapsto t_1, ..., X_n \mapsto t_n\}$ and sometimes simply $\{X := t\}$ if there is only one association.

A renaming is a substitution $\alpha$ such that $\alpha(X) \in V$ for all $X \in V$ and such that it is bijective. In particular, renamings are invertible and the inverse of a renaming $\alpha$ is written $\alpha^{-1}$.

From two substitutions $\theta_1, \theta_2$, we can construct their composition $\theta_1 \circ \theta_2$ such that $(\theta_1 \circ \theta_2)t = \theta_1(\theta_2(t))$. The composition is associative [LMM88, Corollary 6]. It is then possible to write $\theta_1\theta_2\theta_3$ for either $(\theta_1 \circ \theta_2) \circ \theta_3$ or $\theta_1 \circ (\theta_2 \circ \theta_3)$.

§B.1.8 **Example.** Let $\theta := \{X \mapsto c, Y \mapsto c\}$ and $\psi := \{X \mapsto f(Y), Y \mapsto g(c, c)\}$. We have $\theta f(X) = f(\theta X) = f(c)$, $\psi g(X, Y) = g(\psi X, \psi Y) = g(f(Y), g(c, c))$ (substitutions replace simultaneously and not sequentially, hence there is no clash between the two occurrences of $Y$) and $(\theta \circ \psi)g(X, Y) = g((\theta \circ \psi)X, (\theta \circ \psi)Y) = g((\theta \circ \psi)X, (\theta \circ \psi)Y) = g(\theta f(Y), \theta g(c, c)) = g(f(c), g(c, c))$.

§B.1.9 **Definition** (Equation and unification problem). An *equation* is an unordered pair $t \stackrel{?}{=} u$ of terms in $\text{Term}(\mathbb{S})$.

A *unification problem* or simply *problem* is a set of equations $\{t_1 \stackrel{?}{=} u_1, ..., t_n \stackrel{?}{=} u_n\}$.

A *solution* or *unifier* for a problem $P$ is a substitution $\theta$ such that for all $t \stackrel{?}{=} u \in P$, $\theta t = \theta u$. In this case, we say that the terms $t$ and $u$ are *unifiable* and that $\theta$.

§B.1.10 **Example.** The problem $\{f(X, f(Y)) \stackrel{?}{=} f(g(c, c), Z)\}$ has for solution $\theta := \{X \mapsto g(c, c), Z \mapsto f(Y)\}$. The problems $\{f(X) \stackrel{?}{=} g(c, c)\}$ and $\{X \stackrel{?}{=} f(X)\}$ have no solution.
§B.1.11 **Definition (Alpha-equivalence).** Two terms $t$ and $u$ are $\alpha$-equivalent, written $t \approx_{\alpha} u$, if there exists a renaming $\alpha$ such that $t = \alpha(u)$.

§B.1.12 **Definition (Alpha-unification).** An $\alpha$-unifier for a problem $P = \{t_i \stackrel{?}{=} u_i\}_{1\le i\le n}$ is a pair $(\theta, \alpha)$ of a substitution $\theta$ and a renaming $\alpha$ such that $\theta$ is a solution for $\{t_i \stackrel{?}{=} \alpha u_i\}_{1\le i\le n}$. Two terms $t$ and $u$ are $\alpha$-unifiable if there exists an $\alpha$-unifier for $\{t \stackrel{?}{=} u\}$.

§B.1.13 **Example.** A typical example is the problem $\{X \stackrel{?}{=} f(X)\}$ which has no unifier but has an $\alpha$-unifier. A possible $\alpha$-unifier is $(\theta, \alpha)$ with $\theta := \{X \mapsto f(c), X' \mapsto c\}$ and $\alpha := \{X \mapsto X'\}$. We have $\theta X = f(c)$ and $\theta \alpha f(X) = \theta f(X') = f(c) = \theta X$.

§B.1.14 **Lemma (Symmetry of $\alpha$-unifiability).** Let $t$ and $u$ be two terms. We have that $\{t \stackrel{?}{=} u\}$ has an $\alpha$-unifier if and only if $\{u \stackrel{?}{=} t\}$ has one.

*Proof.* To say that $\{t \stackrel{?}{=} u\}$ has an $\alpha$-unifier means that there is some $(\theta, \alpha)$ with $\theta$ a substitution and $\alpha$ a renaming such that $\theta t = \theta \alpha u$, meaning that $t$ and $u$ only differ by a renaming. We only show one implication and the other is similar. Assume $\theta t = \theta \alpha u$ (hypothesis $H$) for some $(\theta, \alpha)$. We define $\theta' := \theta \alpha$ and would like to obtain $\theta' \alpha' t = \theta' u$ for some $\alpha'$. We already know that $\theta t = \theta \alpha u$, hence we need to cancel the renaming $\alpha$ which is part of $\theta'$. We define $\alpha' := \alpha^{-1}$. We finally have $\theta' \alpha' t = \theta \alpha \alpha^{-1} t = \theta t \stackrel{H}{=} \theta \alpha u = \theta' u$ (we used the fact that composition is associative, as stated in Definition B.1.7). $\square$

§B.1.15 These definitions define a preorder on terms. A term $t$ is lesser than another term $u$ when it is more specialised or less general. In terms of substitutions, it means that $t$ can be obtained by instantiating the variables of $u$ with other terms.

§B.1.16 **Definition (Generality relation on terms).** We define the following relation: given $t, u$ two terms, $t \preceq u$ if and only if there exists a substitution $\theta$ such that $t = \theta u$.

§B.1.17 **Proposition.** The relation $\preceq$ defines a preorder.

*Proof.* Let $t$ be a term. If $\theta$ is the identity substitution, we have $t = \theta t$. Let $t_1, t_2, t_3$ be terms. Assume $t_1 = \theta_a t_2$ and $t_2 = \theta_b t_3$. We can compose the two substitutions and obtain $\theta_a \circ \theta_b$. We have $(\theta_a \circ \theta_b) t_3 = \theta_a (\theta_b t_3) = \theta_a t_2 = t_1$. $\square$

§B.1.18 The definition of $\alpha$-unification comes from a simplification of Aubert and Bagnol's definition of *matching* [AB14, Definition 6] itself appearing in Girard's definitions [Gir13b, Section 1.1.2]. However, since *matching* already exists with a different definition in the literature, a different name is chosen. In the proposition below, the two variants are shown to be equivalent.
§B.1.19 **Proposition.** Two terms $t_1$ and $t_2$ are $\alpha$-unifiable if and only if there exists two renamings $\alpha_1$ and $\alpha_2$ such that $\alpha_1 t_1$ and $\alpha_2 t_2$ are unifiable and that $\mathbf{vars}(\alpha_1 t_1) \cap \mathbf{vars}(\alpha_2 t_2) = \emptyset$.

*Proof.* (⇒) Assume that $t_1$ and $t_2$ are $\alpha$-unifiable. Hence, we have $\theta\alpha t_1 = \theta t_2$ for some $(\theta, \alpha)$. We have to find $\psi, \alpha_1$ and $\alpha_2$ such that $\psi\alpha_1 t_1 = \psi\alpha_2 t_2$ and $\mathbf{vars}(\alpha_1 t_1) \cap \mathbf{vars}(\alpha_2 t_2) = \emptyset$. We define $\alpha_2 := \alpha$. Providing there are enough variable symbols, it is possible to design $\alpha_1$ so that $\alpha_1(X) \notin \mathbf{vars}(\alpha_2 t_2)$ for all $X \in \mathbf{vars}(t_1)$, i.e. $\mathrm{img}(\alpha_1) \cap \mathbf{vars}(t_2) = \emptyset$. We then have $\mathbf{vars}(\alpha_1 t_1) \cap \mathbf{vars}(\alpha_2 t_2) = \emptyset$. Now, $\alpha_1 t_1 \stackrel{?}{=} \alpha_2 t_2$ only differ from $t_1 \stackrel{?}{=} \alpha t_2$ by the fact that some variables of $t_1$ have been changed by $\alpha_1$. We can define $\psi$ so that it reverses the effect of $\alpha_1$ without affecting $\alpha_2 t_2$. Hence, we have $\psi := \theta \circ \alpha_1^{-1}$. It has no effect on $\alpha_2 t_2$ because we assumed that $\mathrm{img}(\alpha_1) \cap \mathbf{vars}(t_2) = \emptyset$. ( ⇐ ) Assume that there exists two renamings $\alpha_1$ and $\alpha_2$ such that $\alpha_1 t_1$ and $\alpha_2 t_2$ are unifiable and that $\mathbf{vars}(\alpha_1 t_1) \cap \mathbf{vars}(\alpha_2 t_2) = \emptyset$. We have $\theta\alpha_1 t_1 = \theta\alpha_2 t_2$ for some $\theta$. We can define the substitution $\psi := \theta \circ \alpha_2$ and the renaming $\alpha := \alpha_2^{-1} \circ \alpha_1$ such that $\psi\alpha t_1 = \theta\alpha_2\alpha_2^{-1}\alpha_1 t_1 = \theta\alpha_1 t_1 = \theta\alpha_2 t_2 = \psi t_2$. This shows that $t_1$ and $t_2$ are $\alpha$-unifiable with $(\psi, \alpha)$. $\square$

§B.1.20 It is also possible to define a relation $\leq$ on substitutions instead of terms. This relation is well-known as a preorder in the literature [BN98, Definition 4.5.1]. Its intuitive meaning is that $\theta \leq \psi$ is $\psi$ “more general” than $\theta$.

§B.1.21 **Definition (Generality relation on substitutions).** Let $\theta$ and $\psi$ be two substitutions. We define the relation $\leq$ such that $\theta \leq \psi$ when there exists a substitution $\sigma$ such that $\psi = \sigma\theta$.

§B.1.22 The problem of deciding if a solution to a given problem $P$ exists is known to be decided. Moreover, there exists a maximal solution **solution** $P$ w.r.t. the preorder $\leq$ on substitutions, which is unique up to renaming. Several algorithms were designed to compute the unique solution when it exists, such that the Martelli-Montanari unification algorithm [MM82].

§B.1.23 **Definition (Solved form).** A unification problem $P = \{t_i \stackrel{?}{=} u_i\}_{1 \leq i \leq n}$ is in solved form if:

* for $1 \leq i \leq n$, $t_i$ is a variable $X_i \in V$ and

* no $X_i$ appears in the right-hand side of an equation, i.e.

$$ \{X_i\}_{1 \leq i \leq n} \cap \bigcup_{j=1}^{n} \mathbf{vars}(t_j) = \emptyset. $$
The underlying substitution of $P$ is defined by $\vec{P} := \{X_i \mapsto t_i\}_{1\le i\le n}$.

## B.2 Unification algorithm

§B.2.1 **Definition** (Rules for Martelli-Montanari algorithm). The Martelli-Montanari algorithm is defined by a binary relation $\rightsquigarrow$ (in infix notation) over unification problems. It is defined as follows:

◇ **Clear** $P \cup \{t \stackrel{?}{=} t\} \stackrel{c}{\rightleftharpoons} P$;

◇ **Open** $P \cup \{f(t_1, ..., t_n) \stackrel{?}{=} g(u_1, ..., u_n)\} \stackrel{op}{\rightleftharpoons} P \cup \{t_1 \stackrel{?}{=} u_1, ..., t_n \stackrel{?}{=} u_n\}$ when $f \prec g$;

◇ **Orient** $P \cup \{t \stackrel{?}{=} X\} \stackrel{or}{\rightleftharpoons} P \cup \{X \stackrel{?}{=} t\}$ with $t \notin \text{vars}(t)$;

◇ **Replace** $P \cup \{X \stackrel{?}{=} t\} \stackrel{r(X)}{\rightleftharpoons} \{X \mapsto t\} P \cup \{X \stackrel{?}{=} t\}$
with $X \in \text{vars}(P)$ and $X \notin \text{vars}(t)$.

We simply write $\rightsquigarrow$ when the rule is left implicit and we write $\rightsquigarrow^*$ for the reflexive transitive closure of $\rightsquigarrow$.

§B.2.2 **Definition** (Martelli-Montanari execution). A (Martelli-Montanari) (partial) execution is a non-empty finite sequence of $\rho = (P_1, ..., P_{n+1})$ of unification problems such that $P_i \rightsquigarrow P_{i+1}$ for $1 \le i \le n$. The execution $\rho$ is:

• *successful* if $P_{n+1}$ is in solved form;

• *unsuccessful* if $P_{n+1}$ is not in solved form;

• *full* if there is no $P$ such that $P_{n+1} \rightsquigarrow P$.

§B.2.3 **Theorem** (Correctness and termination of unification algorithm). There exists a full execution $\rho = (P_1, ..., P_n)$ with $P_n$ in solved form if and only if $P_1$ has a solution. Otherwise, $\rho$ is unsuccessful.

*Proof.* Proven in Lassez's article [LMM88, Theorem 3.1]. Other proofs are found in Baader and Nipkow's book [BN98, Lemma 4.6.5 & Lemma 4.6.7 & Lemma 4.6.10]. □

§B.2.4 **Theorem** (Confluence of the unification algorithm). Let $\rho = (P_1, ..., P_n)$ be an execution starting from a solvable problem $P_1$. There exists an extension $\rho' = (Q_1, ..., Q_m)$ such that $\rho \cdot \rho' := (P_1, ..., P_n, Q_1, ..., Q_m)$ is successful.

*Proof.* This corresponds to a result of confluence in rewriting systems [BN98, Definition 2.1.3]. By Theorem B.2.3, we already know that the rewriting system associated to the Martelli-Montanari algorithm is terminating. In addition to this fact, we can use Newman's lemma [BN98, Lemma 2.7.2] by showing that the relation $\rightsquigarrow$ is locally confluent
(cf. [BN98, Lemma 2.7.1]) in order to show that it is confluent. Let $P$ be a unification problem. We consider all the possible divergences of choices induced by the rules of Definition B.2.1.

◇ **Case of clear rule** Let $P$ be a problem and $x$ a rule such that $P \stackrel{x}{\rightsquigarrow} P'$. We have $P \cup \{t \stackrel{?}{=} t\} \stackrel{c}{\rightsquigarrow} P \stackrel{x}{\rightsquigarrow} P'$ and $P \cup \{t \stackrel{?}{=} t\} \stackrel{x}{\rightsquigarrow} P' \cup \{t \stackrel{?}{=} t\} \stackrel{c}{\rightsquigarrow} P'$.

◇ **Case of open rule** Let $P$ be a problem and $x$ a rule such that $P \stackrel{x}{\rightsquigarrow} P'$. We have

$$P \cup \{f(t_1, \dots, t_n) \stackrel{?}{=} f(u_1, \dots, u_n)\}$$

$$\stackrel{op}{\rightsquigarrow} P \cup \{t_1 \stackrel{?}{=} u_1, \dots, t_n \stackrel{?}{=} u_n\}$$

$$\stackrel{x}{\rightsquigarrow} P' \cup \{t_1 \stackrel{?}{=} u_1, \dots, t_n \stackrel{?}{=} u_n\}$$

and

$$P \cup \{f(t_1, \dots, t_n) \stackrel{?}{=} f(u_1, \dots, u_n)\}$$

$$\stackrel{x}{\rightsquigarrow} P' \cup \{f(t_1, \dots, t_n) \stackrel{?}{=} f(u_1, \dots, u_n)\}$$

$$\stackrel{op}{\rightsquigarrow} P' \cup \{t_1 \stackrel{?}{=} u_1, \dots, t_n \stackrel{?}{=} u_n\}.$$

◇ **Case of orient rule** Let $P$ be a problem and $x$ a rule such that $P \stackrel{x}{\rightsquigarrow} P'$. We have $P \cup \{t \stackrel{?}{=} X\} \stackrel{or}{\rightsquigarrow} P \cup \{X \stackrel{?}{=} t\} \stackrel{x}{\rightsquigarrow} P' \cup \{X \stackrel{?}{=} t\}$ and $P \cup \{t \stackrel{?}{=} X\} \stackrel{x}{\rightsquigarrow} P' \cup \{t \stackrel{?}{=} X\} \stackrel{op}{\rightsquigarrow} P' \cup \{X \stackrel{?}{=} t\}$.

◇ **Case of replace** Let $P$ be a problem and $x$ a rule such that $P \stackrel{x}{\rightsquigarrow} P'$. We reason by case on $x$. For more clarity, we write $\theta$ for the substitution $\{X \mapsto t\}$.

◇ **Clear** We have $P \cup \{u \stackrel{?}{=} u, X \stackrel{?}{=} t\} \stackrel{c}{\rightsquigarrow} P \cup \{X \stackrel{?}{=} t\} \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{X \stackrel{?}{=} t\}$ and $P \cup \{u \stackrel{?}{=} u, X \stackrel{?}{=} t\} \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta u \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\} \stackrel{c}{\rightsquigarrow} \theta P \cup \{X \stackrel{?}{=} t\}$.

◇ **Open** We have

$$P \cup \{f(t_1, \dots, t_n) \stackrel{?}{=} f(u_1, \dots, u_n), X \stackrel{?}{=} t\}$$

$$\stackrel{op}{\rightsquigarrow} P \cup \{t_1 \stackrel{?}{=} u_1, \dots, t_n \stackrel{?}{=} u_n, X \stackrel{?}{=} t\}$$

$$\stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta t_1 \stackrel{?}{=} \theta u_1, \dots, \theta t_n \stackrel{?}{=} \theta u_n, X \stackrel{?}{=} t\}$$

and

$$P \cup \{f(t_1, \dots, t_n) \stackrel{?}{=} f(u_1, \dots, u_n), X \stackrel{?}{=} t\}$$

$$\stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta f(t_1, \dots, t_n) \stackrel{?}{=} \theta f(u_1, \dots, u_n), X \stackrel{?}{=} t\}$$

$$= \theta P \cup \{f(\theta t_1, \dots, \theta t_n) \stackrel{?}{=} f(\theta u_1, \dots, \theta u_n), X \stackrel{?}{=} t\}$$

$$\stackrel{op}{\rightsquigarrow} \theta P \cup \{\theta t_1 \stackrel{?}{=} \theta u_1, \dots, \theta t_n \stackrel{?}{=} \theta u_n, X \stackrel{?}{=} t\}.$$
◇ Orient Assume that we have a term $u$ which is not a variable. We have $P \cup \{u \stackrel{?}{=} Y, X \stackrel{?}{=} t\} \stackrel{or}{\rightsquigarrow} P \cup \{Y \stackrel{?}{=} u, X \stackrel{?}{=} t\} \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta Y \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\}$ and $P \cup \{u \stackrel{?}{=} Y, X \stackrel{?}{=} t\} \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta u \stackrel{?}{=} \theta Y, X \stackrel{?}{=} t\} \stackrel{or}{\rightsquigarrow} \theta P \cup \{\theta Y \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\}$. The orient rule in the second reduction works because the substitution $\theta$ does not change the nature of $Y$ and $u$. The first is still a variable and the second still not a variable.

◇ Replace There are two cases. We write $\psi$ for the substitution $\{Y \mapsto u\}$.

• Assume that $X = Y$. We have

$$ 
\begin{align*}
& P \cup \{Y \stackrel{?}{=} u, X \stackrel{?}{=} t\} \\
& \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{\theta Y \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\} \\
& = \theta P \cup \{t \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\} \\
& \text{and} \\
& P \cup \{Y \stackrel{?}{=} u, X \stackrel{?}{=} t\} \\
& \stackrel{r(Y)}{\rightsquigarrow} \psi P \cup \{\psi X \stackrel{?}{=} \psi t, Y \stackrel{?}{=} u\} \\
& = \psi P \cup \{u \stackrel{?}{=} \psi t, Y \stackrel{?}{=} u\}.
\end{align*}
$$

It is then obvious that $t \stackrel{?}{=} u$ and $u \stackrel{?}{=} u$

• Assume that $X \neq Y$. We define $\psi' := \{Y \mapsto \theta u\}$ and $\theta' := \{X \mapsto \psi t\}$. We have

$$ 
\begin{align*}
& P \cup \{Y \stackrel{?}{=} u, X \stackrel{?}{=} t\} \\
& \stackrel{r(X)}{\rightsquigarrow} \theta P \cup \{Y \stackrel{?}{=} \theta u, X \stackrel{?}{=} t\} \\
& \stackrel{r(Y)}{\rightsquigarrow} \psi' \theta P \cup \{X \stackrel{?}{=} \psi' t, Y \stackrel{?}{=} \theta u\} \\
& \text{and} \\
& P \cup \{Y \stackrel{?}{=} u, X \stackrel{?}{=} t\} \\
& \stackrel{r(Y)}{\rightsquigarrow} \psi P \cup \{X \stackrel{?}{=} \psi t, Y \stackrel{?}{=} u\} \\
& \stackrel{r(X)}{\rightsquigarrow} \theta' \psi P \cup \{Y \stackrel{?}{=} \theta' u, X \stackrel{?}{=} \psi t\}.
\end{align*}
$$

□

§B.2.5 Corollary. Let $\rho = (P_1, ..., P_n)$ be an execution starting from a solvable problem $P_1$. There exists an extension $\rho' = (Q_1, ..., Q_m)$ such that $\rho \cdot \rho' := (P_1, ..., P_n, Q_1, ..., Q_m)$ is successful.
*Proof.* By correctness and termination of the unification algorithm (cf. Theorem B.2.3), since $P_1$ is solvable, there exists an execution from $P_1 \rightsquigarrow^* P_f$. Assume that we already started the execution with some arbitrary but valid steps ($P_1, \dots, P_n$). By confluence of the unification algorithm (cf. Theorem B.2.4) □

**§B.2.6 Theorem (Unicity of solution).** If $\rho = (P_1, \dots, P_n)$ is a full execution starting from a solvable problem $P_1$, then $\vec{P}_n$ is the unique solution of $P_1$ modulo $\approx_\alpha$.

*Proof.* Indirectly proven in Lassez's article [LMM88, Theorem 3.17]. The original statement says that any solvable problem $P$ has a unique solution modulo $\approx_\alpha$ but the Martelli-Montanari algorithm computes such a solution by correctness of the algorithm. □

**§B.2.7 Corollary (Execution lifting).** Let $(P, P_1, \dots, P_n)$ be an execution. For all $P'$ such that $P \subseteq P'$, there exists an execution $(P', P'_1, \dots, P'_n)$ such that $P_i \subseteq P'_i$ for $1 \le i \le n$.

*Proof.* By confluence of the unification algorithm (cf. Theorem B.2.4), all paths of execution ultimately lead to a unique result modulo $\approx_\alpha$. We decompose $P'$ into $P \cup P''$ (since it contains $P$). It is possible to focus only on the equation in $P$ without impact on the result. We can then construct the execution $P \cup P'' \rightsquigarrow P_1 \cup P'' \rightsquigarrow^* P_n \cup P''$ corresponding to the execution $P' \rightsquigarrow P'_1 \rightsquigarrow^* P'_n$. □
# Appendix C

## Graph theory

### C.1 Non-directed hypergraphs

Intuitively, hypergraphs are points in space called *vertices* such that some of them are linked together with *hyperedges*. An example of hypergraph is given in Figure C.1.1. Vertices are written $v_i$ and hyperedges $e_i$ for $i \in \mathbb{N}$.

§C.1.1 **Definition (Hypergraph).** A hypergraph $H$ is a tuple $(V, E, \mathbf{end})$ of a set $V$ of elements called *vertices*, a set $E$ of elements called *hyperedges* and a function $\mathbf{end} : E \rightarrow \mathcal{P}(V)$ mapping hyperedges to their associated *endpoints sets*, such that $\mathbf{end}(e) \neq \emptyset$ for all $e \in E$.

§C.1.2 **Example.** The formal definition of the hypergraph illustrated in Figure C.1.1 is given by a tuple $H = (V, E, \mathbf{end})$ such that $V = \{v_1, v_2, v_3, v_4, v_5, v_6, v_7\}$, $E = \{e_1, e_2, e_3, e_4\}$ and $\mathbf{end}(e_1) = \{v_1, v_2, v_3\}$, $\mathbf{end}(e_2) = \{v_2, v_3\}$, $\mathbf{end}(e_3) = \{v_3, v_5, v_6\}$, $\mathbf{end}(e_4) = \{v_4\}$.

§C.1.3 **Definition (Properties of hypergraphs).** Let $H = (V, E, \mathbf{end})$ be a hypergraph.

* The *order* of $H$ is defined by $|V|$;

* The *size* of $H$ is defined by $|E|$;

* The *rank* of $H$, written $\text{rank}(H)$, is the maximal cardinality appearing in $E$, i.e. $\max\{|\mathbf{end}(e)| \text{ such that } e \in E\}$.

§C.1.4 **Definition (Adjacency and incidence).** Let $H = (V, E, \mathbf{end})$ be a hypergraph. Two vertices $x, y \in V$ are *adjacent* when there exists $e \in E$ such that $x, y \in \mathbf{end}(e)$. Two hyperedges $e, e' \in E$ are *incident* when $\mathbf{end}(e) \cap \mathbf{end}(e') \neq \emptyset$.

§C.1.5 **Example.** In Figure C.1.1, $v_1$ and $v_2$ are adjacent because $v_1, v_2 \in \mathbf{end}(e_1)$. The hyperedges $e_1$ and $e_2$ are incident because $\mathbf{end}(e_1) \cap \mathbf{end}(e_2) = \{v_2, v_3\}$. However, $v_1$ and $v_4$ are not adjacent since no hyperedge link them and, $e_1$ and $e_4$ are not incident because they do not link common vertices.
<figure><img src="image_137.png" /><figcaption>Figure C.1.1: Example of hypergraph taken from a StackExchange post: https://tex. stackexchange.com/questions/1175/drawing-a-hypergraph.</figcaption></figure>

§C.1.6 **Definition (Simple hypergraph).** A hypergraph $H = (V, E, \text{end})$ is simple when for all $e, e' \in E$ such that $\text{end}(e) \subseteq \text{end}(e')$, we have $i = j$.

§C.1.7 **Example.** The hypergraph of Figure C.1.1 is not simple because $\text{end}(e_2) \subseteq \text{end}(e_1)$ and $e_1 \neq e_2$. The point is to remove redundant links. Since $e_1$ already links $v_2$ and $v_3$ together, it is possible to forget the hyperedge $e_2$.

§C.1.8 **Definition (Path).** Let $H = (V, E, \text{end})$ be a hypergraph. A path $\rho$ in $H$ from $v_1 \in V$ to $v_{n+1} \in V$ is an alternate sequence of vertices and hyperedges

$$ \rho = (v_1, e_1, v_2, e_2, \dots, v_n, e_n, v_{n+1}) $$

where:

* the $v_i$ are pairwise distinct with the exception of the pair $(v_1, v_{n+1})$, i.e. we can have $v_1 = v_{n+1}$;

* the $e_i$ are all distinct;

* for all $1 \le i \le n$, we have $v_i, v_{i+1} \in \text{end}(e_i)$.

The length of the path is $|\rho| = n$. If $x_1 = x_{n+1}$, then $\rho$ is called a cycle.

§C.1.9 **Example.** A possible path in the hypergraph of Figure C.1.1 from $v_1$ to $v_3$ is

$$ \rho := (v_1, e_1, v_2, e_2, v_3). $$

A possible cycle (which is a loop) is $(v_4)$.
§C.1.10 **Definition (Cyclicity).** A hypergraph containing at least one cycle is called *cyclic*. Otherwise (if it has no cycles), it is *acyclic*.

There exists several notions of acyclicity (α-acyclicity and β-acyclicity for instance) but we will not need them in this thesis.

§C.1.11 **Definition (Connectedness).** A hypergraph $H = (V, E, \text{end})$ is connected when there is a path between all pairs of vertices in $V$. Otherwise, it is disconnected.

§C.1.12 **Definition (Hypergraph homomorphism).** A homomorphism $f$ between two hypergraphs $H = (V_H, E_H, \text{end}_H)$ and $H' = (V_{H'}, E_{H'}, \text{end}_{H'})$ is given by the two following underlying maps with same name:

* $f: V_H \to V_{H'}$ (the vertex map) and

* $f: E_H \to E_{H'}$ (the edge map)

such that $f(\text{end}_H(e)) = \text{end}_{H'}(f(e))$ for all $e \in E_H$, i.e. it maps adjacent vertices to adjacent vertices.

§C.1.13 **Definition (Injectivity and surjectivity of homomorphisms).** Let $f: H \to H'$ be a hypergraph homomorphism. It is:

* *injective* (or an injection) when its underlying maps are injective, i.e. $f(x) = f(x')$ implies $x = x'$ for $x, x'$ edges or vertices of $H$;

* *surjective* (or a surjection) when its underlying maps are surjective, i.e. for every $y$ (edge or vertex of $H'$), there is some $x$ that generates it, i.e. there is some $x$ such that $f(x) = y$.

§C.1.14 **Definition (Hypergraph isomorphism).** Let $f$ be a hypergraph homomorphism between two hypergraph homomorphism $H$ and $H'$. It is a *hypergraph isomorphism* if and only if its underlying maps are bijective, i.e. both injective and surjective. We then say that $H$ and $H'$ are *isomorphic*, written $H \simeq H'$.

Since the underlying maps of an isomorphism are bijective, it induces an inverse isomorphism in the same way that bijections induce inverse functions.

§C.1.15 **Proposition.** A hypergraph homomorphism $f$ between two hypergraphs

$$H = (V_H, E_H, \text{end}_H) \quad \text{and} \quad H' = (V_{H'}, E_{H'}, \text{end}_{H'})$$

is an isomorphism if and only if there exists a bijection $f^{-1}$ such that $f \circ f^{-1} = f^{-1} \circ f = \text{id}_H$ where $\text{id}_H$ is the identity morphism over $H$ defined by the two identity maps $f: V_H \to V_H$ such that $f(v) = v$ and $f: E_H \to E_H$ such that $f(e) = e$.
<figure><img src="image_138.png" /><figcaption>Figure C.1.2: A hypergraph homomorphism $f$ relating two hypergraphs such that $f(v_1) = f(v_2) = v'_1$, $f(v_3) = v'_3$, $f(v_4) = f(v_7) = v'_4$, $f(v_5) = v'_5$, $f(v_6) = v'_6$, $f(e_1) = f(e_2) = e'_1$, $f(e_3) = e'_3$ and $f(e_4) = e'_4$.</figcaption></figure>

§C.1.16 **Example.** A hypergraph homomorphism is illustrated in Figure C.1.2. It makes the hyperedge $e_2$ linking $v_2$ and $v_3$ disappear by merging it with $e_1$. We have $f(\text{ende}_2) = f(\{v_2, v_3\}) = \{v'_1, v'_3\} = \text{end}(e'_1) = \text{end}(f(e_2))$. The isolated vertex $v_7$ also disappears.

In the case of an isomorphisms, we expect $H$ and $f(H)$ to be structurally equivalent. The typical example maps a hypergraph to the same graph up to renaming of vertices and hyperedges.

## C.2 Directed hypergraphs

It is possible to consider directions in hypergraphs by considering that hyperedges have inputs and outputs.

§C.2.1 **Definition (Directed hypergraph).** A directed hypergraph is a tuple

$$H = (V, E, \text{in}, \text{out})$$

where $V$ is the set of vertices, $E$ the set of hyperedges (called hyperarcs) and the two functions $\text{in}: E \to \mathcal{P}(V)$ and $\text{out}: E \to \mathcal{P}(V)$ are respectively the set of inputs and outputs associated to the hyperarc $e$.

Remark that we allow hyperarcs with no input or no output (for a hyperarc $e$, we may have $\text{in}(e) = \emptyset$ or $\text{out}(e) = \emptyset$).

§C.2.2 **Definition (Directed path).** Let $H = (V, E, \text{in}, \text{out})$ be a directed hypergraph. A path $\rho$ in $H$ from $v_1 \in V$ to $v_{n+1} \in V$ is an alternate sequence of vertices and hyperedges

$$\rho = (v_1, e_1, v_2, e_2, \dots, v_n, e_n, v_{n+1})$$
<figure><img src="image_139.png" /><figcaption>Figure C.2.1: Test.</figcaption></figure>

where:

* the $v_i$ are pairwise distinct with the exception of the pair $(v_1, v_{n+1})$, i.e. we can have $v_1 = v_{n+1}$;

* the $e_i$ are all distinct;

* for all $1 \le i \le n$, we have $v_i \in \text{in}(e_i)$ and $v_{i+1} \in \text{out}(e_{i+1})$.

The length of the path is $|\rho| = n$. If $v_1 = v_{n+1}$, then $\rho$ is called a circuit (or n-circuit if we want to make the length explicit).

It is possible to recover undirected graphs by considering symmetric directions.

**§C.2.3 Definition (Symmetric hypergraph).** Let $H = (V, E, \text{in}, \text{out})$ be a directed hypergraph. It is symmetric if for each vertices $v, v'$, there are two hyperedges $e, e'$ such that $v \in \text{in}(e)$, $v' \in \text{out}(e)$, $v' \in \text{in}(e)$ and $v \in \text{out}(e)$.

A hypergraph can also be given an orientation which should be understood as a strict direction, i.e. edges go in one specific direction without leaving the possibility of going back.

**§C.2.4 Definition (Oriented hypergraph).** A directed hypergraph is oriented when it contains no symmetry, i.e. there is no vertices $v, v'$ and edges $e, e'$ such that $v \in \text{in}(e)$, $v' \in \text{out}(e)$, $v' \in \text{in}(e)$ and $v \in \text{out}(e)$.

**§C.2.5 Example.** In Figure C.2.1, we have an example of directed hypergraph

$$H = (V, E, \text{in}, \text{out})$$

such that $V = \{v_1, v_2, v_3, v_4\}$ and $E = \{e_1, e_2, e_3\}$ with:

* $\text{in}(e_1) = \{v_2\}$ and $\text{out}(e_1) = \{v_1\}$;

* $\text{in}(e_2) = \{v_3, v_5\}$ and $\text{out}(e_2) = \{v_4\}$;

* $\text{in}(e_3) = \emptyset$ and $\text{out}(e_3) = \{v_3\}$.

Directed hypergraph homomorphisms must preserve inputs and outputs.
§C.2.6 **Definition** (Directed hypergraph homomorphism). A homomorphism $f$ between two directed hypergraphs $H = (V, E, \text{in}_H, \text{out}_H)$ and $H' = (V_{H'}, E_{H'}, \text{in}_{H'}, \text{out}_{H'})$ is given by the two following maps with same name:

• $f: V_H \to V_{H'}$ (the vertex map) and

• $f: E_H \to E_{H'}$ (the edge map)

such that $f(\text{in}_H(e)) = \text{in}_{H'}(f(e))$ and $f(\text{out}_H(e)) = \text{out}_{H'}(f(e))$ for all $e \in E_H$, i.e. the functions $f$ maps components (vertices and hyperarcs) of $H$ to components of $H'$ by preserving the linking of vertices by hyperarcs.

It is sometimes useful to consider an order in inputs and outputs by extending directed hypergraphs to *ordered* directed hypergraphs.

§C.2.7 **Definition** (Ordered directed hypergraph). An *ordered directed hypergraph* $H = (V, E, \text{in}, \text{out}, \leq)$ is a directed hypergraph $(V, E, \text{in}, \text{out})$ extended with an order relation $\leq$ over $V \times V$.

§C.2.8 **Notation.** We write $\{u_1, \dots, u_n\} \stackrel{e}{\mapsto} \{v_1, \dots, v_m\}$ for an hyperedge $e$ such that $\text{in}(e) = \{u_1, \dots, u_n\}$ and $\text{out}(e) = \{v_1, \dots, v_m\}$.

In case inputs and outputs are ordered (when we have an ordered hypergraph), then we write $[u_1, \dots, u_n] \stackrel{e}{\mapsto} [v_1, \dots, v_m]$ instead.

## C.3 Special cases of hypergraphs

### Multigraphs and graphs

§C.3.1 **Definition** (Multigraph). A *multigraph* is a hypergraph $H$ such that $\text{rank}(H) \leq 2$ (hyperedges only link two vertices or are loops over a vertex). Hyperedges are called *edges* in the case of a multigraph.

§C.3.2 **Definition** (Graph). A loop in a hypergraph $H = (V, E, \text{end})$ is an edge $e$ such that $|\text{end}(e)| = 1$. A *graph* is a simple multigraph $H$ without loop.

§C.3.3 **Example.** An example of multigraph is illustrated in Figure C.3.1a and an example of graph is illustrated in Figure C.3.1b. The lines between vertices are *edges*. For instance, in Figure C.3.1a, $v_1$ and $v_5$ are linked by some hyperedge $e$ such that $\text{end}(e) = \{v_1, v_5\}$, and $v_2$ is connected to itself by a loop, which is a hyperedge $e'$ such that $\text{end}(e') = \{v_2\}$.

In the directed case, we simply write arrows instead of lines between vertices.
<figure><img src="image_140.png" /><figcaption>Figure C.3.1: Example of special cases of hypergraph.</figcaption></figure>

§C.3.4 Notation. We write $u \stackrel{e}{\mapsto} v$ for a directed edge $e$ such that $\text{in}(e) = u$ and $\text{out}(e) = v$.

## Bipartite multigraph

A bipartite multigraph is a multigraph in which the set of vertices can be divided into two disjoint parts such that all edges link an element from one part to the other.

§C.3.5 Definition (Bipartite multigraph). A bipartite multigraph $G = (V, E, \text{end})$ is a multigraph $(V, E)$ such that $V = V_1 \uplus V_2$ and for each $e \in E$, we have $\text{end}(e) = \{v_1, v_2\}$ such that $v_1 \in V_1$ and $v_2 \in V_2$.

## Square grid graph

§C.3.6 Definition (Line graph). A line graph or path graph is a graph $G = (V, E, \text{end})$ where $V$ is an ordered sequence of vertices $[v_1, ..., v_n]$ with $n \ge 1$ and $E$ is an ordered sequence of edges $[e_1, ..., e_{n-1}]$ such that $v_i, v_{i+1} \in \text{end}(e_i)$.

§C.3.7 Definition (Cartesian product of graphs). Let

$$G = (V_G, H_G, \text{end}_G) \quad \text{and} \quad G' = (V_{G'}, H_{G'}, \text{end}_{G'})$$

be two graphs. Their cartesian product is the graph $G \square G' = (V_{G \square G'}, E_{G \square G'}, \text{end}_{G \square G'})$ such that $V_{G \square G'} = V_G \times V_{G'}$ and two vertices $(u, v)$ and $(u', v')$ are adjacent when either $u = u'$ and $v$ is adjacent to $v'$, or $v = v'$ and $u$ is adjacent to $u'$.

§C.3.8 Definition (Square grid graph). Let $G$ be a line graph of size $n$. The associated grid graph is given by the graph product $G \square G$.
<figure><img src="image_141.png" /><figcaption>Figure C.3.2: Example of square grid graph.</figcaption></figure>

An example of line graph and grid graph is given in Figure C.3.2. Grid graphs can be used to represent a finite subset of a set $E^2$ and more typically, the plane $Z^2$.
# Appendix D

## Transcendental aesthetics

In this section, I propose to revisit Kant's transcendental aesthetics in light of Girard's transcendental syntax. You will find a sequence of pictorial entities accessible through the pure intuition of (pixel) space and (waste of) time. It could be made into an NFT collection but I will freely share these pieces of art instead. It is inspired by Girard's "pure waste of paper" [Gir01, Appendix A]. This section itself may be seen as a pure waste of paper as well.

<figure><img src="image_142.png" /><figcaption>$[+a(X), +b(X)]$ 
Identity.</figcaption></figure>

<figure><img src="image_143.png" /><figcaption>$[-a(X), a(X)] + [-b(X), b(X)]$ 
Test for identity.</figcaption></figure>
<figure><img src="image_144.png" /></figure>

$$[-\omega(X), +\omega(f(X))]$$

Black hole.

<figure><img src="image_145.png" /></figure>

$$[+a(X), +b(X)] + [-c(X), -d(X)] + [+e(X), -f(X)]$$

Adapters.

<figure><img src="image_146.png" /></figure>

$$[+nat(0)] + [-nat(X), +nat(s(X))] + [-nat(X), nat(X)]$$

Natural numbers.
<figure><img src="image_147.png" /></figure>

$$ \begin{bmatrix} +a(X), +b(X) \\ -a(X), -b(X) \end{bmatrix}, \begin{bmatrix} +a(X), +b(X) \\ -a(X), -b(X) \end{bmatrix} $$

<figure><img src="image_148.png" /><figcaption>Rhizome.</figcaption></figure>

$$ \begin{bmatrix} +a(+b(t)) \\ -a(X), X \end{bmatrix} $$

<figure><img src="image_149.png" /><figcaption>True digging.</figcaption></figure>

$$ \begin{bmatrix} \dots, +a(X) \\ \dots, -a(X), -b(X) \\ \dots, +b(X), \dots \end{bmatrix} $$

<figure><img src="image_150.png" /><figcaption>The Holy Quaternity of Logic.</figcaption></figure>
<figure><img src="image_151.png" /><figcaption>The Synthetic Compass.</figcaption></figure>
<figure><img src="image_152.png" /></figure>

Menu de Maestracci

<figure><img src="image_153.png" /></figure>

-10% de réduction pour les chercheurs en informatique théorique

Entrée – 4€

Pâtes salées avant ébullition ou
Salade de connecteurs Broccoli (sauce à la Tarski) ou
Camembert mou à la Frege

Plat – 14€

Viande au feu classique (à la moutarde de montre) ou
Steak tartare linéaire (★ spécialité du chef)

Dessert (sorbet sémantique) – 5€

Parfum poire ou
Parfum poire+vanille+lait ou
Sorbet chaud à la tortue ou
Sorbet de petit salé aux lentilles

Boissons – Gratuit

(à volonté avec carte de fidélité sinon un seul service)

Bière 1L

Vin 1L

Maestracci's menu.
* Pâtes salées avant ébullition : “*Le fantôme de la transparence*”;

* Salade de connecteurs Broccoli : “*On the meaning of logical rules I : syntax vs. semantics*”;

* Camembert mou à la Frege : “*Proofs and Types*”;

* Moutarde de montre : “*Mustard watches, an integrated approach to time and food*”;

* Viande au feu classique : “*Shrodinger's cut*”;

* Steak tartare linéaire : “*Shrodinger's cut*”;

* Sorbet sémantique : “*La syntaxe transcendantale, un manifeste*”.

References for Maestracci's menu.
<figure><img src="image_154.png" /><figcaption>Vulcan forging the Thunderbolts of Jupiter (Rubens)</figcaption></figure>
References

[AB09] Sanjeev Arora and Boaz Barak. *Computational complexity: a modern approach*. Cambridge University Press, 2009. doi:10.1017/CBO9780511804090.

[AB14] Clément Aubert and Marc Bagnol. Unification and logarithmic space. In *Rewriting and Typed Lambda Calculi*, pages 77–92. Springer, 2014. doi:10.1007/978-3-319-08918-8_6.

[ABCJ98] David Albrecht, Frank A. Bäuerle, John N. Crossley, and John S. Jeavons. *Curry-Howard terms for linear logic*, volume 61. Springer, 1998. URL: http://www.jstor.org/stable/20016001.

[Abe06] Paul Abelson. *The seven liberal arts: A study in mediaeval culture*. Teachers’ College, Columbia University, 1906.

[Abr91] V. Michele Abrusci. Phase semantics and sequent calculus for pure non-commutative classical linear propositional logic. *The Journal of Symbolic Logic*, 56(4):1403–1451, 1991. doi:10.2307/2275485.

[Abr94] Samson Abramsky. Proofs as processes. *Theoretical Computer Science*, 135(1):5–9, 1994. URL: https://www.sciencedirect.com/science/article/pii/0304397594001030, doi:https://doi.org/10.1016/0304-3975(94)00103-0.

[Abr16] Samson Abramsky. Information, processes and games. *Philosophy of Information*, 2016. URL: https://arxiv.org/abs/1604.02603, doi:10.48550/arXiv.1604.02603.

[ABS16] Clément Aubert, Marc Bagnol, and Thomas Seiller. Unary resolution: Characterizing PTIME. In *International Conference on Foundations of Software Science and Computation Structures*, pages 373–389. Springer, 2016. doi:10.1007/978-3-662-49630-5_22.

[Acc18] Beniamino Accattoli. Proof nets and the linear substitution calculus. In *International Colloquium on Theoretical Aspects of Computing*, pages 37–61. Springer, 2018. doi:10.1007/978-3-030-02508-3_3.

[ACCL91] Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. *Journal of functional programming*, 1(4):375–416, 1991. URL: https://www.cambridge.org/
core/journals/journal-of-functional-programming/article/
explicit-substitutions/C1B1AFAE8F34C953C1B2DF3C2D4C2125,
doi:10.1017/S0956796800000186.

[ACJ97] David Albrecht, John N Crossley, and John S. Jeavons. New Curry-Howard terms for full linear logic. *Theoretical computer science*, 185(2):217-235, 1997. URL: https://www.sciencedirect.com/science/article/pii/S0304397597000443, doi:10.1016/S0304-3975(97)00044-3.

[AJ94] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. *The Journal of Symbolic Logic*, 59(2):543-574, 1994. doi:10.2307/2275407.

[AK12] Jesse Alama and Johannes Korbmacher. The lambda calculus. 2012. URL: https://plato.stanford.edu/entries/lambda-calculus/.

[AL95] Andrea Asperti and Cosimo Laneve. Paths, computations and labels in the λ-calculus. *Theoretical Computer Science*, 142(2):277-297, 1995. URL: https://www.sciencedirect.com/science/article/pii/S0304397594002797, doi:10.1016/0304-3975(94)00279-7.

[AM20] Matteo Acclavio and Roberto Maieli. Generalized connectives for multiplicative linear logic. In *28th EACSL Annual Conference on Computer Science Logic (CSL 2020)*. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2020. URL: https://drops.dagstuhl.de/opus/volltexte/2020/11649/, doi:10.4230/LIPIcs.CSL.2020.6.

[Ama16] Roberto Amadio. Operational methods in semantics. 2016. URL: https://hal.science/cel-01422101v2/.

[And76] Andrews. Refutations by matings. *IEEE transactions on computers*, 100(8):801-807, 1976. URL: https://ieeexplore.ieee.org/document/1674698, doi:10.1109/TC.1976.1674698.

[And92] Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. *Journal of logic and computation*, 2(3):297-347, 1992. doi:doi.org/10.1093/logcom/2.3.297.

[AP14] V. Michele Abrusci and Paolo Pistone. On transcendental syntax: A kantian program for logic? 2014. URL: https://www.academia.edu/10495057/On-Trascendental_syntax_a_Kantian_program_for_logic.

[AR99] V. Michele Abrusci and Paul Ruet. Non-commutative logic I: the multiplicative fragment. *Annals of pure and applied logic*, 101(1):29-64, 1999. URL: https://www.sciencedirect.com/science/article/pii/S0168007299000147, doi:10.1016/S0168-0072(99)00014-7.
[AS16a] Clément Aubert and Thomas Seiller. Characterizing co-NL by a group action. *Mathematical Structures in Computer Science*, 26(4):606-638, 2016. URL: https://hal.science/hal-01005705/, doi:10.1017/S0960129514000267.

[AS16b] Clément Aubert and Thomas Seiller. Logarithmic space and permutations. *Information and Computation*, 248:2-21, 2016. URL: https://www.sciencedirect.com/science/article/pii/S0890540115001364, doi: 10.1016/j.ic.2014.01.018.

[Bag14] Marc Bagnol. *On the resolution semiring*. PhD thesis, Aix-Marseille Université, 2014. URL: https://www.normalesup.org/~bagnol/phd/these_screen.pdf.

[Bar91] Michael Barr. *-autonomous categories and linear logic. *Mathematical Structures in Computer Science*, 1(2):159-178, 1991. doi:10.1017/S0960129500001274.

[Bar01] Chris Barker. Iota and Jot: the simplest languages? *The Esteric Programming Languages Webring*, 2001. URL: http://semarch.linguistics.fas.nyu.edu/barker/Iota/.

[Bar21] Davide Barbarossa. *Towards a resource based approximation theory of programs*. PhD thesis, Université Sorbonne Paris Nord, 2021. URL: https://theses.hal.science/tel-03886068v1.

[BC06] Normand Baillargeon and Charb. *Petit cours d'autodéfense intellectuelle*. Lux, 2006.

[BC18] Mikołaj Bojańczyk and Wojciech Czerwiński. Automata toolbox. 2018.

[BDS15] Marc Bagnol, Amina Doumane, and Alexis Saurin. On the dependencies of logical rules. In *International Conference on Foundations of Software Science and Computation Structures*, pages 436-450. Springer, 2015. doi: 10.1007/978-3-662-46678-0_28.

[Bef06] Emmanuel Beffara. A concurrent model for linear logic. *Electronic Notes in Theoretical Computer Science*, 155:147-168, 2006. URL: https://www.sciencedirect.com/science/article/pii/S1571066106001927, doi: 10.1016/j.entcs.2005.11.055.

[Bel62] Nuel D. Belnap. Tonk, plonk and plink. *Analysis*, 22(6):130-134, 1962. doi:10.2307/3326862.

[Ber66] Robert Berger. *The undecidability of the domino problem*. American Mathematical Soc., 1966. doi:10.1090/MEMO/0066.

[BF97] Cesare Burali-Forti. Una questione sui numeri transfiniti. *Rendiconti del Circolo Matematico di Palermo (1884-1940)*, 11(1):154-164, 1897. doi: 10.1007/BF03015911.
[BF11] Michele Basaldella and Claudia Faggian. Ludics with repetitions (expone nentials, interactive types and completeness). *Logical Methods in Com- puter Science*, 7, 2011. URL: https://lmcs.episciences.org/1095, doi:10.2168/LMCS-7(2:13)2011.

[Bib13] Wolfgang Bibel. Automated theorem proving. Springer Science & Business Media, 2013. doi:10.1007/978-3-322-90102-6.

[BK08] Christel Baier and Joost-Pieter Katoen. Principles of model checking . MIT press, 2008.

[Bla92] Andreas Blass. A game semantics for linear logic. Annals of Pure and Applied logic , 56(1-3):183–220, 1992. URL: https://www. sciencedirect.com/science/article/pii/0168007292900739, doi: 10.1016/0168-0072(92)90073-9.

[Bla98] Deborah L. Black. Logic in Islamic philosophy. Routledge Encyclopedia of Philosophy , 5:706–13, 1998. doi:10.4324/9780415249126-H017-1.

[BN98] Franz Baader and Tobias Nipkow. Term rewriting and all that . Cambridge university press, 1998. doi:10.1017/CBO9781139172752.

[Boc61] Józef Maria Bochenski. A history of formal logic . University of Notre Dame Press, 1961. URL: https://circulosemiotico.files..wordpress.com/2012/10/historyofformal100boch.pdf.

[BP84] Paul Benacerraf and Hilary Putnam. Philosophy of mathematics: Selected readings . Cambridge University Press, 1984.

[BP99] Patrick Baillot and Marco Pedicini. Elementary complexity and geometry of interaction. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications , pages 25–33, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg.

[Brü04] Kai Brünnler. Deep inference and symmetry in classical proofs . Logos Verlag Berlin, 2004. URL: https://iccl.inf.tu-dresden.de/web/ Phdthesis3005/en.

[BT09] Michele Basaldella and Kazushige Terui. On the meaning of logical com- pleteness. In International Conference on Typed Lambda Calculi and Ap- plications , pages 50–64. Springer, 2009. URL: https://arxiv.org/abs/ 1011.1625, doi:10.48550/arXiv.1011.1625.

[Bur00] Stanley Burris. The laws of Boole’s thought. Preprint , 2000.

[CC23] Simon Castellan and Pierre Clairambault. The geometry of causality: Multi-token geometry of interaction and its causal unfolding. Proceedings of the ACM on Programming Languages , 7(POPL):689–717, 2023. URL: https://dl.acm.org/doi/abs/10.1145/3571217, doi:10.1145/ 3571217.
[CDG+97] Hubert Comon, Max Dauchet, Remi Gilleron, Florent Jacquemard, Denis Lugiez, Christof Löding, Sophie Tison, and Marc Tommasi. Tree automata techniques and applications. Available online since, 1997. URL: https://inria.hal.science/hal-03367725.

[Chm09] Janusz Chmielewski. Language and Logic in Ancient China: Collected Papers on the Chinese Language and Logic. Warsaw: PAN, 2009.

[Chu32] Alonzo Church. A set of postulates for the foundation of logic. Annals of mathematics, pages 346-366, 1932. URL: https://www.jstor.org/stable/1968337, doi:10.2307/1968337.

[Chu40] Alonzo Church. A formulation of the simple theory of types. The journal of symbolic logic, 5(2):56-68, 1940. doi:10.2307/2266170.

[CI96] Karel Culik II. An aperiodic set of 13 Wang tiles. Discrete Mathematics, 160(1-3):245-251, 1996. URL: https://www.sciencedirect.com/science/article/pii/S0012365X96001185, doi:10.1016/S0012-365X(96)00118-5.

[Col58] Henry Thomas Colebrooke. Essays on the Religion and Philosophy of the Hindus. Williams and Norgate, 1858.

[Con22] Sidney Congard. La logique face à l'arbitraire. 2022. URL: https://hal.science/hal-03689001/.

[CR96] Alain Colmerauer and Philippe Roussel. The birth of Prolog. In History of Programming Languages—II, page 331-367. Association for Computing Machinery, New York, NY, USA, 1996. URL: https://dl.acm.org/doi/10.1145/234286.1057820, doi:10.1145/234286.1057820.

[Cur34] Haskell B. Curry. Functionality in combinatory logic. Proceedings of the National Academy of Sciences of the United States of America, 20(11):584, 1934. URL: https://www.pnas.org/doi/pdf/10.1073/pnas.20.11.584, doi:10.1073/pnas.20.11.584.

[Cur03] Pierre-Louis Curien. Symmetry and interactivity in programming. Bulletin of Symbolic Logic, pages 169-180, 2003. URL: https://www.jstor.org/stable/3094788.

[Cur05a] Pierre-Louis Curien. Introduction to linear logic and ludics, part I. arXiv preprint cs/0501035, 2005. URL: https://arxiv.org/abs/cs/0501035, doi:10.48550/arXiv.cs/0501035.

[Cur05b] Pierre-Louis Curien. Introduction to linear logic and ludics, part II. arXiv preprint cs/0501039, 2005. URL: https://arxiv.org/abs/cs/0501039, doi:10.48550/arXiv.cs/0501039.
[CVV21] Kostia Chardonnet, Benoît Valiron, and Renaud Vilmart. Geometry of Interaction for ZX-Diagrams. In Filippo Bonchi and Simon J. Puglisi, editors, *46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)*, volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1–30:16, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/opus/volltexte/2021/14470, doi:10.4230/LIPIcs.MFCS.2021.30.

[Dan90] Vincent Danos. *La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du Lambda-calcul)*. PhD thesis, Paris 7, 1990. URL: https://perso.ens-lyon.fr/pierre.lescanne/PUBLICATIONS/DanosPhD.pdf.

[Dav58] Martin Davis. Computability and Unsolvability. 1982 ed, 1958. doi:10.2307/2273892.

[DC18] Daniel De Carvalho. Execution time of λ-terms via denotational semantics and intersection types. *Mathematical Structures in Computer Science*, 28(7):1169–1203, 2018. URL: https://arxiv.org/abs/0905.4251, doi:10.48550/arXiv.0905.4251.

[DCK97] Roberto Di Cosmo and Delia Kesner. Strong normalization of explicit substitutions via cut elimination in proof nets. In *Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science*, pages 35–46. IEEE, 1997. URL: https://ieeexplore.ieee.org/document/614927, doi:10.1109/LICS.1997.614927.

[DCKP03] Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonovski. Proof nets and explicit substitutions. *Mathematical Structures in Computer Science*, 13(3):409, 2003. doi:10.1017/S0960129502003791.

[DEGV01] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov. Complexity and expressive power of logic programming. *ACM Comput. Surv.*, 33(3):374–425, sep 2001. doi:10.1145/502807.502810.

[Des16] Joëlle Despeyroux. (mathematical) logic for systems biology. In *Computational Methods in Systems Biology*, 2016. URL: https://wwwsemanticscholar.org/paper/(Mathematical)-Logic-for-Systems-Biology-(Invited-Despeyroux/c4789e2f981ae3ad82f565cb3964993efccf5fe1, doi:10.1007/978-3-319-45177-0_1.

[DFLO19] Joëlle Despeyroux, Amy Felty, Pietro Liò, and Carlos Olarte. A logical framework for modelling breast cancer progression. In *Madalena Chaves and Manuel A. Martins, editors, Molecular Logic and Computational Synthetic Biology*, pages 121–141, Cham, 2019. Springer International Publishing. doi:10.1007/978-3-030-19432-1_8.
[Dij01] Edsger W. Dijkstra. Solution of a problem in concurrent programming control. In *Pioneers and Their Contributions to Software Engineering*, pages 289–294. Springer, 2001. doi:10.1145/365559.365617.

[DJS95] Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. Lkq and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication. *Advances in Linear Logic*, 222:211–224, 1995. URL: https://wwwsemanticscholar.org/paper/LKQ-and-LKT%3A-sequent-calculi-for-second-order-logic-Danos-Joinet/20fb476610426c30608714e984a451cc1108c659.

[DLTY17] Ugo Dal Lago, Ryo Tanaka, and Akira Yoshimizu. The geometry of concurrent interaction: Handling multiple ports by way of multiple tokens. In *2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–12. IEEE, 2017. URL: https://www.computer.org/csdl/proceedings-article/lics/2017/08005112/120mNwE90zy, doi: 10.1109/LICS.2017.8005112.

[DM60] Augustus De Morgan. *Syllabus of a proposed system of logic*. Walton and Maberly, 1860.

[dMDF+20] Elisabetta de Maria, Joelle Despeyroux, Amy Felty, Pietro Lió, Carlos Olarte, and Abdorrahim Bahrami. Computational logic for biomedicine and neurosciences. *ArXiv*, 2020. URL: https://arxiv.org/abs/2007.07571, doi:10.48550/arXiv.2007.07571.

[DP60] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. *Journal of the ACM (JACM)*, 7(3):201–215, 1960. URL: https://dl.acm.org/doi/10.1145/321033.321034, doi: 10.1145/321033.321034.

[DR89] Vincent Danos and Laurent Regnier. The structure of multiplicatives. *Archive for Mathematical logic*, 28(3):181–203, 1989. doi:10.1007/BF01622878.

[DR95] Vincent Danos and Laurent Regnier. Proof-nets and the hilbert space. In Jean-Yves Girard, Yves Lafont, and Laurent Editors Regnier, editors, *Advances in Linear Logic*, London Mathematical Society Lecture Note Series, page 307–328. Cambridge University Press, 1995. doi:10.1017/CBO9780511629150.016.

[DR99] Vincent Danos and Laurent Regnier. Reversible, irreversible and optimal $\lambda$-machines. *Theoretical Computer Science*, 227(1-2):79–97, 1999. URL: https://www.sciencedirect.com/science/article/pii/S0304397599000493, doi:10.1016/S0304-3975(99)00049-3.
[Duc09] Etienne Duchesne. *La localisation en logique: géométrie de l'interaction et sémantique dénotationnelle*. PhD thesis, Université Aix-Marseille II, 2009. URL: https://www.theses.fr/2009AIX22080.

[Dum91] Michael Dummett. *The logical basis of metaphysics*. Harvard university press, 1991.

[EIK09] Thomas Eiter, Giovambattista Ianni, and Thomas Krennwallner. Answer set programming: A primer. In *Reasoning Web International Summer School*, pages 40–110. Springer, 2009. doi:10.1007/978-3-642-03754-2_2.

[EMJP19] Joanna Ellis-Monaghan, Nataša Jonoska, and Greta Pangborn. Tile-based DNA nanostructures: mathematical design and problem encoding. *Algebraic and Combinatorial Computational Biology*, pages 35–60, 2019. URL: https://www.sciencedirect.com/science/article/abs/pii/B9780128140666000027, doi:10.1016/B978-0-12-814066-6.00002-7.

[EO91] Norbert Eisinger and Hans Jürgen Ohlbach. Deduction systems based on resolution. 1991. URL: https://uir.unisa.ac.za/handle/10500/24123.

[F+79] Gottlob Frege et al. Begriffsschrift, a formula language, modeled upon that of arithmetic, for pure thought. *From Frege to Gödel: A source book in mathematical logic*, 1931:1–82, 1879.

[Fac83] R. Lance Factor. What is the "logic" in buddhist logic? *Philosophy East and West*, 33(2):183–188, 1983. URL: https://www.jstor.org/stable/1399101, doi:10.2307/1399101.

[Fer01] José Ferreirós. The road to modern logic—an interpretation. *Bulletin of Symbolic Logic*, 7(4):441–484, 2001. doi:10.2307/2687794.

[FF03] John Fuegi and Jo Francis. Lovelace & Babbage and the creation of the 1843'notes'. *IEEE Annals of the History of Computing*, 25(4):16–26, 2003. URL: https://ieeexplore.ieee.org/document/1253887, doi:10.1109/MAHC.2003.1253887.

[FPQ21] Christophe Fouqueré, Jean-Jacques Pinto, and Myriam Quatrini. In-coherences in dialogues and their formalization focus on dialogues with schizophrenic individuals. In (In) coherence of Discourse, pages 91–115. Springer, 2021. URL: https://sorbonne-paris-nord.hal.science/hal-03660353/, doi:10.1007/978-3-030-71434-5_5.

[FR94] Arnaud Fleury and Christian Retoré. The mix rule. *Mathematical Structures in Computer Science*, 4(2):273–285, 1994. doi:10.1017/S0960129500000451.
[Fre82] Gottlob Frege. Ueber die wissenschaftliche Berechtigung einer Begriffschrift. *Zeitschrift für philosophie und philosophische Kritik: vormals Fichte-Ulricische Zeitschrift*, 81:48, 1882.

[Fri75] Harvey Friedman. Some systems of second order arithmetic and their use. In *Proceedings of the international congress of mathematicians (Vancouver, BC, 1974)*, volume 1, pages 235–242, 1975.

[Fri76] Harvey M. Friedman. Systems on second order arithmetic with restricted induction I, II. *J. Symb. Logic*, 41:557–559, 1976.

[Fro00] Bertram Fronhöfer. Proof structures and matrix graphs. *Intellectics and Computational Logic: Papers in Honor of Wolfgang Bibel*, pages 159–173, 2000. doi:10.1007/978-94-015-9383-0_10.

[FY19] Yosuke Fukuda and Akira Yoshimizu. A linear-logical reconstruction of intuitionistic modal logic S4. *ArXiv*, 2019. URL: https://arxiv.org/abs/1904.10605, doi:10.48550/arXiv.1904.10605.

[GAL92a] Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. The geometry of optimal lambda reduction. In *Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 15–26, 1992. URL: https://dl.acm.org/doi/abs/10.1145/143165.143172, doi:10.1145/143165.143172.

[GAL92b] Georges Gonthier, Martín Abadi, and Jean-Jacques Lévy. Linear logic without boxes. In [*1992*] *Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science*, pages 223–234, 1992. doi:10.1109/LICS.1992.185535.

[Gan13] Jonardon Ganeri. The philosophy of the Hindus: On the Nyāya and Vaiśesika systems (1824). In *Indian Logic*, pages 34–66. Routledge, 2013.

[Gel08] Michael Gelfond. Answer sets. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, *Handbook of Knowledge Representation*, volume 3 of *Foundations of Artificial Intelligence*, pages 285–316. Elsevier, 2008. URL: https://www.sciencedirect.com/science/article/pii/S1574652607030076, doi:https://doi.org/10.1016/S1574-6526(07)03007-6.

[Gen35a] Gerhard Gentzen. Untersuchungen über das logische Schließen. I. *Mathematische zeitschrift*, 39(1):176–210, 1935.

[Gen35b] Gerhard Gentzen. Untersuchungen über das logische Schließen. II. *Mathematische Zeitschrift*, 39(1):405–431, 1935. doi:10.1007/BF01201363.

[GG07] Alessio Guglielmi and Tom Gundersen. Normalisation control in deep inference via atomic flows. *ArXiv*, 2007. URL: https://arxiv.org/abs/0709.1205, doi:10.48550/arXiv.0709.1205.
[Gim09] Stéphane Gimenez. *Programmer, calculer et raisonner avec les réseaux de la logique linéaire*. PhD thesis, Université Paris-Diderot-Paris VII, 2009. URL: https://theses.hal.science/tel-00629013/.

[Gir87a] Jean-Yves Girard. Linear logic. *Theoretical computer science*, 50(1):1-101, 1987. URL: https://www.sciencedirect.com/science/article/pii/0304397587900454, doi:10.1016/0304-3975(87)90045-4.

[Gir87b] Jean-Yves Girard. Multiplicatives. In G. Lolli, editor, *Logic and Computer Science: New Trends and Applications*, pages 11-34. Rosenberg & Sellier, 1987.

[Gir88] Jean-Yves Girard. Normal functors, power series and λ-calculus. *Annals of Pure and Applied Logic*, 37(2):129-177, 1988. URL: https://www.sciencedirect.com/science/article/pii/0168007288900255, doi: https://doi.org/10.1016/0168-0072(88)90025-5.

[Gir89a] Jean-Yves Girard. Geometry of interaction I: interpretation of system F. In *Studies in Logic and the Foundations of Mathematics*, volume 127, pages 221-260. Elsevier, 1989. URL: https://www.sciencedirect.com/science/article/abs/pii/S0049237X08702714, doi:10.1016/S0049-237X(08)70271-4.

[Gir89b] Jean-Yves Girard. Towards a geometry of interaction. *Contemporary Mathematics*, 92(69-108):6, 1989.

[Gir91] Jean-Yves Girard. Quantifiers in linear logic II. *Nuovi problemi della logica e della filosofia della scienza*, 2:1, 1991.

[Gir95] Jean-Yves Girard. Geometry of interaction III: Accommodating the additives. In *Proceedings of the Workshop on Advances in Linear Logic*, page 329-389, USA, 1995. Cambridge University Press. URL: https://girard.perso.math.cnrs.fr/GOI3.pdf.

[Gir96] Jean-Yves Girard. *Proof-nets: the parallel syntax for proof-theory*, chapter 4, pages 95-123. Routledge, 1996. URL: https://girard.perso.math.cnrs.fr/Proofnets.pdf.

[Gir98] Jean-Yves Girard. Light linear logic. *Information and Computation*, 143(2):175-204, 1998. URL: https://www.sciencedirect.com/science/article/pii/S0890540198927006, doi: https://doi.org/10.1006/inco.1998.2700.

[Gir99] Jean-Yves Girard. On the meaning of logical rules I: syntax versus semantics. In *Computational logic*, pages 215-272. Springer, 1999. URL: https://girard.perso.math.cnrs.fr/meaning1.pdf, doi:10.1007/978-3-642-58622-4_7.
[Gir00] Jean-Yves Girard. On the meaning of logical rules II: multiplicatives and additives. *NATO ASI Series F Computer and Systems Sciences*, 175:183–212, 2000. URL: https://girard.perso.math.cnrs.fr/meaning2.pdf.

[Gir01] Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. *Mathematical structures in computer science*, 11(3):301, 2001. doi:10.1017/S096012950100336X.

[Gir06] Jean-Yves Girard. Geometry of interaction IV: the feedback equation. In Viggo Stoltenberg-Hansen and JoukoEditors Väänänen, editors, *Logic Colloquium '03, Lecture Notes in Logic*, page 76–117. Cambridge University Press, 2006. doi:10.1017/9781316755785.006.

[Gir07] Jean-Yves Girard. Truth, modality and intersubjectivity. *Mathematical structures in computer science*, 17(6):1153–1167, 2007. doi:10.1017/S0960129507006342.

[Gir11a] Jean-Yves Girard. *The Blind Spot: lectures on logic*. European Mathematical Society, 2011.

[Gir11b] Jean-Yves Girard. Geometry of interaction V: logic in the hyperfinite factor. *Theoretical Computer Science*, 412(20):1860–1883, 2011. URL: https://www.sciencedirect.com/science/article/pii/S0304397510007073, doi:10.1016/j.tcs.2010.12.016.

[Gir11c] Jean-Yves Girard. La syntaxe transcendantale, manifeste. 2011. URL: https://girard.perso.math.cnrs.fr/syntran.pdf.

[Gir13a] Jean-Yves Girard. Geometry of interaction VI: a blueprint for transcendental syntax. 2013.

[Gir13b] Jean-Yves Girard. Three lightings of logic (invited talk). In *Computer Science Logic 2013 (CSL 2013)*. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2013. URL: https://drops.dagstuhl.de/opus/volltexte/2013/4185/, doi:10.4230/LIPIcs.CSL.2013.11.

[Gir16a] Jean-Yves Girard. *Le fantôme de la transparence*. Éditions Allia Paris, 2016.

[Gir16b] Jean-Yves Girard. Transcendental syntax II: non-deterministic case. 2016. URL: https://girard.perso.math.cnrs.fr/trsy2.pdf.

[Gir17] Jean-Yves Girard. Transcendental syntax I: deterministic case. *Mathematical Structures in Computer Science*, 27(5):827–849, 2017. URL: https://girard.perso.math.cnrs.fr/trsy1.pdf, doi:10.1017/S0960129515000407.

[Gir18a] Jean-Yves Girard. La logique 2.0. 2018. URL: https://girard.perso.math.cnrs.fr/logique2.0.pdf.
[Gir18b] Jean-Yves Girard. Transcendental syntax III: equality. 2018. URL: https://girard.perso.math.cnrs.fr/trsy3.pdf.

[Gir19] Jean-Yves Girard. Un tract anti-système. 2019. URL: https://girard.perso.math.cnrs.fr/systeme.pdf.

[Gir20a] Jean-Yves Girard. *Transcendental Syntax IV: Logic Without Systems*, pages 17–36. Springer International Publishing, Cham, 2020. doi:10.1007/978-3-030-62077-6_2.

[Gir20b] Jean-Yves Girard. Un tract anti-système II: le monstre de Gila. 2020. URL: https://girard.perso.math.cnrs.fr/gila.pdf.

[Göd31] Kurt Gödel. Über formal unentscheidbare sätze der Principia Mathematica und verwandter Systeme I. *Monatshefte für mathematik und physik*, 38(1):173–198, 1931. doi:10.1007/BF01700692.

[Gri89] Timothy G. Griffin. A formulae-as-type notion of control. In *Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 47–58, 1989. URL: https://dl.acm.org/doi/pdf/10.1145/96709.96714, doi:10.1145/96709.96714.

[Gue04] Stefano Guerrini. Proof nets and the lambda-calculus. *Linear logic in computer science*, pages 65–118, 2004. doi:10.1017/CBO9780511550850.003.

[Gug] Alessio Guglielmi. Deep inference and the calculus of structures. URL: https://people.bath.ac.uk/ag248/p/CalcStrPR.pdf.

[Gur12] Yuri Gurevich. What is an algorithm? In *SOFSEM 2012: Theory and Practice of Computer Science: 38th Conference on Current Trends in Theory and Practice of Computer Science, Spindleruv Mlyn, Czech Republic, January 21-27, 2012. Proceedings 38*, pages 31–42. Springer, 2012. doi:10.1007/978-3-642-27660-6_3.

[GW04] Dov M. Gabbay and John Hayden Woods. *Handbook of the History of Logic*, volume 2009. Elsevier North-Holland, 2004.

[Ham21] Wendy Hammache. *Contrôle du calcul et limites du sens: fonctions, computation et types de G. Frege à A. Church*. PhD thesis, Université Lyon III, 2021. URL: https://scd-resnum.univ-lyon3.fr/out/theses/2021_out_hammache_w.pdf.

[Har09] John Harrison. *Handbook of practical logic and automated reasoning*. Cambridge University Press, 2009. URL: 10.1017/CBO9780511576430.

[Hed04] Shawn Hedman. *A First Course in Logic: An introduction to model theory, proof theory, computability, and complexity*, volume 1. OUP Oxford, 2004. doi:10.1093/oso/9780198529804.001.0001.
[Her30] Jacques Herbrand. *Recherches sur la théorie de la démonstration*. PhD thesis, Université de Paris, 1930. URL: https://eudml.org/doc/192791.

[HH16] Dominic Hughes and Willem Heijltjes. Conflict nets: Efficient locally canonical MALL proof nets. In *2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–10, 2016. URL: https://ieeexplore.ieee.org/document/8576483.

[HM89] Jochen Hager and Martin Moser. An approach to parallel unification using transputers. In *GWAI-89 13th German Workshop on Artificial Intelligence: Eringerfeld, 18.–22. September 1989*, pages 83–91. Springer, 1989. URL: 10.1007/978-3-642-75100-4_10.

[HMOS08] Matthew Hague, Andrzej S. Murawski, C. H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In *2008 23rd Annual IEEE Symposium on Logic in Computer Science*, pages 452–461. IEEE, 2008. URL: https://ieeexplore.ieee.org/document/4557934, doi:10.1109/LICS.2008.34.

[Hor51] Alfred Horn. On sentences which are true of direct unions of algebras. *The Journal of Symbolic Logic*, 16(1):14–21, 1951. URL: https://www.jstor.org/stable/2268661.

[How80] William A. Howard. The formulae-as-types notion of construction. In *HB Curry: essays on combinatory logic, lambda calculus and formalism*, 44:479–490, 1980.

[HR04] Michael Huth and Mark Ryan. *Logic in Computer Science: Modelling and reasoning about systems*. Cambridge university press, 2004.

[HS97] Jaakko Hintikka and Gabriel Sandu. Game-theoretical semantics. In *Handbook of logic and language*, pages 361–410. Elsevier, 1997. URL: https://www.sciencedirect.com/science/article/abs/pii/S9780444817143500096, doi:10.1016/B978-044481714-3/50009-6.

[HS03] Martin Hyland and Andrea Schalk. Glueing and orthogonality for models of linear logic. *Theoretical computer science*, 294(1-2):183–231, 2003. URL: https://www.sciencedirect.com/science/article/pii/S0304397501002419, doi:10.1016/S0304-3975(01)00241-9.

[HS06] Esfandiar Haghverdi and Philip Scott. A categorical model for the geometry of interaction. *Theoretical Computer Science*, 350(2-3):252–274, 2006. URL: https://www.sciencedirect.com/science/article/pii/S0304397505006808, doi:10.1016/j.tcs.2005.10.028.

[HVG03] D. Hughes and R. Van Glabbeek. Proof nets for unit-free multiplicative-additive linear logic (extended abstract). In *18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings.*, pages 1–10,
2003. URL: https://ieeexplore.ieee.org/document/1210039, doi: 10.1109/LICS.2003.1210039.

[iln90] Robin ilner. *Functions as processes*, pages 167–180. Springer Berlin Heidelberg, Berlin, Heidelberg, 1990. doi:10.1007/BFb0032030.

[Imm86] Neil Immerman. Relational queries computable in polynomial time. In *Information and Control*, 68(1):86 – 104, 1986. doi:https://doi.org/10.1016/S0019-9958(86)80029-8.

[Imm12] Neil Immerman. *Descriptive complexity*. Springer Science & Business Media, 2012. doi:10.1007/978-1-4612-0539-5.

[Jae96] Peter Jaenecke. Elementary principles for representing knowledge. *KO KNOWLEDGE ORGANIZATION*, 23(2):88–102, 1996. URL: https://kr.org/proceedings/KR-1991-proceedings-scanned.pdf.

[JM05] Nataša Jonoska and Gregory L. McColm. A computational model for self-assembling flexible tiles. In *International Conference on Unconventional Computation*, pages 142–156. Springer, 2005. doi:10.1007/11560319_14.

[JM06] Nataša Jonoska and Gregory L. McColm. Flexible versus rigid tile assembly. In *International Conference on Unconventional Computation*, pages 139–151. Springer, 2006. URL: https://link.springer.com/chapter/10.1007/11839132_12, doi:10.1007/11839132_12.

[JMS11] Natasha Jonoska, Gregory L. McColm, and Ana Staninska. On stoichiometry for the assembly of flexible tile DNA complexes. *Natural Computing*, 10(3):1121–1141, 2011. doi:10.1007/s11047-009-9169-1.

[Joi93] Jean-Baptiste Joinet. *Etude de la normalisation du calcul des séquents classique à travers la logique linéaire*. PhD thesis, Paris 7, 1993. URL: https://www.theses.fr/1993PA077066.

[JR15] Emmanuel Jeandel and Michael Rao. An aperiodic set of 11 Wang tiles. *ArXiv*, 2015. URL: https://arxiv.org/abs/1506.06492, doi: 10.48550/arXiv.1506.06492.

[JS21] Jean-Baptiste Joinet and Thomas Seiller. From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl's theory of ideal elements. *Kagaku tetsugaku*, 53(2):65–93, 2021. URL: https://hal.science/hal-03128018v1/document.

[KCHM09] Jean-Louis Krivine, Pierre-Louis Curien, Hugo Herbelin, and Paul-André Melliès. Interactive models of computation and program behavior. *Panorama et Synthèses*, 27, 2009.
[Kit91] Hiroaki Kitano. Unification algorithms for massively parallel computers. In *Proceedings of the Second International Workshop on Parsing Technologies*, pages 172–181. IEEE, 1991. URL: https://ieeexplore.ieee.org/document/77189, doi:10.1109/PARBSE.1990.77189.

[KK71] Robert Kowalski and Donald Kuehner. Linear resolution with selection function. *Artificial Intelligence*, 2(3-4):227–260, 1971. URL: https://www.sciencedirect.com/science/article/abs/pii/0004370271900129, doi:10.1016/0004-3702(71)90012-9.

[KKPS82] Norman Kretzmann, Anthony Kenny, Jan Pinborg, and Eleonore Stump. *The Cambridge history of later medieval philosophy: from the rediscovery of Aristotle to the disintegration of scholasticism, 1100-1600*. Cambridge University Press, 1982. doi:10.1017/CHOL9780521226059.

[Knu99] Simo Knuuttila. Medieval theories of modality. 1999. URL: https://plato.stanford.edu/entries/modality-medieval/.

[Koe01] Teun Koetsier. On the prehistory of programmable machines: musical automata, looms, calculators. *Mechanism and Machine theory*, 36(5):589–603, 2001.

[Kow74] Robert Kowalski. Predicate logic as programming language. In *IFIP congress*, volume 74, pages 569–544, 1974. URL: https://www-public.imtbs-tsp.eu/~gibson/Teaching/Teaching-ReadingMaterial/Kowalski74.pdf.

[Kow75] Robert Kowalski. A proof procedure using connection graphs. *J. ACM*, 22(4):572–595, oct 1975. URL: https://dl.acm.org/doi/10.1145/321906.321919, doi:10.1145/321906.321919.

[Laf89] Yves Lafont. Interaction nets. In *Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 95–108. ACM, 1989. URL: https://dl.acm.org/doi/10.1145/96709.96718, doi:10.1145/96709.96718.

[Laf95] Yves Lafont. *From proof nets to interaction nets*, page 225–248. London Mathematical Society Lecture Note Series. Cambridge University Press, 1995. doi:10.1017/CBO9780511629150.012.

[Laf97] Yves Lafont. Interaction combiners. *Information and Computation*, 137(1):69–101, 1997. URL: https://www.sciencedirect.com/science/article/pii/S0890540197926432, doi:10.1006/inco.1997.2643.

[Laf99] Yves Lafont. Linear logic pages. 1999. URL: http://iml.univ-mrs.fr/~lafont/pub/llpages.pdf.
[Laf04] Yves Lafont. Soft linear logic and polynomial time. *Theoretical computer science*, 318(1-2):163-180, 2004. URL: https://www.sciencedirect.com/science/article/pii/S0304397503005231, doi:10.1016/j.tcs.2003.10.018.

[Lam89] John Lamping. An algorithm for optimal lambda calculus reduction. In *Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 16-30, 1989. URL: https://dl.acm.org/doi/pdf/10.1145/96709.96711, doi:10.1145/96709.96711.

[Lau99] Olivier Laurent. Polarized proof-nets: proof-nets for LC. In *International Conference on Typed Lambda Calculi and Applications*, pages 213-227. Springer, 1999. doi:10.1007/3-540-48959-2_16.

[Lau01] Olivier Laurent. A token machine for full geometry of interaction. In *International Conference on Typed Lambda Calculi and Applications*, pages 283-297. Springer, 2001. doi:10.1007/3-540-45413-6_23.

[Lau03] Olivier Laurent. Polarized proof-nets and $\lambda\mu$-calculus. *Theoretical Computer Science*, 290(1):161-188, 2003. URL: https://www.sciencedirect.com/science/article/pii/S0304397501002973, doi:10.1016/S0304-3975(01)00297-3.

[Lec11] Alain Lecomte. *Meaning, logic and ludics*. World Scientific, 2011. doi:10.1142/p670.

[Lei12] Alexander Leitsch. *The resolution calculus*. Springer Science & Business Media, 2012. doi:10.1007/978-3-642-60605-2.

[Lév78] Jean-Jacques Lévy. *Réductions correctes et optimales dans le lambda-calcul*. PhD thesis, Université Paris VII, 1978.

[LJBA01] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In *Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 81-92, 2001. doi:10.1145/360204.360210.

[LLS09] James I. Lathrop, Jack H. Lutz, and Scott M. Summers. Strict self-assembly of discrete Sierpinski triangles. *Theoretical Computer Science*, 410(4-5):384-405, 2009. URL: https://www.sciencedirect.com/science/article/pii/S030439750800724X, doi:10.1016/j.tcs.2008.09.062.

[LM08] Olivier Laurent and Roberto Maieli. Cut elimination for monomial MALL proof nets. In *2008 23rd Annual IEEE Symposium on Logic in Computer Science*, pages 486-497. IEEE, 2008. URL: https://ieeexplore.ieee.org/document/4557937, doi:10.1109/LICS.2008.31.
[LMM88] J-L. Lassez, Michael J. Maher, and Kim Marriott. Unification revisited. In *Foundations of logic and functional programming*, pages 67–113. Springer, 1988. doi:10.1007/3-540-19129-1_4.

[LP11] Giuseppe Longo and Thierry Paul. The mathematics of computing between logic and physics. In *Computability in Context: Computation and Logic in the Real World*, pages 243–273. World Scientific, 2011. doi:10.1142/9781848162778_0007.

[LQ09] Alain Lecomte and Myriam Quatrini. Ludics and its applications to natural language semantics. In *International Workshop on Logic, Language, Information, and Computation*, pages 242–255. Springer, 2009. doi:10.1007/978-3-642-02261-6_20.

[LR03] Olivier Laurent and Laurent Regnier. About translations of classical logic into polarized linear logic. In *18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings.*, pages 11–20. IEEE, 2003. URL: https://ieeexplore.ieee.org/document/1210040, doi:10.1109/LICS.2003.1210040.

[LRM91] Jorge Lobo, Arcot Rajasekar, and Jack Minker. Semantics of horn and disjunctive logic programs. *Theoretical Computer Science*, 86(1):93–106, 1991. URL: https://www.sciencedirect.com/science/article/pii/030439759190006N, doi:10.1016/0304-3975(91)90006-N.

[LS10] Ugo Dal Lago and Ulrich Schöpp. Functional programming in sublinear space. In *European Symposium on Programming*, pages 205–225. Springer, 2010. doi:10.1007/978-3-642-11957-6_12.

[Mar86] Christopher J. Martin. William's machine. *The Journal of Philosophy*, 83(10):564–572, 1986. URL: http://www.jstor.org/stable/2026432, doi:10.2307/2026432.

[Maz17] Damiano Mazza. *Polyadic Approximations in Logic and Computation (Habilitation thesis)*. PhD thesis, Université Paris 13, 2017. URL: https://www.lipn.fr/~mazza/papers/Habilitation.pdf.

[McL08] Colin McLarty. Theology and its discontents: the origin myth of modern mathematics. *wersja April*, 15:2008, 2008.

[Mer15] Lucius Gregory Meredith. Linear types can change the blockchain. *arXiv preprint arXiv:1506.01001*, 2015. URL: https://arxiv.org/abs/1506.01001, doi:10.48550/arXiv.1506.01001.

[Mil95] Dale Miller. A survey of linear logic programming. *Computational Logic: The Newsletter of the European Network of Excellence in Computational Logic*, 2(2):63–67, 1995. URL: https://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ComputNet95/llsurvey.html.
[Mil21] Dale Miller. A survey of the proof-theoretic foundations of logic programming. *Theory and Practice of Logic Programming*, pages 1–46, 2021. URL: https://arxiv.org/abs/2109.01483, doi:10.1017/S1471068421000533.

[Min94] Jack Minker. Overview of disjunctive logic programming. *Annals of Mathematics and Artificial Intelligence*, 12(1-2):1–24, 1994. doi:10.1007/BF01530759.

[Miq09] Alexandre Miquel. De la formalisation des preuves à l'extraction de programmes. *HdR thesis*, Université Paris, 7, 2009.

[Miq17] Étienne Miquey. *Classical realizability and side-effects*. PhD thesis, Université Sorbonne Paris Cité-Université Paris Diderot (Paris 7), 2017. URL: https://www.i2m.univ-amu.fr/perso/etienne.miquey/these/these.pdf.

[MLS84] Per Martin-Löf and Giovanni Sambin. *Intuitionistic type theory*, volume 9. Bibliopolis Naples, 1984.

[MM82] Alberto Martelli and Ugo Montanari. An efficient unification algorithm. *ACM Transactions on Programming Languages and Systems (TOPLAS)*, 4(2):258–282, 1982. URL: https://dl.acm.org/doi/10.1145/357162.357169, doi:10.1145/357162.357169.

[Moo97] Gregory H. Moore. The prehistory of infinitary logic: 1885–1955. In *Structures and Norms in Science*, pages 105–123. Springer, 1997. doi:10.1007/978-94-017-0538-7_7.

[MOTW99] John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. *Theoretical Computer Science*, 228(1-2):175–210, 1999. URL: https://www.sciencedirect.com/science/article/pii/S1571066104000222, doi:10.1016/S1571-0661(04)00022-2.

[Mou88] Guy Mourlevat. *Les machines arithmétiques de Blaise Pascal*, volume 51. Académie des sciences, lettres, arts, 1988.

[MP05] Roberto Maieli and Quintijn Puite. Modularity of proof-nets. *Archive for Mathematical Logic*, 44(2):167–193, 2005. doi:10.1007/s00153-004-0242-2.

[MT03] Harry G. Mairson and Kazushige Terui. On the computational complexity of cut-elimination in linear logic. In *Italian Conference on Theoretical Computer Science*, pages 23–36. Springer, 2003. doi:10.1007/978-3-540-45208-9_4.
[MT15] Damiano Mazza and Kazushige Terui. Parsimonious types and non-uniform computation. In *International Colloquium on Automata, Languages, and Programming*, pages 350–361. Springer, 2015. doi:10.1007/978-3-662-47666-6_28.

[MW17] Pierre-Étienne Meunier and Damien Woods. The non-cooperative tile assembly model is not intrinsically universal or capable of bounded turing machine simulation. In *Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing*, pages 328–341, 2017. URL: https://dl.acm.org/doi/10.1145/3055399.3055446, doi:10.1145/3055399.3055446.

[NGSKDS07] Manh Thang Nguyen, Jürgen Giesl, Peter Schneider-Kamp, and Danny De Schreye. Termination analysis of logic programs based on dependency graphs. In *International Symposium on Logic-based Program Synthesis and Transformation*, pages 8–22. Springer, 2007. doi:10.1007/978-3-540-78769-3_2.

[Ngu21] Lê Thành Dũng Nguyễn. *Towards a resource based approximation theory of programs*. PhD thesis, Université Sorbonne Paris Nord, 2021. URL: https://theses.hal.science/tel-04132636v1/document.

[NS19] Lê Thành Dũng Nguyen and Thomas Seiller. Coherent interaction graphs. *ArXiv*, 2019. URL: https://arxiv.org/abs/1904.06849, doi:10.48550/arXiv.1904.06849.

[Par92] Michel Parigot. $\lambda\mu$-calculus: an algorithmic interpretation of classical natural deduction. In *International Conference on Logic for Programming Artificial Intelligence and Reasoning*, pages 190–201. Springer, 1992. doi:10.1007/BFb0013061.

[Pas97] Blaise Pascal. Machine d'arithmétique. *Modern Logic*, 7(1):56–66, 1997.

[Pat14] Matthew J. Patitz. An introduction to tile-based self-assembly and a survey of recent results. *Natural Computing*, 13(2):195–224, 2014. doi:10.1007/s11047-013-9379-4.

[Pei79] Charles S. Peirce. On junctures and fractures in logic. *Writings of Charles S. Peirce*, 1884:391, 1879. URL: https://www.jstor.org/stable/j.ctt16gz8j1.

[Pen92] Mati Pentus. Equivalent types in Lambek calculus and linear logic. *Mian Prepublication Series*, 1992. URL: https://www.semanticscholar.org/paper/Equivalent-Types-in-Lambek-Calculus-and-Linear-Pentus-Series/c8e6b6789cad6675bc73ac0a98c1014814feb90c.
[Pet08] Charles Petzold. *The annotated Turing: a guided tour through Alan Turing's historic paper on computability and the Turing machine*. Wiley Publishing, 2008.

[Pis15] Paolo Pistone. Rule-following and the limits of formalization: Wittgenstein's considerations through the lens of logic. In *From Logic to Practice*, pages 91–110. Springer, 2015. doi:10.1007/978-3-319-10434-8_6.

[PL09] Thierry Paul and Giuseppe Longo. Le monde et le calcul: réflexions sur calculabilité, mathématiques et physique. In *Logique & Interaction: Géométrie de la cognition, Actes du colloque et école thématique du CNRS*" *Logique, Sciences, Philosophie*" a Cerisy, Hermann, 2009.

[Pos36] Emil L. Post. Finite combinatory processes—formulation 1. *The journal of symbolic logic*, 1(3):103–105, 1936. doi:https://doi.org/10.2307/2269031.

[Pos46] Emil L. Post. A variant of a recursively unsolvable problem. *Bulletin of the American Mathematical Society*, 52(4):264–268, 1946. URL: https://www.ams.org/journals/bull/1946-52-04/S0002-9904-1946-08555-9/S0002-9904-1946-08555-9.pdf, doi:10.1090/S0002-9904-1946-08555-9.

[R+65] John Alan Robinson et al. A machine-oriented logic based on the resolution principle. *Journal of the ACM*, 12(1):23–41, 1965. URL: https://dl.acm.org/doi/10.1145/321250.321253, doi:10.1145/321250.321253.

[Rad62] Tibor Rado. On non-computable functions. *Bell System Technical Journal*, 41(3):877–884, 1962. doi:10.1002/j.1538-7305.1962.tb00480.x.

[Rea02] Stephen Read. Medieval theories: properties of terms. 2002. URL: https://plato.stanford.edu/entries/medieval-terms/.

[Reg92] Laurent Regnier. Lambda-calcul et réseaux. PhD thesis, Université Paris 7, 1992. URL: https://www.theses.fr/1992PA077165.

[Reg94] Laurent Regnier. Une équivalence sur les lambda-termes. *Theoretical Computer Science*, 126(2):281–292, 1994. URL: https://www.sciencedirect.com/science/article/pii/0304397594900124, doi:10.1016/0304-3975(94)90012-4.

[Res64] Nicholas Rescher. Studies in the history of arabic logic. *Revue Philosophique de Louvain*, 76:669–670, 1964. doi:10.2307/2217894.

[Res02] Greg Restall. *An introduction to substructural logics*. Routledge, 2002.

[Res12] Nicholas Rescher. *Temporal modalities in Arabic logic*, volume 2. Springer Science & Business Media, 2012. URL: https://link.springer.com/book/10.1007/978-94-010-3523-1, doi:10.1007/978-94-010-3523-1.
[Rib07] Colin Riba. Strong normalization as safe interaction. In *22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)*, pages 13–22. IEEE, 2007. URL: https://www.computer.org/csdl/proceedings-article/lics/2007/29080013/120mNxWui8x, doi: 10.1109/LICS.2007.46.

[Rie14] Lionel Rieg. *On forcing and classical realizability*. PhD thesis, Ecole normale supérieure de lyon-ENS LYON, 2014. URL: https://theses.hal.science/tel-01061442/PDF/RIEG_Lionel_2014_These.pdf.

[Ros96] Kristoffer H. Rose. *Explicit substitution: tutorial & survey*. Computer Science Department, 1996. doi:https://www.researchgate.net/publication/228386201_Explicit_substitution_tutorial survey.

[Rus03] Bertrand Russell. *The principles of mathematics*. Public Domain, 1903. URL: https://people.umass.edu/klement/pom/.

[Sch31] Arthur Schopenhauer. *Eristische Dialektik: Die Kunst, Recht zu Behalten*. Kein & Aber Verlag, 1831.

[Sch24] Moses Schönfinkel. Über die bausteine der mathematischen Logik. *Mathematische annalen*, 92(3):305–316, 1924. doi:10.1007/BF01448013.

[Sch56] Kurt Schütte. Ein system des verknüpfenden schliessens. *Archiv für mathematische Logik und Grundlagenforschung*, 2(2):55–67, 1956. doi: 10.1007/BF01969991.

[Sch65] Thomas W. Scharle. Axiomatization of propositional calculus with Sheffer functors. *Notre Dame Journal of Formal Logic*, 6(3):209–217, 1965. URL: https://projecteuclid.org/journals/notre-dame-journal-of-formal-logic/volume-6/issue-3/Axiomatization-of-propositional-calculus-with-Sheffer-functors/10.1305/ndjfl/1093958259.full, doi:10.1305/ndjfl/1093958259.

[Sch94] Harold Schellinx. *The noble art of linear decorating*. University of Amsterdam, 1994.

[Sch06] Ulrich Schöpp. Space-efficient computation by interaction. In *International Workshop on Computer Science Logic*, pages 606–621. Springer, 2006. doi:10.1007/11874683_40.

[Sco82] Dana Scott. Domains for denotational semantics. In *International Colloquium on Automata, Languages, and Programming*, pages 577–610. Springer, 1982. URL: https://www.researchgate.net/publication/220897586_Domains_for_Denotational_Semantics, doi:10.1007/BFb0012801.
[See82] Nadrian C. Seeman. Nucleic acid junctions and lattices. *Journal of theoretical biology*, 99(2):237-247, 1982. URL: https://www.sciencedirect.com/science/article/abs/pii/0022519382900029, doi:10.1016/0022-5193(82)90002-9.

[Sei12a] Thomas Seiller. Interaction graphs: multiplicatives. *Annals of Pure and Applied Logic*, 163(12):1808-1837, 2012. URL: https://www.sciencedirect.com/science/article/pii/S0168007212000759, doi: 10.1016/j.apal.2012.04.005.

[Sei12b] Thomas Seiller. *Logique dans le facteur hyperfini: géometrie de l'interaction et complexité*. PhD thesis, Aix-Marseille Université, 2012. URL: https://theses.hal.science/tel-00768403/.

[Sei16a] Thomas Seiller. Interaction graphs: additives. *Annals of Pure and Applied Logic*, 167(2):95-154, 2016. URL: https://www.sciencedirect.com/science/article/pii/S0168007215000998, doi: 10.1016/j.apal.2015.10.001.

[Sei16b] Thomas Seiller. Interaction graphs: Full linear logic. In *2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1-10. IEEE, 2016. URL: https://dl.acm.org/doi/10.1145/2933575.2934568, doi:10.1145/2933575.2934568.

[Sei17] Thomas Seiller. Interaction graphs: Graphings. *Annals of Pure and Applied Logic*, 168(2):278-320, 2017. URL: https://www.sciencedirect.com/science/article/pii/S0168007216301300, doi: 10.1016/j.apal.2016.10.007.

[Sei18] Thomas Seiller. Interaction graphs: Non-deterministic automata. *ACM Transactions on Computational Logic (TOCL)*, 19(3):1-24, 2018. doi: 10.1145/3226594.

[Sei20a] Thomas Seiller. Probabilistic complexity classes through semantics. *ArXiv*, 2020. URL: https://arxiv.org/abs/2002.00009, doi:10.48550/arXiv.2002.00009.

[Sei20b] Thomas Seiller. Zeta functions and the (linear) logic of Markov processes. *ArXiv*, 2020. URL: https://arxiv.org/abs/2001.11906, doi: 10.48550/arXiv.2001.11906.

[Sha38] Claude E. Shannon. A symbolic analysis of relay and switching circuits. *Electrical Engineering*, 57(12):713-723, 1938. doi:10.1109/T-AIEE.1938.5057767.

[Sha84] Ehud Y. Shapiro. Alternation and the computational complexity of logic programs. *The Journal of Logic Programming*, 1(1):19-33, 1984. URL: https://www.sciencedirect.com/science/article/pii/0743106684900219, doi:10.1016/0743-1066(84)90021-9.
[Shi03] Masaru Shirahata. Geometry of interaction explained (algebra, logic and geometry in informatics). 数理解析研究所講究録, 1318:160-187, 2003. URL: https://www.kurims.kyoto-u.ac.jp/~hassei/alg-13/ kokyuroku/19_shirahata.pdf.

[Sib05] Fadi N. Sibai. Parallel unification: Theory and implementations. In *Parallelization in Inference Systems: International Workshop Dagstuhl Castle, Germany, December 17-18, 1990 Proceedings*, pages 51-81. Springer, 2005. doi:https://doi.org/10.1007/3-540-55425-4_3.

[Sic76] Sharon Sickel. A search technique for clause interconnectivity graphs. *IEEE Transactions on Computers*, pages 823-835, 1976. URL: https://ieeexplore.ieee.org/document/1674701, doi:10.1109/TC. 1976.1674701.

[Sim88] Stephen G. Simpson. Partial realizations of Hilbert's program. *The Journal of Symbolic Logic*, 53(2):349-363, 1988. doi:10.2307/2274508.

[Sip06] Michael Sipser. *Introduction to the Theory of Computation* (second edition). Thomsom, 2006.

[Smi13] Peter Smith. *An introduction to Gödel's theorems*. Cambridge University Press, 2013. URL: https://www logicmatters net/resources pdfs/ godelbook GodelBookLM pdf, doi:10.1017/CBO9781139149105.

[Spa02] Paul Vincent Spade. Thoughts, words and things: An introduction to late mediaeval logic and semantic theory. Copyright by Paul Vincent Spade, 10:2009, 2002. URL: http://pvspade.com/Logic/docs/thoughts1_1a.pdf.

[Ste61] J. T. Stevenson. Roundabout the runabout inference-ticket. *Analysis*, 21(6):124-128, 1961. URL: http://www.jstor.org/stable/3326421.

[Str06] Lutz Straßburger. Proof nets and the identity of proofs. *ArXiv*, 2006. URL: https://arxiv.org/abs/cs/0610123, doi:10.48550/arXiv.cs/ 0610123.

[SU06] Morten Heine Sørensen and Pawel Urzyczyn. *Lectures on the Curry-Howard isomorphism*. Elsevier, 2006.

[Tai81] William W. Tait. Finitism. *The Journal of Philosophy*, 78(9):524-546, 1981. doi:10.2307/2026089.

[Tär77] Sten-Åke Tärnlund. Horn clause computability. *BIT Numerical Mathematics*, 17(2):215-226, 1977. doi:10.1007/BF01932293.

[Ten79] Neil Tennant. La barre de Scheffer dans la logique des séquents et des syllogismes. *Logique et Analyse*, 22(88):505-514, 1979. URL: http:// www.jstor.org/stable/44085164.
[Ter04] Kazushige Terui. Proof nets and boolean circuits. In *Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004.*, pages 182–191. IEEE, 2004. URL: https://ieeexplore.ieee.org/document/1319612, doi:10.1109/LICS.2004.1319612.

[Ter11] Kazushige Terui. Computational ludics. *Theoretical Computer Science*, 412(20):2048–2071, 2011. URL: https://www.sciencedirect.com/science/article/pii/S0304397510007176, doi:10.1016/j.tcs.2010.12.026.

[TGBB95] Alan Mathison Turing, Jean-Yves Girard, Julien Basch, and Patrice Blanchard. *La machine de Turing*. Editions du seuil, 1995.

[Tho91] Wolfgang Thomas. On logics, tilings, and automata. In *International Colloquium on Automata, Languages, and Programming*, pages 441–454. Springer, 1991. doi:10.1007/3-540-54233-7_154.

[Tur36] Alan Mathison Turing. On computable numbers, with an application to the Entscheidungsproblem. *J. of Math*, 58(345-363):5, 1936. doi:10.1112/plms/s2-42.1.230.

[Vää19] Jouko Väänänen. Second-order and higher-order logic. 2019. URL: https://plato.stanford.edu/entries/logic-higher-order/.

[VS84] Jeffrey Scott Vitter and Roger A. Simons. Parallel algorithms for unification and other complete problems in P. In *Proceedings of the 1984 Annual Conference of the ACM on The Fifth Generation Challenge*, ACM '84, page 75–84, New York, NY, USA, 1984. Association for Computing Machinery. doi:10.1145/800171.809607.

[Wad90] Philip Wadler. Linear types can change the world! In *Programming concepts and methods*, volume 3, page 5, 1990. URL: https://wwwsemanticscholar.org/paper/Linear-Types-can-Change-the-World!-Wadler/24c850390fba27fc6f3241cb34ce7bc6f3765627.

[Wad03] Philip Wadler. Call-by-value is dual to call-by-name. *SIGPLAN Not.*, 38(9):189–201, aug 2003. doi:10.1145/944746.944723.

[Wad12] Philip Wadler. Propositions as sessions. *ACM SIGPLAN Notices*, 47(9):273–286, 2012. doi:10.1145/2398856.2364568.

[Wan57] Hao Wang. A variant to Turing's theory of computing machines. *Journal of the ACM (JACM)*, 4(1):63–92, 1957. URL: https://dl.acm.org/doi/pdf/10.1145/320856.320867, doi:10.1145/320856.320867.

[WGRO93] Anna Wierzbicka, Richard A. Geiger, and Brygida Rudzka-Ostyn. The alphabet of human thoughts. *Conceptualizations and Mental Processing in Language*, 3:23, 1993. doi:10.1515/9783110857108.23.
[Win98] Erik Winfree. *Algorithmic self-assembly of DNA*. PhD thesis, California Institute of Technology, 1998. URL: https://thesis.library.caltech.edu/1866/.

[Wit10] Ludwig Wittgenstein. *Philosophical investigations*. John Wiley & Sons, 2010.

[Woo15] Damien Woods. Intrinsic universality and the computational power of self-assembly. *Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences*, 373(2046):20140214, 2015. URL: https://royalsocietypublishing.org/doi/10.1098/rsta.2014.0214, doi:10.1098/rsta.2014.0214.