related to the Curry-Howard correspondence between proofs and programs [@curry1934functionality; @howard1980formulae]. While Curry-Howard traditionally assimilates terms in the $\lambda$-calculus with proofs in intuitionnistic logic, stellar resolution terms – named constellations – will be assimilated with (generalisations of) proofs in linear logic.

Linear Logic was introduced by Girard [@girard1987linear] as a refinement of intuitionnistic logic inspired from semantics of $\lambda$-calculus [@girard1988normal]. Soon after the introduction of linear logic, the *geometry of interaction* programme emerged [@girard1989towards], aiming at defining semantics of proofs and programs accounting for the dynamics of the cut-elimination procedure. This *dynamic semantics* approach, a major inspiration behind game semantics [@hyland2000full; @abramsky2000full], distinguishes itself from denotational semantics in which cut-elimination is represented as equality.

However, the geometry of interaction ambition went beyond the dynamic semantics aspects. It also aimed to reconstruct logic – in particular linear logic – from what could be understood as an untyped model of computation by using realisability techniques. In some way, the idea is the same as the reconstruction of simple types from pure $\lambda$-calculus. In $\lambda$-calculus, one defines an orthogonality relation between terms $t$ and contexts $E(\cdot)$ by letting $t\perp E(\cdot)\Leftrightarrow E(t) \text{ is strongly normalising}$. A type $A$ is then defined as a 