Substructural Parametricity

Aberlé, C. B.; Crary, Karl; Martens, Chris; Pfenning, Frank

doi:10.4230/LIPIcs.FSCD.2025.4

Substructural Parametricity

C. B. Aberlé

Carnegie Mellon University, Pittsburgh, PA, USA Karl Crary

Carnegie Mellon University, Pittsburgh, PA, USA Chris Martens

Northeastern University, Boston, MA, USA Frank Pfenning

Carnegie Mellon University, Pittsburgh, PA, USA

Abstract

Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary logical relations that allow us to prove consequences of parametricity for a range of substructural type systems. A key idea is to parameterize the relation by an algebra, which we exemplify with a monoid and commutative monoid to interpret ordered and linear type systems, respectively. We prove the fundamental theorem of logical relations and apply it to deduce extensional properties of inhabitants of certain types. Examples include demonstrating that the ordered types for list append and reversal are inhabited by exactly one function, as are types of some tree traversals. Similarly, the linear type of the identity function on lists is inhabited only by permutations of the input. Our most advanced example shows that the ordered type of the list fold function is inhabited only by the fold function.

Keywords and phrases:

Substructural type systems, logical relations, ordered logic

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type structures

Acknowledgements:

The authors thank Bob Atkey and Stephanie Balzer for helpful comments regarding related work.

Funding:

This material is based upon work supported by the United States Air Force Office of Scientific Research under grant number A210038S002 (Tristan Nguyen, program manager). Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.

DOI:

10.4230/LIPIcs.FSCD.2025.4

Event:

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Editors:

Maribel Fernández

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Substructural type systems and parametric polymorphism are two mechanisms for capturing precise behavioral properties of programs at the type level, enabling powerful static reasoning. The goal of this paper is to give a theoretical account of these mechanisms in combination.

Substructural type systems have been investigated since the advent of linear logic, starting with the seminal paper by Girard and Lafont [18]. Among other applications, with substructural type systems one can avoid garbage collection, update memory in place [27, 28], make message-passing [16, 12] or shared memory concurrency [17, 35] safe, model quantum computation [15], or reason efficiently about imperative programs [26]. Substructural type systems have thus been incorporated into languages that seek to offer such guarantees, such as Rust, Koka, Haskell, Oxidized OCaml, and ProtoQuipper.

Parametricity, originally introduced for System F [42], enables the idea that programs whose types involve universal quantification over type parameters have certain strong semantic properties. This idea supports powerful program reasoning principles such as representation independence across abstraction boundaries [30] and “theorems for free” that can be derived about all inhabitants of certain types, for example that every inhabitant of $\forall{\alpha}.\;\alpha\to\alpha$ is equivalent to the identity function [46].

The theory of substructural logics and type systems is now relatively well understood, including several ways to integrate substructural and structural type systems [9, 38, 19]. It is therefore somewhat surprising that we do not yet know much about how parametricity and its applications interact with them. The main foray into substructural parametricity is a paper by Zhao et al. [47] that accounts for a polymorphic dual-intuitionistic linear logic. They point out that logical relations on closed terms are problematic because substitution obscures linearity. Their solution was to construct a logical relation on open terms, necessitating the introduction of “semantic typing” judgments that mirror the syntactic type system, which complicates their definition and application.

In this paper, we follow an approach using constructive resource semantics in the style of Reed et al. [39, 41, 40] to construct logical relations on closed terms. We start with an ordered type system [37, 36, 24], which may be considered the least permissive among substructural type systems and therefore admits a pleasantly minimal definition. However, the construction is generic with respect to certain properties of the resource algebra, which allows us to extend it also to linear and unrestricted types. Consequences of our development include that certain polymorphic types are only inhabited by the polymorphic append and reverse functions on lists. Similarly, certain types are only inhabited by functions that swap or maintain the order of pairs. The most advanced application shows that the ordered type of fold over lists is inhabited only by the fold function.

We conjecture that the three substructural modes we investigate – ordered, linear, and unrestricted – can also be combined in an adjoint framework [9, 19] but leave this to future work. Similarly, we simplify our presentation by defining only a unary logical relation since it is sufficient to demonstrate proof-of-concept, but nothing stands in the way of a more general definition (for example, to support representation-independence results).

2 A Minimalist Fragment

We start with a small fragment of the Lambek Calculus [25, 29], extended with parametric polymorphism [43]. This fragment is sufficient to illustrate the main ideas behind our constructions. For the sake of simplicity we choose a Curry-style formulation of typing, concentrating on properties of untyped terms rather than intrinsically typed terms. This allows the same terms to inhabit ordered, linear, and unrestricted types and thereby focus on semantic rather than syntactic issues.

\begin{array}[]{llcll}\mbox{Types}&A,B&::=&\alpha\mid\mathbf{1}\mid A\bullet B% \mid A\rightarrowtail B\mid A\twoheadrightarrow B\mid\forall\alpha.\,A\\ \mbox{Terms}&e&::=&x\\ &&\mid&()\mid\mathbf{match}\;e\;(()\Rightarrow e^{\prime})&(\mathbf{1})\\ &&\mid&(e_{1},e_{2})\mid\mathbf{match}\;e\;((x,y)\Rightarrow e^{\prime})&(A% \bullet B)\\ &&\mid&\lambda x.\ e\mid e_{1}\,e_{2}&(A\rightarrowtail B,A\twoheadrightarrow B% )\end{array}

In this fragment, we have $A\bullet B$ (read “ $A$ fuse $B$ ”) which, logically, is a noncommutative conjunction. We have two forms of implication: $A\rightarrowtail B$ (read: “ $A$ under $B$ ”, originally written as $A\mathbin{\backslash}B$ ) which is true if from the hypothesis $A$ placed at the left end of the antecedents we can deduce $B$ , and $A\twoheadrightarrow B$ (read: “ $B$ over $A$ ”, originally written as $B\mathbin{/}A$ ) which is true if from the hypothesis $A$ placed at the right end of the antecedents we can prove $B$ . Lambek’s original notation was suitable for the sequent calculus and its applications in linguistics, but is less readable for natural deduction and functional programming.

Our basic typing judgment has the form $\Delta\mid\Omega\vdash e:A$ where $\Delta$ consists of hypotheses $\alpha\;\mathsf{type}$ , and $\Omega$ is an ordered context $(x_{1}:A_{1})\ldots(x_{n}:A_{n})$ . We make the standard presuppositions that $\Delta\vdash A\;\mathsf{type}$ and $\Delta\vdash A_{i}\;\mathsf{type}$ for every $x_{i}:A_{i}$ in $\Omega$ , and that both type variables and term variables are pairwise distinct. The rules are show in Figure 1.

Figure 1: Ordered Natural Deduction.

Here are a few example judgments that hold or fail. We elide the context $\Delta=$ $(\alpha\,\mathsf{type},\beta\,\mathsf{type},\gamma\,\mathsf{type})$ .

\begin{array}[]{lcll}&\vdash&\lambda x.\,x:\alpha\rightarrowtail\alpha\\ &\vdash&\lambda x.\,x:\alpha\twoheadrightarrow\alpha\\ &\not\vdash&\lambda x.\,\lambda y.\,x:\alpha\twoheadrightarrow(\beta% \twoheadrightarrow\alpha)&(\mbox{no weakening})\\ &\not\vdash&\lambda x.\,(x,x):\alpha\twoheadrightarrow(\alpha\bullet\alpha)&(% \mbox{no contraction})\\ &\vdash&\lambda x.\,\lambda y.\,(x,y):\alpha\twoheadrightarrow(\beta% \twoheadrightarrow(\alpha\bullet\beta))\\ &\not\vdash&\lambda x.\,\lambda y.\,(x,y):\alpha\rightarrowtail(\beta% \rightarrowtail(\alpha\bullet\beta))&(\mbox{no exchange})\\[4.30554pt] f:\beta\twoheadrightarrow(\alpha\rightarrowtail\gamma)&\vdash&\lambda x.\,% \lambda y.\,(f\,y)\,x:\alpha\rightarrowtail(\beta\twoheadrightarrow\gamma)&(% \mbox{``associativity''})\\ g:\alpha\rightarrowtail(\beta\twoheadrightarrow\gamma)&\vdash&\lambda y.\,% \lambda x.\,(g\,x)\,y:\beta\twoheadrightarrow(\alpha\rightarrowtail\gamma)\\[4% .30554pt] g:(\alpha\bullet\beta)\twoheadrightarrow\gamma&\vdash&\lambda x.\,\lambda y.\,% g\,(x,y):\alpha\twoheadrightarrow(\beta\twoheadrightarrow\gamma)&(\mbox{% currying})\\ f:\alpha\twoheadrightarrow(\beta\twoheadrightarrow\gamma)&\vdash&\lambda p.\,% \mathbf{match}\;p\;((x,y)\Rightarrow f\,x\,y):(\alpha\bullet\beta)% \twoheadrightarrow\gamma&(\mbox{uncurrying})\end{array}

The strictures of the typing judgment imply that certain types may be uninhabited, or may be inhabited by terms that are extensionally equivalent (i.e., that yield the same outputs for all closed inputs) to a small number of possibilities. To count the number of linear functions, translate $(A\twoheadrightarrow B)^{\mathchoice{\mathsf{L}}{\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}{\scriptscriptstyle\mathsf{L}}}=(A\rightarrowtail B% )^{\mathchoice{\mathsf{L}}{\mathsf{L}}{\scriptscriptstyle\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}}=A^{\mathchoice{\mathsf{L}}{\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}{\scriptscriptstyle\mathsf{L}}}\multimap B^{% \mathchoice{\mathsf{L}}{\mathsf{L}}{\scriptscriptstyle\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}}$ and $(A\bullet B)^{\mathchoice{\mathsf{L}}{\mathsf{L}}{\scriptscriptstyle\mathsf{L}% }{\scriptscriptstyle\mathsf{L}}}=A^{\mathchoice{\mathsf{L}}{\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}{\scriptscriptstyle\mathsf{L}}}\otimes B^{% \mathchoice{\mathsf{L}}{\mathsf{L}}{\scriptscriptstyle\mathsf{L}}{% \scriptscriptstyle\mathsf{L}}}$ and similarly for unrestricted functions.

Types	Ordered	Linear	Unrestricted
$\alpha\twoheadrightarrow\alpha$	1	1	1
$\alpha\twoheadrightarrow(\alpha\twoheadrightarrow\alpha)$	0	0	2
$\alpha\twoheadrightarrow(\alpha\twoheadrightarrow(\alpha\bullet\alpha))$	1	2	4
$\alpha\twoheadrightarrow(\alpha\rightarrowtail(\alpha\bullet\alpha))$	1	2	4
$\alpha\twoheadrightarrow(\beta\twoheadrightarrow(\beta\bullet\alpha))$	0	1	1
$\alpha\twoheadrightarrow(\beta\twoheadrightarrow(\alpha\bullet\beta))$	1	1	1

Because our intended application language based on adjoint natural deduction [19] is call-by-value, we can give a straightforward big-step operational semantics [22] relating a term to its final value. Because this evaluation does not directly interact with or benefit from substructural properties, we show it without further comment in Figure 2. It has the property of preservation that if $\cdot\vdash e:A$ and $e\mathrel{\hookrightarrow}v$ then $\cdot\vdash v:A$ . Jang et al. give an account [19] that exploits linearity and other substructural properties, although not the lack of exchange.

Figure 2: Big-Step Operational Semantics.

3 An Algebraic Logical Predicate

Because of our particular setting, we define two mutually dependent logical predicates: $\llbracket A\rrbracket$ for closed terms and $[A]$ for closed values. In addition, the relation is parameterized by elements from an algebraic domain which may have various properties. For the ordered case, it should be a monoid, for the linear case a commutative monoid. However, the rules themselves do not require this for the pure sets of terms. We use $m\cdot n$ for the binary operation on the monoid, and $\epsilon$ for its unit.

Ignoring polymorphism for now, we write $m\Vdash e\in\llbracket A\rrbracket$ and $m\Vdash v\in[A]$ , which is defined by

\begin{array}[]{lcl}m\Vdash e\in\llbracket A\rrbracket&\Longleftrightarrow&% \exists v.\,e\mathrel{\hookrightarrow}v\land m\Vdash v\in[A]\\[10.00002pt] m\Vdash v\in[\mathbf{1}]&\Longleftrightarrow&m=\epsilon\land v=(\,)\\ m\Vdash v\in[A\bullet B]&\Longleftrightarrow&\hskip-5.0pt\begin{array}[t]{l}% \exists m_{1},m_{2}.\;m=m_{1}\cdot m_{2}\land v=(v_{1},v_{2})\\ \quad\land\leavevmode\nobreak\ m_{1}\Vdash v_{1}\in[A]\land m_{2}\Vdash v_{2}% \in[B]\end{array}\\ m\Vdash v\in[A\twoheadrightarrow B]&\Longleftrightarrow&\forall k.\,k\Vdash w% \in[A]\Longrightarrow m\cdot k\Vdash v\,w\in\llbracket B\rrbracket\\ m\Vdash v\in[A\rightarrowtail B]&\Longleftrightarrow&\forall k.\,k\Vdash w\in[% A]\Longrightarrow k\cdot m\Vdash v\,w\in\llbracket B\rrbracket\end{array}

We can see how the algebraic structure of the monoid tracks information about order if its operation is not commutative.

The key step, as usual in logical predicates of this nature, is the case for universal quantification and type variables. We map type variables $\alpha$ to relations $R_{B}$ between monoid elements and values in $[B]$ where $B$ is a closed type. We use $S$ to denote this mapping from type variables to sets of values and write it as a superscript on $\Vdash$ .

\begin{array}[]{lcl}m\Vdash^{S}v\in[\alpha]&\Longleftrightarrow&m\mathrel{S(% \alpha)}v\\ m\Vdash^{S}v\in[\forall\alpha.\,A(\alpha)]&\Longleftrightarrow&\forall B,R_{B}% .\,m\Vdash^{S,\alpha\mapsto R_{B}}v\in[A(\alpha)]\end{array}

The mapping $S$ is just passed through identically in the cases of the relation defined above.

We can already verify some interesting properties. As a first example we show that the logical predicates are nonempty.

Example 1.

\epsilon\Vdash\lambda x.\,\lambda y.\,(x,y)\in\llbracket\forall\alpha.\,\alpha% \twoheadrightarrow(\alpha\twoheadrightarrow(\alpha\bullet\alpha))\rrbracket

Proof.

Because the $\lambda$ -term is a value, we need to check

\epsilon\Vdash\lambda x.\,\lambda y.\,(x,y)\in[\forall\alpha.\,\alpha% \twoheadrightarrow(\alpha\twoheadrightarrow(\alpha\bullet\alpha))]

By definition, this is true if for an arbitrary $A$ and relation $m\mathrel{R_{A}}v$ we have

\epsilon\Vdash^{\alpha\mapsto R_{A}}\lambda x.\,\lambda y.\,(x,y)\in[\alpha% \twoheadrightarrow(\alpha\twoheadrightarrow(\alpha\bullet\alpha))]

Using the definition of the logical predicate for right implication twice and one intermediate step of evaluation, this holds iff

m\cdot k\Vdash^{\alpha\mapsto R_{A}}(\lambda y.\,(v,y))\;w\in\llbracket\alpha% \bullet\alpha\rrbracket

for all $m, k$ with $m\Vdash^{\alpha\mapsto R_{A}}v$ and $k\Vdash^{\alpha\mapsto R_{A}}w$ . By evaluation, this is true iff

m\cdot k\Vdash^{\alpha\mapsto R_{A}}(v,w)\in[\alpha\bullet\alpha]

Now we can apply the definition of $[A\bullet B]$ , splitting $m\cdot k$ into $m$ and $k$ and reducing it to

m\Vdash^{\alpha\mapsto R_{A}}v\in[\alpha]\land k\Vdash^{\alpha\mapsto R_{A}}w% \in[\alpha]

Both of these hold because, by assumption, $m\mathrel{R_{A}}v$ and $k\mathrel{R_{A}}w$ . $\hfill\blacktriangleleft$

More interesting, perhaps, is the reverse.

Example 2.

If

\epsilon\Vdash e\in\llbracket\forall\alpha.\,\alpha\twoheadrightarrow(\alpha% \twoheadrightarrow(\alpha\bullet\alpha))\rrbracket

then $e$ is extensionally equal to $\lambda x.\,\lambda y.\,(x,y)$ , in that for any closed type $A$ and closed terms $v, w : A$ , it must be the case that $e\,v\,w\hookrightarrow(v,w)$ . In particular, it can not be $\lambda x.\,\lambda y.\,(y,x)$ .

Proof.

We choose our monoid to be the free monoid over two generators $a$ and $b$ and we choose an arbitrary closed type $A$ and two elements $v$ and $w$ . Moreoever, we pick $R_{A}$ relating only $a\mathrel{R_{A}}v$ and $b\mathrel{R_{A}}w$ .

From the definitions (and skipping over some simple properties regarding evaluation), we obtain

a\cdot b\Vdash^{\alpha\mapsto R_{A}}e\;v\;w\in\llbracket\alpha\bullet\alpha\rrbracket

By the clauses for $\llbracket\alpha\bullet\alpha\rrbracket$ , $[\alpha\bullet\alpha]$ and $\alpha$ we conclude that

e\;v\;w\mathrel{\hookrightarrow}(u_{1},u_{2})

for some values $u_{1}$ and $u_{2}$ with $a\mathrel{R_{A}}u_{1}$ and $b\mathrel{R_{A}}u_{2}$ . Because the only value related to $a$ is $v$ and the only value related to $b$ is $w$ , we conclude $u_{1}=v$ and $u_{2}=w$ . Therefore

e\;v\;w\mathrel{\hookrightarrow}(v,w)

Since $v$ and $w$ were chosen arbitrarily, we see that $e$ is extensionally equal to $\lambda x.\,\lambda y.\,(x,y)$ . $\hfill\blacktriangleleft$

4 The Fundamental Theorem

The fundamental theorem of logical predicates states that every well-typed term is in the predicate. Our relations also include terms that are not well-typed, which can occasionally be useful when one exceeds the limits of static typing.

We need a few standard lemmas, adapted to this case. We only spell out one.

Lemma 3 (Compositionality).

Define $R_{A}$ such that $k\mathrel{R_{A}}w$ iff $k\Vdash w\in[A]$ . Then $m\Vdash^{S,\alpha\mapsto R_{A}}v\in[B(\alpha)]$ iff $m\Vdash^{S}v\in[B(A)]$

Proof.

By induction on $B(\alpha)$ . $\hfill\blacktriangleleft$

We would like to prove the fundamental theorem by induction over the structure of the typing derivation. Since our logical relation is defined for closed terms, we need a closing substitution $\eta$ , i.e., a substitution of closed terms into the typing context of the term $e$ for which we seek to prove the fundamental theorem by induction, such that the application $\eta(e)$ of $\eta$ to $e$ is a closed term. We therefore extend the definition of the logical relation to substitutions and contexts as follows:

\begin{array}[]{lcl}m\Vdash^{S}(x\mapsto v)\in[x:A]&\Longleftrightarrow&m% \Vdash^{S}v\in[A]\\ m\Vdash^{S}(\eta_{1}\,\eta_{2})\in[\Omega_{1}\,\Omega_{2}]&\Longleftrightarrow% &\exists m_{1},m_{2}.\,m=m_{1}\cdot m_{2}\land m_{1}\Vdash^{S}\eta_{1}\in[% \Omega_{1}]\land m_{2}\Vdash^{S}\eta_{2}\in[\Omega_{2}]\\ m\Vdash^{S}(\cdot)\in[\cdot]&\Longleftrightarrow&m=\epsilon\end{array}

Due to the associativity of the monoid operation and concatenation of contexts, this constitutes a valid definition.

Theorem 4 (Fundamental Theorem (purely ordered)).

Assume $\Delta\mid\Omega\vdash e:A$ , a mapping $S$ with domain $\Delta$ , and closing substitution $m\Vdash^{S}\eta\in[\Omega]$ . Then $m\Vdash^{S}\eta(e)\in\llbracket A\rrbracket$ .

Proof.

By induction on the structure of the given typing derivation. We show a few cases.

Case:

Then $m\Vdash^{S}\eta(x)\in[A]$ by assumption and definition, and $m\Vdash^{S}\eta(x)\in\llbracket A\rrbracket$ since $\eta(x)$ is a value.

Case:

m\Vdash^{S}\eta\in[\Omega]

Given

k\Vdash^{S}v\in[A]

Assumption (1)

k\Vdash^{S}(x\mapsto v)\in[x:A]

By definition

m\cdot k\Vdash^{S}(\eta,x\mapsto v)\in[\Omega\,(x:A)]

By definition

m\cdot k\Vdash^{S}(\eta,x\mapsto v)(e)\in\llbracket B\rrbracket

By ind. hyp.

m\cdot k\Vdash^{S}(\eta(\lambda x.\,e))\,v\in\llbracket B\rrbracket

By reverse evaluation,

v

closed

m\Vdash^{S}\eta(\lambda x.\,e)\in[A\twoheadrightarrow B]

By definition, discharging (1)

m\Vdash^{S}\eta(\lambda x.\,e)\in\llbracket A\twoheadrightarrow B\rrbracket

By definition

Case:

m\Vdash^{S}\eta\in[\Omega\,\Omega_{A}]

Given

m_{1}\Vdash^{S}\eta_{1}\in[\Omega]

and

m_{2}\Vdash^{S}\eta_{2}\in[\Omega_{A}]

for some

m_{1}

,

m_{2}

,

\eta_{1}

, and

\eta_{2}

with

m=m_{1}\cdot m_{2}

and

\eta=\eta_{1}\;\eta_{2}

By definition

m_{1}\Vdash^{S}\eta_{1}(e_{1})\in\llbracket A\twoheadrightarrow B\rrbracket

By ind. hyp.

m_{2}\Vdash^{S}\eta_{2}(e_{2})\in\llbracket A\rrbracket

By ind. hyp.

\eta_{1}(e_{1})\mathrel{\hookrightarrow}v_{1}

with

m_{1}\Vdash^{S}v_{1}\in[A\twoheadrightarrow B]

By definition

\eta_{2}(e_{2})\mathrel{\hookrightarrow}v_{2}

with

m_{2}\Vdash^{S}v_{2}\in[A]

By definition

m_{1}\cdot m_{2}\Vdash^{S}v_{1}\,v_{2}\in\llbracket B\rrbracket

By definition

(\eta_{1}\,\eta_{2})(e_{1}\,e_{2})=(\eta_{1}(e_{1}))\,(\eta_{2}(e_{2}))

By properties of substitution

m\Vdash^{S}\eta(e_{1}\,e_{2})\in\llbracket B\rrbracket

Since

m=m_{1}\cdot m_{2}

and

\eta=(\eta_{1}\,\eta_{2})

Case:

m\Vdash^{S}\eta\in[\Omega]

Given

R_{B}

an arbitrary relation

k\mathrel{R_{B}}v

Assumption (1)

m\Vdash^{S,\alpha\mapsto R_{B}}\eta\in[\Omega]

Since

\alpha

fresh

m\Vdash^{S,\alpha\mapsto R_{B}}\eta(e)\in\llbracket A\rrbracket

By ind. hyp.

m\Vdash^{S}\eta(e)\in\llbracket\forall\alpha.\,A\rrbracket

By definition, discharging (1)

Case:

m\Vdash^{S}\eta\in[\Omega]

Given

m\Vdash^{S}\eta(e)\in\llbracket\forall\alpha.\,A(\alpha)\rrbracket

By ind. hyp.

Define

k\mathrel{R}_{B}v

iff

k\Vdash^{S}v\in[B]

m\Vdash^{S,\alpha\mapsto R_{B}}\eta(e)\in\llbracket A(\alpha)\rrbracket

By definition

m\Vdash^{S,\alpha\mapsto R_{B}}v\in[A(\alpha)]

for

\eta(e)\mathrel{\hookrightarrow}v

By definition

m\Vdash^{S}v\in[A(B)]

By compositionality (Lemma 4)

m\Vdash^{S}\eta(e)\in\llbracket A(B)\rrbracket

By definition

$\hfill\blacktriangleleft$

Because typing implies that the logical predicate holds, the earlier examples now apply to well-typed terms.

Theorem 5 (Section 3 revisited).

If

\cdot\vdash e:\forall\alpha.\,\alpha\twoheadrightarrow(\alpha% \twoheadrightarrow(\alpha\bullet\alpha))

then $e$ is extensionally equivalent to $\lambda x.\,\lambda y.\,(x,y)$ .

Proof.

We just note that

\epsilon\Vdash e\in\llbracket\forall\alpha.\,\alpha\twoheadrightarrow(\alpha% \twoheadrightarrow(\alpha\bullet\alpha))\rrbracket

since $(\cdot)\in[\cdot]$ and $(\cdot)e=e$ and the empty mapping $S$ suffices without any free type variables. Then we appeal to the reasoning in Section 3. $\hfill\blacktriangleleft$

5 Unrestricted Functions

We are interested in properties of functions such as list append or list reversal, or higher-order functions such as fold. This requires inductive types, but the functions on them are not used linearly. For example, append has a recursive call in the case of a nonempty list, but none in the case of an empty list. We could introduce a general modality ${!}A$ for this purpose. A simpler alternative that is sufficient for our situation is to introduce unrestricted function types $A\mathbin{\rightarrow}B$ (usually coded as ${!}A\multimap B$ in linear logic or ${!}A\twoheadrightarrow B$ in ordered logic). This path has been explored previously [37] with different motivations. There, an open logical relation was defined on the negative monomorphic fragment in order to show the existence of canonical forms, a property that is largely independent of ordered typing.

Adding unrestricted functions is rather straightforward in typing by using two kinds of variables: those that are ordered and those unrestricted. Then, in the logical predicate, unrestricted variables must not use any resources, that is, they are assigned the unit element $\epsilon$ of the monoid during the definition.

The generalized judgment has the form $\Delta\mid\Gamma\mathrel{;}\Omega\vdash e:A$ where $\Gamma$ contains type assignments for variables that can be used in an unrestricted (not linear and not ordered) way. All the previous rules are augmented by propagating $\Gamma$ from the conclusion to all premises. Because our term language is untyped, no extensions are needed there. Similarly, the rules of our dynamics do not need to change.

Figure 3: Unrestricted functions.

We extend the logical predicate using arguments not afforded any resources.

The fundamental theorem extends in a straightforward way.

Theorem 6 (Fundamental Theorem (mixed ordered/unrestricted)).

Assume $\Delta\mid\Gamma\mathrel{;}\Omega\vdash e:A$ , a mapping $S$ with domain $\Delta$ , and two closing substitutions $\epsilon\Vdash^{S}\theta\in[\Gamma]$ and $m\Vdash^{S}\eta\in[\Omega]$ . Then $m\Vdash^{S}(\theta\mathrel{;}\eta)(e)\in\llbracket A\rrbracket$ .

Proof.

By induction on the structure of the given typing derivation. $\hfill\blacktriangleleft$

An interesting side effect of these definitions is that if we omit ordered functions but retain pairs we obtain the “usual” formulation of closed logical predicates, including certain consequences of parametricity for the ordinary $\lambda$ -calculus.

Theorem 7.

If

\cdot\vdash e:\forall\alpha.\,\alpha\mathbin{\rightarrow}(\alpha\mathbin{% \rightarrow}(\alpha\bullet\alpha))

then $e$ is extensionally equivalent to one of 4 functions: $\lambda x.\,\lambda y.\,(x,y)$ , $\lambda x.\,\lambda y.\,(y,x)$ , $\lambda x.\,\lambda y.\,(x,x)$ , or $\lambda x.\,\lambda y.\,(y,y)$ .

Proof.

By the fundamental theorem, we have

\epsilon\Vdash e\in\llbracket\forall\alpha.\,\alpha\mathbin{\rightarrow}(% \alpha\mathbin{\rightarrow}(\alpha\bullet\alpha))\rrbracket

We use this for an abitrary closed type $A$ with two arbitary values $v$ , and $w$ and relation $R_{A}$ with $\epsilon\mathrel{R_{A}}v$ and $\epsilon\mathrel{R_{A}}w$ . Exploiting the definition, we get

\epsilon\Vdash^{\alpha\mapsto R_{A}}e\in\llbracket\alpha\mathbin{\rightarrow}(% \alpha\mathbin{\rightarrow}(\alpha\bullet\alpha))\rrbracket

Using the definition of function twice and skipping over some evaluation and reverse evaluation, we obtain

\epsilon\Vdash^{\alpha\mapsto R_{A}}e\,v\,w\in\llbracket\alpha\bullet\alpha\rrbracket

This means that $e\,v\,w\mathrel{\hookrightarrow}(u_{1},u_{2})$ with $\epsilon\mathrel{R_{A}}u_{1}$ and $\epsilon\mathrel{R_{A}}u_{2}$ . Because of the definition of $R_{A}$ there are 4 possibilities for $(u_{1},u_{2})$ , namely $(v,w)$ , $(w,v)$ , $(v,v)$ and $(w,w)$ . This in turn means $e$ is extensionally equal to one of the 4 functions shown. $\hfill\blacktriangleleft$

6 Sums, Twist, and Recursive Types

At this point, we are at a crossroads. Because we would like to prove theorems regarding more complex data structures such as lists, trees, or streams, we could extend the development with general inductive and coinductive types and their recursors. We conjecture that this is possible and leave it to future work. The other path is to work with purely positive types, including recursive ones whose values can be directly observed. In this approach, the definition of the logical predicate is quite easy to extend. It becomes a nested inductive definition: either the type becomes smaller or, once we encounter a purely positive type and recursion is possible, from then on the terms become strictly smaller. In this paper we take the latter approach, which excludes coinductive types such as streams from consideration, but still yields many interesting and intuitive consequences.

We take the opportunity to also round out our language with sums and twist (the symmetric counterpart of fuse). We use a signature defining equirecursive type names that may be arbitrarily mutually recursive. Because such type definitions are otherwise closed, they constitute metavariables in the sense of contextual modal type theory [31]. Each type definition $F[\Delta]=A^{+}$ (for $\Delta$ a context of type variables as in previous sections) must be contractive, that is, its definiens cannot be be another type name. Moreover, $A^{+}$ must be purely positive, which is interpreted inductively.

\begin{array}[]{llcll}\mbox{Types}&A&::=&\ldots\mid A\mathbin{\circ}B\mid% \oplus\{\ell:A_{\ell}\}_{\ell\in L}\\ \mbox{Purely Positive Types}&A^{+},B^{+}&::=&A^{+}\bullet B^{+}\mid A^{+}% \mathbin{\circ}B^{+}\mid\mathbf{1}\mid\oplus\{\ell:A_{\ell}^{+}\}_{\ell\in L}% \mid F[\theta]\\ \mbox{Type Definitions}&\Sigma&::=&F[\Delta]=A^{+}\mid(\cdot)\mid\Sigma_{1},% \Sigma_{2}\\ \mbox{Type Substitutions}&\theta&::=&\alpha\mapsto A^{+}\mid(\cdot)\mid\theta_% {1}\,\theta_{2}\\[10.00002pt] \end{array}

The language of terms does not change much because type names are equirecursive.

\begin{array}[]{llcll}\mbox{Term}&e&::=&\ldots\\ &&\mid&k(e)\mid\mathbf{match}\;e\;\{\ell(x_{\ell})\Rightarrow e^{\prime}\}_{% \ell\in L}&(\oplus\{\ell:A_{\ell}\})\end{array}

We add the type $A\mathbin{\circ}B$ (“twist”), symmetric to $A\bullet B$ , since encoding it as $B\bullet A$ requires rewriting terms, flipping the order of pairs. For $A\mathbin{\circ}B$ it is merely the typechecking that changes. This allows more types to be assigned to the same term. We allow silent unfolding of type definitions, so there are no explicit rules for $F[\theta]$ .

Figure 4: Ordered Natural Deduction, Extended.

Figure 5: Big-Step Operational Semantics, Extended.

The logical predicate is also extended in a straightforward manner. We assume the signature $\Sigma$ is fixed and therefore do not carry it explicitly through the definitions.

\begin{array}[]{lcl}m\Vdash^{S}v\in[A\mathbin{\circ}B]&\Longleftrightarrow&% \exists m_{1},m_{2}.\;m=m_{2}\cdot m_{1}\land v=(v_{1},v_{2})\\ &&\hbox{}\land m_{1}\Vdash^{S}v_{1}\in[A]\land m_{2}\Vdash^{S}v_{2}\in[B]\\ m\Vdash^{S}k(v)\in[{\oplus}\{\ell:A_{\ell}\}_{\ell\in L}]&\Longleftrightarrow&% m\Vdash^{S}v\in[A_{k}]\land k\in L\\ m\Vdash^{S}v\in[F[\theta]]&\Longleftrightarrow&m\Vdash^{S}v\in\theta(A^{+})\ % \mbox{where $F[\Delta]=A^{+}\in\Sigma$}\end{array}

Because we have equirecursive type definitions, the last clause is usually applied silently. The definition of the logical predicate is no longer straightforwardly inductive on the structure of the type. However, we see that for purely positive types (the only ones involved in recursion), the value in the definition becomes strictly smaller in each clause if type definitions are contractive. In other words, we now have a nested inductive definition of the logical predicate, first on the type, and when the type is purely positive, on the structure of the value.

We can also add recursion to our term language with the key proviso that we either restrict ourselves to certain patterns of recursion (for example, primitive recursion), or termination is guaranteed by other external means (for example, an analysis using sized types [2]). This assumption allows us to maintain the structure of the logical predicate, even if it is no longer a means to prove termination (which we are not interested in for this paper).

Lemma 8 (Compositionality (including purely positive equirecursive types)).

Define $R_{A}$ such that $k\mathrel{R_{A}}w$ iff $k\Vdash w\in[A]$ . Then $m\Vdash^{S,\alpha\mapsto R_{A}}v\in[B(\alpha)]$ iff $m\Vdash^{S}v\in[B(A)]$ .

Proof.

By nested induction on the definition of the logical predicate for $B(\alpha)$ , first on the structure of $B$ and second on the structure of the value when a purely positive type $F[\theta]$ has been reached. $\hfill\blacktriangleleft$

Theorem 9 (Fundamental Theorem (including purely positive recursive types)).

Assume $\Delta\mid\Gamma\mathrel{;}\Omega\vdash e:A$ , a mapping $S$ with domain $\Delta$ , and two closing substitutions $\epsilon\Vdash^{S}\theta\in[\Gamma]$ and $m\Vdash^{S}\eta\in[\Omega]$ . Then $m\Vdash^{S}(\theta\mathrel{;}\eta)(e)\in\llbracket A\rrbracket$ .

Proof.

By induction on the structure of the given typing derivation. When reasoning about functions and recursion, we need the assumption of termination. $\hfill\blacktriangleleft$

7 Free Theorems for Ordered Lists

We start with some theorems about ordered lists, not unlike those analyzed by Wadler [46], but much sharper due to substructural typing. We define two versions of ordered lists, one that is ordered left-to-right and one that is ordered right-to-left. Both of these use exactly the same representation; just their typing is different.

\mathit{llist}\;\alpha={\oplus}\{\underline{\mathsf{nil}}:\mathbf{1},% \underline{\mathsf{cons}}:\alpha\bullet\mathit{llist}\;\alpha\}

\mathit{rlist}\;\alpha={\oplus}\{\underline{\mathsf{nil}}:\mathbf{1},% \underline{\mathsf{cons}}:\alpha\mathbin{\circ}\mathit{rlist}\;\alpha\}

The following will be a useful lemma about ordered lists.

Lemma 10 (Ordered Lists).

\begin{array}[]{lcl}m\Vdash^{S}v\in[\mathit{llist}\;\alpha]&% \Longleftrightarrow&m=\epsilon\land v=\underline{\mathsf{nil}}\,(\,)\\ &&\hbox{}\lor\exists m_{1},m_{2}.\,m=m_{1}\cdot m_{2}\land v=\underline{% \mathsf{cons}}\;(v_{1},v_{2})\\ &&\quad\hbox{}\land m_{1}\mathrel{S(\alpha)}v_{1}\land m_{2}\Vdash v_{2}\in[% \mathit{llist}\;\alpha]\\[10.00002pt] m\Vdash^{S}v\in[\mathit{rlist}\;\alpha]&\Longleftrightarrow&m=\epsilon\land v=% \underline{\mathsf{nil}}\,(\,)\\ &&\hbox{}\lor\exists m_{1},m_{2}.\,m=m_{2}\cdot m_{1}\land v=\underline{% \mathsf{cons}}\;(v_{1},v_{2})\\ &&\quad\hbox{}\land m_{1}\mathrel{S(\alpha)}v_{1}\land m_{2}\Vdash v_{2}\in[% \mathit{rlist}\;\alpha]\end{array}

Proof.

By unrolling the definitions of the logical predicate and the equirecursive nature of the definition of lists. $\hfill\blacktriangleleft$

For the applications, we abbreviate lists, writing $[v_{1},\ldots,v_{n}]$ for $\underline{\mathsf{cons}}(v_{1},\ldots,$ $\underline{\mathsf{cons}}(v_{n},\underline{\mathsf{nil}}\,(\,)))$ .

\begin{array}[]{l}m\Vdash^{\alpha\mapsto R_{A}}v\in[\mathit{llist}\;\alpha]% \Longleftrightarrow m=m_{1}\cdots m_{n},v=[v_{1},\ldots,v_{n}]\ \mbox{where}\ % m_{i}\mathrel{R_{A}}v_{i}\ \mbox{(for some $m_{i},v_{i}$)}\\[9.24994pt] m\Vdash^{\alpha\mapsto R_{A}}v\in[\mathit{rlist}\;\alpha]\Longleftrightarrow m% =m_{n}\cdots m_{1},v=[v_{1},\ldots,v_{n}]\ \mbox{where}\ m_{i}\mathrel{R_{A}}v% _{i}\ \mbox{(for some $m_{i},v_{i}$)}\end{array}

Now we state a first property of lists that follows as a consequence of our parameterized logical predicate.

Theorem 11.

If $\cdot\vdash f:\forall\alpha.\,\mathit{llist}\;\alpha\twoheadrightarrow\mathit{% llist}\;\alpha$ then $f$ is extensionally equal to the identity function on lists.

Proof.

By the fundamental theorem, we have

\epsilon\Vdash f\in[\forall\alpha.\,\mathit{llist}\;\alpha\twoheadrightarrow% \mathit{llist}\;\alpha]

To construct a relation $R_{A}$ we pick an arbitary closed type $A$ . For the monoid, we pick the one freely generated by $a_{1},a_{2},\ldots$ and define

m\mathrel{R_{A}}v\Longleftrightarrow m=a_{i}\land v=v_{i}

for arbitrary elements $v_{i}$ . By definition, we obtain, for $S=\alpha\mapsto R_{A}$ ,

\epsilon\Vdash^{S}f\in[\mathit{llist}\;\alpha\twoheadrightarrow\mathit{llist}% \;\alpha]

Again by definition, that’s the case iff

\forall m,v.\,m\Vdash^{S}v\in[\mathit{llist}\;\alpha]\Longrightarrow\epsilon% \cdot m\Vdash^{S}f\,v\in\llbracket\mathit{llist}\;\alpha\rrbracket

Here, $\epsilon\cdot m=m$ , by the monoid laws. Therefore $f\,v\mathrel{\hookrightarrow}w$ and

\forall m,v.\,m\Vdash^{S}v\in[\mathit{llist}\;\alpha]\Longrightarrow m\Vdash^{% S}w\in[\mathit{llist}\;\alpha]

We use this for $m=a_{1}\cdots a_{n}$ and $v=[v_{1},\ldots,v_{n}]$ . By our lemma about lists and the arbitrary nature of $A$ and $v_{i}$ we conclude that $w=v$ . $\hfill\blacktriangleleft$

By similar reasoning we can obtain the following properties.

Theorem 12.

1.

If $f:\forall\alpha.\mathit{rlist}\;\alpha\twoheadrightarrow\mathit{rlist}\;\alpha$ then $f$ is extensionally equal to the identity function.
2.

If $f:\forall\alpha.\mathit{rlist}\;\alpha\twoheadrightarrow\mathit{llist}\;\alpha$ then $f$ is extensionally equal to the list reversal function.
3.

If $f:\forall\alpha.\mathit{llist}\;\alpha\twoheadrightarrow\mathit{rlist}\;\alpha$ then $f$ is extensionally equal to the list reversal function.

Proof.

By very similar reasoning to the one in Theorem 11. $\hfill\blacktriangleleft$

But can we deduce properties of higher-order functions using ordered parametricity? We show one primary example; others such as $\mathit{map}$ follow directly from it or similarly.

Unlike the usual or even linear parametricity, the type of $\mathit{fold}$ in ordered natural deduction guarantees that it must be the fold function! (The essential difference being that in, say, linear natural deduction, a function having the same type as $\mathit{fold}$ may still apply a permutation to its argument before performing the fold.) Note that the combining function and initial element are unrestricted arguments (one is called for every list element, and one is called only for the empty list), but that the combining function’s arguments are ordered.

Theorem 13.

If

\cdot\vdash f:\forall\alpha.\,\forall\beta.\,(\alpha\bullet\beta% \twoheadrightarrow\beta)\mathbin{\rightarrow}\beta\mathbin{\rightarrow}\mathit% {llist}\;\alpha\twoheadrightarrow\beta

then $f$ extensionally equal to the fold function, that is,

f\;g\;b\;[v_{1},v_{2},\ldots,v_{n}]=g(v_{1},g(v_{2},\ldots,g(v_{n},b)))

Proof.

We use the free monoid over constructors $a_{1},a_{2},\ldots$ . Furthermore, given a type $A$ with arbitrary elements $v_{i}$ we define the relation $R_{A}$ by

m\mathrel{R_{A}}v\Longleftrightarrow m=a_{i}\land v=v_{i}\ \mbox{for some $i$}

Since the type involves another quantified type $\beta$ , we need to define a second relation $R_{B}$ where

m\mathrel{R_{B}}d\Longleftrightarrow m=a_{i_{1}}\cdots a_{i_{k}}\land d=g(v_{i% _{1}},g(v_{i_{2}},\ldots,g(v_{i_{k}},b)))

With these relations and the definition on of the logical predicate we get the following two properties.

1.

$\forall m_{1},m_{2},v,d.\,m_{1}\mathrel{R_{A}}v\land m_{2}\mathrel{R_{B}}d% \Longrightarrow m_{1}\cdot m_{2}\mathrel{R_{B}}g(v,d)$
2.

$\epsilon\mathrel{R_{B}}g$

Since

a_{1}\cdots a_{n}\Vdash^{\alpha\mapsto R_{A}}[v_{1},\ldots,v_{n}]\in[\mathit{% llist}\;\alpha]

we can use the second and iterate the first property to conclude that

a_{1}\cdots a_{n}\mathrel{R_{B}}w\qquad\mbox{for $f\;g\;b\;[v_{1},\ldots,v_{n}% ]\mathrel{\hookrightarrow}w$}

By definition of $R_{B}$ , this yields

f\;g\;b\;[v_{1},\ldots,v_{n}]=g(v_{1},\ldots g(v_{n},b))

in the sense that both sides evaluate to $w$ . Because functions and values were chosen arbitrarily, this expresses the desired extensional equality. $\hfill\blacktriangleleft$

8 Free Theorems Regarding Trees

Consider

\mathit{lxrtree}\;\alpha={\oplus}\{\underline{\mathsf{leaf}}:\mathbf{1},% \underline{\mathsf{cons}}:\mathit{lxrtree}\;\alpha\bullet\alpha\bullet\mathit{% lxrtree}\;\alpha\}

\mathit{xlrtree}\;\alpha={\oplus}\{\underline{\mathsf{leaf}}:\mathbf{1},% \underline{\mathsf{cons}}:(\mathit{xlrtree}\;\alpha\mathbin{\circ}\alpha)% \bullet\mathit{xlrtree}\;\alpha\}

\mathit{lrxtree}\;\alpha={\oplus}\{\underline{\mathsf{leaf}}:\mathbf{1},% \underline{\mathsf{cons}}:\mathit{lrxtree}\;\alpha\bullet(\alpha\mathbin{\circ% }\mathit{xlrtree}\;\alpha)\}

Here are a few free theorems regarding such trees. Further variations exist.

Theorem 14.

1.

If $f:\forall\alpha.\,\mathit{lxrtree}\;\alpha\twoheadrightarrow\mathit{llist}\;\alpha$ then $f\;t$ lists the elements of $t$ following an inorder traversal.
2.

If $f:\forall\alpha.\,\mathit{xlrtree}\;\alpha\twoheadrightarrow\mathit{llist}\;\alpha$ then $f\;t$ lists the elements of $t$ following a preorder traversal.
3.

If $f:\forall\alpha.\,\mathit{lrxtree}\;\alpha\twoheadrightarrow\mathit{llist}\;\alpha$ then $f\;t$ lists the elements of $t$ following a postorder traversal.

Proof.

Trees, like lists, are purely positive types. As such, we can prove an analogue of Section 7. We only show one of them, writing $t$ for tree values.

\begin{array}[]{lcl}m\Vdash^{S}t\in[\mathit{lxrtree}\;\alpha]&% \Longleftrightarrow&m=\epsilon\land t=\underline{\mathsf{leaf}}(\,)\\ &&\hbox{}\lor\exists m_{1},k,m_{2}.\,m=m_{1}\cdot k\cdot m_{2}\land v=% \underline{\mathsf{node}}(t_{1},v,t_{2})\\ &&\quad\hbox{}\land m_{1}\Vdash^{S}t_{1}\in[\mathit{lxrtree}\;\alpha]\land k% \mathrel{S(\alpha)}v\land m_{2}\Vdash^{S}t_{2}\in[\mathit{lxrtree}\;\alpha]% \end{array}

$\hfill\blacktriangleleft$

9 From Ordered to Linear Types

Exploring parametricity for linear types instead of ordered ones is now a rather straightforward change. We conflate the left and right implication into a single implication, and similarly for conjunction.

\begin{array}[]{lll|l}\mbox{ordered}&\mbox{linear}&\mbox{structural}&\mbox{% values}\\ \hline\cr B\twoheadrightarrow A&&\\ &A\multimap B&A\mathbin{\rightarrow}B&\lambda x.\,e\\ A\rightarrowtail B&&\\ \hline\cr A\bullet B&&\\ &A\otimes B&A\times B&(v_{1},v_{2})\\ A\mathbin{\circ}B&&\\ \hline\cr\mathbf{1}&\mathbf{1}&\mathbf{1}&(\,)\\ {\oplus}\{\ell:A_{\ell}\}&{\oplus}\{\ell:A_{\ell}\}&{\oplus}\{\ell:A_{\ell}\}&% \ell(v)\end{array}

We see that in the transition from the linear to the structural case, no further connectives collapse. That’s because we would still distinguish eager pairs ( $A\times B$ ) from lazy records that we have elided from our development since they do not introduce any fundamentally new ideas.

From the point of view of typing, the easiest change is to just permit the silent rule of exchange

The more typical change is to replace context concatenation $\Omega_{L}\,\Omega_{R}$ with context merge $\Omega_{L}\bowtie\Omega_{R}$ which allows arbitrary interleavings of the hypotheses.

Our definition of the logical predicates remains that same, except that we assume that the algebraic structure parameterizing our definitions is a commutative monoid. This immediately validates the rules of exchange and the fundamental theorem goes through as before.

The results of exploiting the fundamental theorem to obtain parametricity results are no longer as sharp. For example:

Theorem 15.

If $\cdot\vdash e:\forall\alpha.\,\alpha\multimap\alpha\multimap\alpha\otimes\alpha$ then $f$ is extensionally equal to $\lambda x.\,\lambda y.\,(x,y)$ or $\lambda x.\,\lambda y.\,(y,x)$ .

Proof.

By the fundamental theorem, we have

\epsilon\Vdash e\in\llbracket\forall\alpha.\,\alpha\multimap\alpha\multimap% \alpha\otimes\alpha\rrbracket

Therefore $e\mathrel{\hookrightarrow}f$ and

\epsilon\Vdash f\in[\forall\alpha.\,\alpha\multimap\alpha\multimap\alpha% \otimes\alpha]

We use a free commutative monoid with two generators, $a$ and $b$ , arbitrary values $v$ and $w$ such that $a\mathrel{R}v$ and $b\mathrel{R}w$ . By the fundamental theorem:

\epsilon\Vdash^{\alpha\mapsto R}f\in[\alpha\multimap\alpha\multimap\alpha% \otimes\alpha]

Applying this function to $v$ and $w$ , we obtain that $f\,v\,w\mathrel{\hookrightarrow}p$ and

a\cdot b\Vdash^{\alpha\mapsto R}p\in[\alpha\otimes\alpha]

This is true, again by definition, if for some $m$ and $k$ and $p_{1}$ and $p_{2}$ we have

m\cdot k=a\cdot b\land p=(p_{1},p_{2})\land m\Vdash^{\alpha\mapsto R}p_{1}\in[% \alpha]\land k\Vdash^{\alpha\mapsto R}p_{2}\in[\alpha]

Further applying definitions, we get that for some $m$ , $k$ , $p_{1}$ , and $p_{2}$ , we have

m\cdot k=a\cdot b\land m\mathrel{R}p_{1}\land k\mathrel{R}p_{2}

There are 4 ways that $a\cdot b$ could be decomposed into $m\cdot k$ , but the definition of $R$ leaves only two possibilities: $m=a$ , $k=b$ , $p_{1}=v$ and $p_{2}=w$ or $m=b$ , $k=a$ , $p_{1}=w$ and $p_{2}=v$ . Summarizing: either

e\,v\,w\mathrel{\hookrightarrow}(v,w)

or

e\,v\,w\mathrel{\hookrightarrow}(w,v)

which expresses that $e$ is extensionally equal to $\lambda x.\,\lambda y.\,(x,y)$ or $\lambda x.\,\lambda y.\,(y,x)$ . $\hfill\blacktriangleleft$

Theorem 16.

If $\cdot\vdash e:\forall\alpha.\mathit{list}\,\alpha\multimap\mathit{list}\,\alpha$ then $e$ is extensionally equal to a permutation of the list elements.

Proof.

As in the proof of the related ordered theorem, we apply the fundamental theorem and then the definition for arbitrary values $v_{i}$ with $a_{i}\mathrel{R}v_{i}$ where $\alpha\mapsto R$ , and the commutative monoid is freely generated from $a_{1},a_{2},\ldots$ .

Taking analogous steps to the ordered case, we conclude that $a_{1}\cdots a_{n}=m_{1}\cdots m_{n}$ modulo commutativity (and associativity, as always) where each $m_{i}$ is a unique $a_{j}$ . $\hfill\blacktriangleleft$

In the unrestricted case where various algebraic elements are fixed to be $\epsilon$ , we can only obtain that every element of the output list must be a member of the input list, because those elements are in $\epsilon\mathrel{R}v_{i}$ . We do not write out the details of this straightforward adaptation of foregoing proofs.

10 Related Work

The most directly related work is Zhao et al.’s [47] open logical relation for parametricity for a dual intuitionistic-linear polymorphic lambda calculus. In this work, they define an open logical relation that includes an analog of typing contexts in the semantic model. While our development follows a similar structure, our resource algebraic account allows us to eliminate spurious typechecking premises in definitions and permits a more flexible range of substructural type systems.

Ahmed, Fluet, and Morrisett [4] introduce a logical relation for substructural state via step-indexing, followed by [5] a linear language with locations (L3) defined by a Kripke-style logical relation to account for a language with mutable storage. However, the underlying languages in these developments do not support parametric polymorphism. Ahmed, Dreyer, and Rossberg later provide a logical relations account of a System F-based language supporting imperative state update, and they demonstrate representation independence results for this system [3]. The languages modeled in this body of work represent a specific point in the design space with respect to imperative state update and references, as opposed to our more general schema for substructural types in a functional setting. However, Kripke-style logical relations that model a store as a partial commutative monoid have some parallels to our development, and drawing out a more precise relationship between these systems represents an interesting path of future work.

There are a few developments that start from different settings but develop semantics with similar properties. Pérez et al. develop logical relations for linear session types [33, 34] to establish normalization results, but there is no account of parametricity. Caires et al. [11], Derakhshan et al. [13], and Balzer et al. [8] account for parametricity in linear session-typed communication with the goal of reasoning abstractly over protocol implementations. Their logical relations do not directly capture resource usage nor obviously admit free theorems similar to ours, but rather form a basis for information flow reasoning as an orthogonal application of parametricity [14, 44].

The Iris system for program reasoning via higher-order separation logic incorporates a semantic model initially based on monoids [21], which is later extended to more general resource algebras [20]. Their parameterization over resource algebras seems to work similarly to ours, but towards the goal of program verification rather than type-based reasoning. Birkedal et al. [10] demonstrate free theorems for separation logic specifications in service of enforcing communication protocols between clients and libraries.

The use of “resource semantics” more generally to account for the semantics of substructural logics extends at least to Kamide [23] and the logic of bunched implications [32], and similar ideas have recently gained traction in the context of graded modal type systems [45]. For instance, Atkey and Wood [6] introduce a notion of “context constrained computation” to generalize parametricity reasoning over linear list operations to arbitrary semiring-graded modalities. They do not directly account for polymorphism in the type system, but can instantiate their calculus with example-specific world definitions to prove e.g. that a linear function on lists of a generic key type must return a permutation. Abel and Bernardy [1] extend this idea to a similar one that includes polymorphic types and presents free theorems. The ringoid structure that generalizes the graded approach does not, however, accommodate ordered logic.

11 Conclusion

We have provided an account of substructural parametricity including ordered, linear, and unrestricted disciplines. The fewer structural properties are supported, the more precise the characterization of a function’s behavior from its type. We have also implemented an ordered type checker using a bidirectional type system with so-called additive contexts [7], but the details are beyond the scope of this paper. Suffice it to say that all the functions such as append, reverse, tree traversals, and fold can actually be implemented in a variety of ways and our “free theorems” are therefore not vacuous.

The most immediate item of future work is to support general inductive and coinductive types instead of purely positive recursive types. This would allow a new class of applications, including (productive) stream processing and object-oriented program patterns.

We also envision an adjoint combination of different substructural type systems [19], extended to include exchange among the explicit structural rules, with the logical predicates given herein properly extended to account for the different modalities present in the adjoint type system.

References

[1] Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages, 4(ICFP):1–28, 2020. doi:10.1145/3408972.
[2] Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26:e2, 2016. doi:10.1017/S0956796816000022.
[3] Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In 36th Symposium on Principles of Programming Languages (POPL 2009), pages 340–353, Savannah, Georgia, USA, January 2009. ACM. doi:10.1145/1480881.1480925.
[4] Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In 10th International Conference on Functional Programming (ICFP 2005), pages 78–91, 2005. doi:10.1145/1086365.1086376.
[5] Amal Ahmed, Matthew Fluet, and Greg Morrisett. L³: a linear language with locations. Fundamenta Informaticae, 77(4):397–449, 2007.
[6] Bob Atkey and James Wood. Context constrained computation. In 3rd Workshop on Type-Driven Development (TyDe’18), 2018.
[7] Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, 33rd Conference on Logic in Computer Science (LICS 2018), pages 56–65, Oxford, UK, July 2018. ACM. doi:10.1145/3209108.3209189.
[8] Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. arXiv preprint arXiv:2309.00192, 2023. doi:10.48550/arXiv.2309.00192.
[9] P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Leszek Pacholski and Jerzy Tiuryn, editors, Selected Papers from the 8th International Workshop on Computer Science Logic (CSL’94), pages 121–135, Kazimierz, Poland, September 1994. Springer LNCS 933. An extended version appears as Technical Report UCAM-CL-TR-352, University of Cambridge.
[10] Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages, 5(ICFP):1–29, 2021. doi:10.1145/3473586.
[11] Luís Caires, Jorge A Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In 22nd European Symposium on Programming (ESOP 2013), pages 330–349, Rome, Italy, March 2013. Springer LNCS 7792. doi:10.1007/978-3-642-37036-6_19.
[12] Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In P.Gastin and F.Laroussinie, editors, 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222–236, Paris, France, August 2010. Springer LNCS 6269. doi:10.1007/978-3-642-15375-4_16.
[13] Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual Symposium on Logic in Computer Science (LICS 2021), pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470654.
[14] Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading policies for flexible information flow control in session-typed concurrency (artifact). Dagstuhl Artifacts Series, 10(2):4–1, 2024.
[15] Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In 35th Symposium on Logic in Computer Science (LICS 2020), pages 440–453, Saarbrücken, Germany, July 2020. ACM.
[16] Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19–50, January 2010. doi:10.1017/S0956796809990268.
[17] Aïna Linn Georges, Benjamin Peters, Laila Albeheiry, Leo White, Stephan Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. Data race freedom à la mode. In Principles of Programming Languages (POPL 2025), volume 9 of Proceedings on Programming Languages, pages 656–686. ACM, January 2025. doi:10.1145/3704859.
[18] Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 2, pages 52–66, Pisa, Italy, March 1987. Springer-Verlag LNCS 250. doi:10.1007/BFB0014972.
[19] Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint natural deduction. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), pages 15:1–15:23, Tallinn, Estonia, July 2024. LIPIcs 299. Extended version available as https://arxiv.org/abs/2402.01428.
[20] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. doi:10.1017/S0956796818000151.
[21] Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In 42nd Annual Symposium on Principles of Programming Languages (POPL 2015), pages 637–650, Mumbai, India, January 2015. ACM. doi:10.1145/2676726.2676980.
[22] Gilles Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22–39. Springer-Verlag LNCS 247, 1987. doi:10.1007/BFB0039592.
[23] Norihiro Kamide. Kripke semantics for modal substructural logics. Journal of Logic, Language and Information, 11:453–470, 2002. doi:10.1023/A:1019915908844.
[24] Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. A logical framework with commutative and non-commutative subexponentials. In International Joint Conference on Automated Reasoning (IJCAR 2018), pages 228–245. Springer LNAI 10900, 2018. doi:10.1007/978-3-319-94205-6_16.
[25] Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154–170, 1958.
[26] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. In Proceedings of the ACM on Programming Languages, volume 7 (OOPSLA 2023), pages 286–315, April 2023. Extended version available as https://arxiv.org/abs/2303.05491.
[27] Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP²: Fully in-place functional programming. In International Conference on Functional Programming (ICFP 2023), Proceedings on Programming Languages, pages 275–304. ACM, August 2023. doi:10.1145/3607840.
[28] Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley. The functional essence of imperative binary search trees. In Programming Language Design and Implementation (PLDI 2024), volume 8 of Proceedings on Programming Languages, pages 518–542. ACM, January 2024. doi:10.1145/3656398.
[29] Wendy MacCaull. Relational semantics and a relational proof system for full Lambek calculus. Journal of Symbolic Logic, 63(2):623–637, 1998. doi:10.2307/2586855.
[30] John C Mitchell. Representation independence and data abstraction. In Proceedings of the 13th Symposium on Principles of Programming Languages (POPL 1986), pages 263–276. ACM, 1986. doi:10.1145/512644.512669.
[31] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. doi:10.1145/1352582.1352591.
[32] Peter W O’Hearn and David J Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999. doi:10.2307/421090.
[33] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Termination in session-based concurrency via linear logical relations. In H. Seidl, editor, 22nd European Symposium on Programming (ESOP 2012), pages 539–558, Tallinn, Estonia, March 2012. Springer LNCS 7211.
[34] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254–302, 2014. doi:10.1016/J.IC.2014.08.001.
[35] Frank Pfenning and Klaas Pruiksma. Relating message passing and shared memory, proof-theoretically. In S. Jongmans and A. Lopes, editors, 25th International Conference on Coordination Models and Languages (COORDINATION 2023), pages 3–27, Lisbon, Portugal, June 2023. Springer LNCS 13908. Notes to an invited talk. doi:10.1007/978-3-031-35361-1_1.
[36] Jeff Polakow. Ordered Linear Logic and Applications. PhD thesis, Department of Computer Science, Carnegie Mellon University, August 2001.
[37] Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA’99), pages 295–309, L’Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. doi:10.1007/3-540-48959-2_21.
[38] Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed. Adjoint logic and its concurrent operational interpretation. Unpublished manuscript, January 2018.
[39] Jason Reed. Hybridizing a logical framework. In Proceedings of the International Workshop on Hybrid Logic (HyLo’06), pages 135–148. Electronic Notes in Theoretical Computer Science, v.174(6), 2007.
[40] Jason Reed and Frank Pfenning. A constructive approach to the resource semantics of substructural logics. Unpublished Manuscript, May 2010. URL: https://www.cs.cmu.edu/˜jcreed/papers/rp-substruct.pdf.
[41] Jason C. Reed. A Hybrid Logical Framework. PhD thesis, Carnegie Mellon University, September 2009. Available as Technical Report CMU-CS-09-155.
[42] John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A. Mason, editor, Information Processing 83, pages 513–523. Elsevier, September 1983.
[43] Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13:11–49, 2000. Notes for lecture course given at the International Summer School in Computer Programming at Copenhagen, Denmark, August 1967. doi:10.1023/A:1010000313106.
[44] Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information flow control in cyclic process networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024), pages 40:1–40:30. LIPIcs 313, 2024. doi:10.4230/LIPICS.ECOOP.2024.40.
[45] Victoria Vollmer, Danielle Marshall, Harley Eades, III, and Dominic Orchard. A mixed linear and graded logic: Proofs, terms, and models. In 33rd Conference on Computer Science Logic (CSL 2025), pages 32:1–32:21, Amsterdam, The Netherlands, February 2025. LIPIcs 326. doi:10.4230/LIPICS.CSL.2025.32.
[46] Philip Wadler. Theorems for free! In J. Stoy, editor, Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture (FPCA’89), pages 347–359, London, UK, September 1989. ACM. doi:10.1145/99370.99404.
[47] Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational parametricity for a polymorphic linear lambda calculus. In K. Ueda, editor, 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), pages 344–359. Springer LNCS 6461, 2010. doi:10.1007/978-3-642-17164-2_24.

Appendix A Complete definition of the Type System

\begin{array}[]{llcll}\mbox{Types}&A,B&::=&\alpha\mid 1\mid A\bullet B\mid A% \rightarrowtail B\mid A\twoheadrightarrow B\mid\forall\alpha.\,A\\ &&\mid&A\to B\mid A\circ B\mid\oplus\{\ell:A_{\ell}\}_{\ell\in L}\end{array}

\begin{array}[]{llcl}\mbox{Purely Positive Types}&A^{+},B^{+}&::=&A^{+}\bullet B% ^{+}\mid A^{+}\circ B^{+}\\ &&\mid&\mathbf{1}\mid\oplus\{\ell:A^{+}_{\ell}\}_{\ell\in L}\mid F[\theta]\end% {array}

\begin{array}[]{llcl}\mbox{Type Definitions}&\Sigma&::=&F[\Delta]=A^{+}\mid(% \cdot)\mid\Sigma_{1},\Sigma_{2}\end{array}

\begin{array}[]{llcl}\mbox{Type Substitutions}&\theta&::=&\alpha\mapsto A^{+}% \mid(\cdot)\mid\theta_{1}\theta_{2}\end{array}

\begin{array}[]{llcll}\mbox{Terms}&e&::=&x\\ &&\mid&()\mid\mathbf{match}\;e\;(()\Rightarrow e^{\prime})&(\mathbf{1})\\ &&\mid&(e_{1},e_{2})\mid\mathbf{match}\;e\;((x,y)\Rightarrow e^{\prime})&(A% \bullet B)\\ &&\mid&\lambda x.\ e\mid e_{1}\,e_{2}&(A\rightarrowtail B,A\twoheadrightarrow B% ,A\to B)\\ &&\mid&k(e)\mid\mathbf{match}\leavevmode\nobreak\ e\leavevmode\nobreak\ \{\ell% (x_{\ell})\Rightarrow e^{\prime}\}_{\ell\in L}&(\oplus\{\ell:A_{\ell}\})\end{array}

Typing rules:

Operational semantics:

Appendix B Complete definition of the Logical Predicate

\begin{array}[]{lcl}m\Vdash^{S}e\in\llbracket A\rrbracket&\Longleftrightarrow&% \exists v.\,e\mathrel{\hookrightarrow}v\land m\Vdash^{S}v\in[A]\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[A\bullet B]&\Longleftrightarrow&\hskip-5.0% pt\begin{array}[t]{l}\exists m_{1},m_{2}.\;m=m_{1}\cdot m_{2}\land v=(v_{1},v_% {2})\\ \quad\land\leavevmode\nobreak\ m_{1}\Vdash^{S}v_{1}\in[A]\land m_{2}\Vdash^{S}% v_{2}\in[B]\end{array}\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[A\twoheadrightarrow B]&\Longleftrightarrow% &\forall k.\,k\Vdash^{S}w\in[A]\Longrightarrow m\cdot k\Vdash^{S}v\,w\in% \llbracket B\rrbracket\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[A\rightarrowtail B]&\Longleftrightarrow&% \forall k.\,k\Vdash^{S}w\in[A]\Longrightarrow k\cdot m\Vdash^{S}v\,w\in% \llbracket B\rrbracket\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[\alpha]&\Longleftrightarrow&m\mathrel{S(% \alpha)}v\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[\forall\alpha.\,A(\alpha)]&% \Longleftrightarrow&\forall B,R_{B}.\,m\Vdash^{S,\alpha\mapsto R_{B}}v\in[A(% \alpha)]\end{array}

\begin{array}[]{lcl}m\Vdash v\in[A\mathbin{\rightarrow}B]&\Longleftrightarrow&% \forall w.\,\epsilon\Vdash w\in[A]\Longrightarrow m\Vdash v\,w\in\llbracket B% \rrbracket\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[A\mathbin{\circ}B]&\Longleftrightarrow&% \exists m_{1},m_{2}.\;m=m_{2}\cdot m_{1}\land v=(v_{1},v_{2})\\ &&\hbox{}\land m_{1}\Vdash^{S}v_{1}\in[A]\land m_{2}\Vdash^{S}v_{2}\in[B]\end{array}

\begin{array}[]{lcl}m\Vdash^{S}k(v)\in[{\oplus}\{\ell:A_{\ell}\}_{\ell\in L}]&% \Longleftrightarrow&m\Vdash^{S}v\in[A_{k}]\land k\in L\end{array}

\begin{array}[]{lcl}m\Vdash^{S}v\in[F[\theta]]&\Longleftrightarrow&m\Vdash^{S}% v\in\theta(A^{+})\ \mbox{where $F[\Delta]=A^{+}\in\Sigma$}\end{array}

[bib.bib1] [1] Andreas Abel and Jean-Philippe Bernardy. A unified view of modalities in type systems. Proceedings of the ACM on Programming Languages, 4(ICFP):1–28, 2020. doi:10.1145/3408972.

[bib.bib2] [2] Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26:e2, 2016. doi:10.1017/S0956796816000022.

[bib.bib3] [3] Amal Ahmed, Derek Dreyer, and Andreas Rossberg. State-dependent representation independence. In 36th Symposium on Principles of Programming Languages (POPL 2009), pages 340–353, Savannah, Georgia, USA, January 2009. ACM. doi:10.1145/1480881.1480925.

[bib.bib4] [4] Amal Ahmed, Matthew Fluet, and Greg Morrisett. A step-indexed model of substructural state. In 10th International Conference on Functional Programming (ICFP 2005), pages 78–91, 2005. doi:10.1145/1086365.1086376.

[bib.bib5] [5] Amal Ahmed, Matthew Fluet, and Greg Morrisett. L³: a linear language with locations. Fundamenta Informaticae, 77(4):397–449, 2007.

[bib.bib6] [6] Bob Atkey and James Wood. Context constrained computation. In 3rd Workshop on Type-Driven Development (TyDe’18), 2018.

[bib.bib7] [7] Robert Atkey. Syntax and semantics of quantitative type theory. In Anuj Dawar and Erich Grädel, editors, 33rd Conference on Logic in Computer Science (LICS 2018), pages 56–65, Oxford, UK, July 2018. ACM. doi:10.1145/3209108.3209189.

[bib.bib8] [8] Stephanie Balzer, Farzaneh Derakhshan, Robert Harper, and Yue Yao. Logical relations for session-typed concurrency. arXiv preprint arXiv:2309.00192, 2023. doi:10.48550/arXiv.2309.00192.

[bib.bib9] [9] P. N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Leszek Pacholski and Jerzy Tiuryn, editors, Selected Papers from the 8th International Workshop on Computer Science Logic (CSL’94), pages 121–135, Kazimierz, Poland, September 1994. Springer LNCS 933. An extended version appears as Technical Report UCAM-CL-TR-352, University of Cambridge.

[bib.bib10] [10] Lars Birkedal, Thomas Dinsdale-Young, Armaël Guéneau, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. Theorems for free from separation logic specifications. Proceedings of the ACM on Programming Languages, 5(ICFP):1–29, 2021. doi:10.1145/3473586.

[bib.bib11] [11] Luís Caires, Jorge A Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In 22nd European Symposium on Programming (ESOP 2013), pages 330–349, Rome, Italy, March 2013. Springer LNCS 7792. doi:10.1007/978-3-642-37036-6_19.

[bib.bib12] [12] Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In P.Gastin and F.Laroussinie, editors, 21st International Conference on Concurrency Theory (CONCUR 2010), pages 222–236, Paris, France, August 2010. Springer LNCS 6269. doi:10.1007/978-3-642-15375-4_16.

[bib.bib13] [13] Farzaneh Derakhshan, Stephanie Balzer, and Limin Jia. Session logical relations for noninterference. In 36th Annual Symposium on Logic in Computer Science (LICS 2021), pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470654.

[bib.bib14] [14] Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading policies for flexible information flow control in session-typed concurrency (artifact). Dagstuhl Artifacts Series, 10(2):4–1, 2024.

[bib.bib15] [15] Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages. In 35th Symposium on Logic in Computer Science (LICS 2020), pages 440–453, Saarbrücken, Germany, July 2020. ACM.

[bib.bib16] [16] Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. Journal of Functional Programming, 20(1):19–50, January 2010. doi:10.1017/S0956796809990268.

[bib.bib17] [17] Aïna Linn Georges, Benjamin Peters, Laila Albeheiry, Leo White, Stephan Dolan, Richard A. Eisenberg, Chris Casinghino, François Pottier, and Derek Dreyer. Data race freedom à la mode. In Principles of Programming Languages (POPL 2025), volume 9 of Proceedings on Programming Languages, pages 656–686. ACM, January 2025. doi:10.1145/3704859.

[bib.bib18] [18] Jean-Yves Girard and Yves Lafont. Linear logic and lazy computation. In H. Ehrig, R. Kowalski, G. Levi, and U. Montanari, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development, volume 2, pages 52–66, Pisa, Italy, March 1987. Springer-Verlag LNCS 250. doi:10.1007/BFB0014972.

[bib.bib19] [19] Junyoung Jang, Sophia Roshal, Frank Pfenning, and Brigitte Pientka. Adjoint natural deduction. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), pages 15:1–15:23, Tallinn, Estonia, July 2024. LIPIcs 299. Extended version available as https://arxiv.org/abs/2402.01428.

[bib.bib20] [20] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 28:e20, 2018. doi:10.1017/S0956796818000151.

[bib.bib21] [21] Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In 42nd Annual Symposium on Principles of Programming Languages (POPL 2015), pages 637–650, Mumbai, India, January 2015. ACM. doi:10.1145/2676726.2676980.

[bib.bib22] [22] Gilles Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, pages 22–39. Springer-Verlag LNCS 247, 1987. doi:10.1007/BFB0039592.

[bib.bib23] [23] Norihiro Kamide. Kripke semantics for modal substructural logics. Journal of Logic, Language and Information, 11:453–470, 2002. doi:10.1023/A:1019915908844.

[bib.bib24] [24] Max Kanovich, Stepan Kuznetsov, Vivek Nigam, and Andre Scedrov. A logical framework with commutative and non-commutative subexponentials. In International Joint Conference on Automated Reasoning (IJCAR 2018), pages 228–245. Springer LNAI 10900, 2018. doi:10.1007/978-3-319-94205-6_16.

[bib.bib25] [25] Joachim Lambek. The mathematics of sentence structure. The American Mathematical Monthly, 65(3):154–170, 1958.

[bib.bib26] [26] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel. Verus: Verifying Rust programs using linear ghost types. In Proceedings of the ACM on Programming Languages, volume 7 (OOPSLA 2023), pages 286–315, April 2023. Extended version available as https://arxiv.org/abs/2303.05491.

[bib.bib27] [27] Anton Lorenzen, Daan Leijen, and Wouter Swierstra. FP²: Fully in-place functional programming. In International Conference on Functional Programming (ICFP 2023), Proceedings on Programming Languages, pages 275–304. ACM, August 2023. doi:10.1145/3607840.

[bib.bib28] [28] Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley. The functional essence of imperative binary search trees. In Programming Language Design and Implementation (PLDI 2024), volume 8 of Proceedings on Programming Languages, pages 518–542. ACM, January 2024. doi:10.1145/3656398.

[bib.bib29] [29] Wendy MacCaull. Relational semantics and a relational proof system for full Lambek calculus. Journal of Symbolic Logic, 63(2):623–637, 1998. doi:10.2307/2586855.

[bib.bib30] [30] John C Mitchell. Representation independence and data abstraction. In Proceedings of the 13th Symposium on Principles of Programming Languages (POPL 1986), pages 263–276. ACM, 1986. doi:10.1145/512644.512669.

[bib.bib31] [31] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. doi:10.1145/1352582.1352591.

[bib.bib32] [32] Peter W O’Hearn and David J Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, 1999. doi:10.2307/421090.

[bib.bib33] [33] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Termination in session-based concurrency via linear logical relations. In H. Seidl, editor, 22nd European Symposium on Programming (ESOP 2012), pages 539–558, Tallinn, Estonia, March 2012. Springer LNCS 7211.

[bib.bib34] [34] Jorge A. Pérez, Luís Caires, Frank Pfenning, and Bernardo Toninho. Linear logical relations and observational equivalences for session-based concurrency. Information and Computation, 239:254–302, 2014. doi:10.1016/J.IC.2014.08.001.

[bib.bib35] [35] Frank Pfenning and Klaas Pruiksma. Relating message passing and shared memory, proof-theoretically. In S. Jongmans and A. Lopes, editors, 25th International Conference on Coordination Models and Languages (COORDINATION 2023), pages 3–27, Lisbon, Portugal, June 2023. Springer LNCS 13908. Notes to an invited talk. doi:10.1007/978-3-031-35361-1_1.

[bib.bib36] [36] Jeff Polakow. Ordered Linear Logic and Applications. PhD thesis, Department of Computer Science, Carnegie Mellon University, August 2001.

[bib.bib37] [37] Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA’99), pages 295–309, L’Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. doi:10.1007/3-540-48959-2_21.

[bib.bib38] [38] Klaas Pruiksma, Willow Chargin, Frank Pfenning, and Jason Reed. Adjoint logic and its concurrent operational interpretation. Unpublished manuscript, January 2018.

[bib.bib39] [39] Jason Reed. Hybridizing a logical framework. In Proceedings of the International Workshop on Hybrid Logic (HyLo’06), pages 135–148. Electronic Notes in Theoretical Computer Science, v.174(6), 2007.

[bib.bib40] [40] Jason Reed and Frank Pfenning. A constructive approach to the resource semantics of substructural logics. Unpublished Manuscript, May 2010. URL: https://www.cs.cmu.edu/˜jcreed/papers/rp-substruct.pdf.

[bib.bib41] [41] Jason C. Reed. A Hybrid Logical Framework. PhD thesis, Carnegie Mellon University, September 2009. Available as Technical Report CMU-CS-09-155.

[bib.bib42] [42] John C. Reynolds. Types, abstraction, and parametric polymorphism. In R.E.A. Mason, editor, Information Processing 83, pages 513–523. Elsevier, September 1983.

[bib.bib43] [43] Christopher Strachey. Fundamental concepts in programming languages. Higher-Order and Symbolic Computation, 13:11–49, 2000. Notes for lecture course given at the International Summer School in Computer Programming at Copenhagen, Denmark, August 1967. doi:10.1023/A:1010000313106.

[bib.bib44] [44] Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information flow control in cyclic process networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024), pages 40:1–40:30. LIPIcs 313, 2024. doi:10.4230/LIPICS.ECOOP.2024.40.

[bib.bib45] [45] Victoria Vollmer, Danielle Marshall, Harley Eades, III, and Dominic Orchard. A mixed linear and graded logic: Proofs, terms, and models. In 33rd Conference on Computer Science Logic (CSL 2025), pages 32:1–32:21, Amsterdam, The Netherlands, February 2025. LIPIcs 326. doi:10.4230/LIPICS.CSL.2025.32.

[bib.bib46] [46] Philip Wadler. Theorems for free! In J. Stoy, editor, Proceedings of the 4th International Conference on Functional Programming Languages and Computer Architecture (FPCA’89), pages 347–359, London, UK, September 1989. ACM. doi:10.1145/99370.99404.

[bib.bib47] [47] Jianzhou Zhao, Qi Zhang, and Steve Zdancewic. Relational parametricity for a polymorphic linear lambda calculus. In K. Ueda, editor, 8th Asian Symposium on Programming Languages and Systems (APLAS 2010), pages 344–359. Springer LNCS 6461, 2010. doi:10.1007/978-3-642-17164-2_24.