# A Program Logic for Fresh Name Generation

Harold Pancho Eliott, Martin Berger

► To cite this version:

Harold Pancho Eliott, Martin Berger. A Program Logic for Fresh Name Generation. 9th International Conference on Fundamentals of Software Engineering (FSEN), May 2021, Virtual, Iran. pp.76-91, 10.1007/978-3-030-89247-0_6. hal-04074511

HAL Id: hal-04074511

https://inria.hal.science/hal-04074511

Submitted on 19 Apr 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

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

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

ifip

International Federation for Information Processing

This document is the original author manuscript of a paper submitted to an IFIP
conference proceedings or other IFIP publication by Springer Nature. As such, there
may be some differences in the official published version of the paper. Such
differences, if any, are usually due to reformatting during preparation for publication or
minor corrections made by the author(s) during final proofreading of the publication
manuscript.
# A Program Logic for Fresh Name Generation

Harold Pancho Eliott¹ and Martin Berger¹,²

¹ Department of Informatics, University of Sussex, Brighton, UK.

² Turing Core, Huawei 2012 Labs, London, UK.

**Abstract.** We present a program logic for Pitts and Stark's $v$-calculus, an extension of the call-by-value simply-typed $\lambda$-calculus with a mechanism for the generation of fresh names. Names can be compared for equality and inequality, producing programs with subtle observable properties. Hidden names produced by interactions between generation and abstraction are captured logically with a second-order quantifier over type contexts. We illustrate usage of the logic through reasoning about well-known difficult cases from the literature.

## 1 Introduction

Naming is a long-standing problem in computer science. Most programming languages can define naming constructs, which, when called, yield a fresh name. The $\pi$-calculus [11] made naming and the $v$-operator, a constructor for name creation, a first-class construct, leading to a flurry of research, e.g. [6–8, 14, 15, 18]. Initially it was unclear if the $\pi$-calculus approach had purchase beyond process calculi. Pitts and Stark [16] as well as Odersky [12] added the $v$-operator to the simply-typed $\lambda$-calculus (STLC from now on), and showed that the subtleties of naming are already present in the interplay between higher-order functions and fresh name generation. This raises the question of how compositionally to reason about programs that can generate fresh names? There are program logics for ML-like languages that can generate fresh references, such as [4, 19], but, to the best of our knowledge, always in the context of languages with other expressive features such as aliasing, mutable higher-order state or pointer arithmetic, leading to complex logics, where the contribution of fresh name generation to the difficulties of reasoning is not apparent. This is problematic because, while the type $Nm$ carries the same information as Ref(Unit) in ML, we are often interested in reasoning about languages that combine fresh name generation with other features, such as meta-programming [3]. Can we study reasoning about fresh names in as simple a programming language as possible?

**Research question.** Is there a Hoare-style program logic for the $v$-calculus, conservatively extending program logics for the STLC in a natural manner, that allows for compositional reasoning about fresh name generation?

The present paper gives an affirmative answer to the research question, and presents the first program logic for the $v$-calculus.
**Informal explanation.** By the $\nu$-calculus we mean the STLC with a type $Nm$ of names, a constructor $gensym$ of type $Unit \to Nm$ and a destructor, in form of equality and inequality on names ($gensym$ and $\nu$ are essentially identical, but the former is more widely used). Immediately we realise that the $\nu$-calculus loses extensionality, as $gensym() = gensym()$ evaluates to false. While the loss of extensionality is expected in a stateful language, the $\nu$-calculus does not have state, at least not in a conventional sense.

A first difficulty is expressing freshness in logic. What does it mean for a name $x$ to be fresh? A first idea might be to say that $x$ is guaranteed to be distinct from all existing names. We cannot simply say

$$ \{T\} \text{gensym()} :_u \{\forall x.u \neq x\} $$

since we must prevent $\forall x.u \neq x$ being instantiated to $u \neq u$. We want to say something like:

$$ \forall x. \{T\} \text{gensym()} :_u \{u \neq x\} \qquad (1) $$

Unfortunately we cannot quantify over Hoare triples. A second problem is that (1) is not strong enough, in the sense that $gensym$ does not just create names that are fresh w.r.t. existing names, but also w.r.t. all future calls to $gensym$. We introduce a new quantifier to deal with both problems at the same time. A third difficulty is that fresh names can be exported or remain hidden, with observable consequences. Consider:

$$ \text{let } x = \text{gensym()} \text{ in } \lambda y.x = y \qquad (2) $$

of type $Nm \to Bool$. It receives a name $y$ as argument and compares it with fresh name $x$. Since $x$ is never exported to the outside, no context can ever supply this fresh $x$ to $\lambda y.x = y$. Hence (2) must be contextually indistinguishable from $\lambda yfalse$ Operationally, this is straightforward. But how can we prove this compositionally? Note that this is not a property of $\lambda y.x = y$, but it is also not a consequence of $x$'s being freshly generated, for $x$ is also fresh in this program:

$$ \text{let } x = \text{gensym()} \text{ in } \langle x, \lambda y.x = y \rangle \qquad (3) $$

But in (3), $\lambda y.x = y$ can return true, for example if we use (3) in this context:

$$ \text{let } p = [] \text{ in } (\pi_2 p)(\pi_1 p) $$

In program logics like [9], the specification of any abstraction $\lambda y.M$ will be a universally quantified formula $\forall y.A$. With fresh names, instantiation of quantification is a core difficulty. Recall that in first-order logic, $\forall y.A$ always implies $A[e/y]$, for all ambient expressions $e$. Clearly, in the case of (2) we cannot conclude to $A[x/y]$ from $\forall y.A$, because $x$ is, in some sense, not available for instantiation. In contrast, in the case of (3) we can infer $A[x/y]$. Hence we need to answer the question how to express logically the inability to instantiate a universal quantifier with a fresh and hidden name like $x$ in (2). We introduce a novel restricted quantifier, limiting the values based on a type context, and a new quantifier over type contexts to extend the reach of restricted quantifiers.
## 2 Programming Language

Our programming language is essentially the $\nu$-calculus of [16], with small additions in particular pairs, included for the sake of convenience. We assume a countably infinite set of variables, ranged over by $x, y, ...$ and a countably infinite set, disjoint from variables, of names, ranged over by $r, ...$. Constants ranged over by $c$ are Booleans true, false, and Unit ($\emptyset$). For simplicity we also call our language $\nu$-calculus. It is given by the following grammar, where $\alpha$ ranges over types, $\Gamma$ over standard type contexts (STC), $V$ over values and $M$ over programs. (Key additions over the STLC highlighted.)

$$ 
\begin{array}{lclcl}
\alpha & ::= & \text{Unit} \mid \text{Bool} \mid \text{Nm} & \mid & \alpha \to \alpha \mid \alpha \times \alpha & \Gamma ::= \emptyset \mid \Gamma, x : \alpha \\[1em]
V & ::= & r & \mid & \text{gensym} & \mid x \mid c \mid \lambda x.M \mid \langle V, V \rangle \\[1em]
M & ::= & V \mid MM \mid \text{let } x = M \text{ in } M & \mid & M = M & \\
& & & & \text{if } M \text{ then } M \text{ else } M & \mid \langle M, M \rangle \mid \pi_i(M)
\end{array}
$$

Free variables in $M$, written $fv(M)$ are defined as usual. $M$ is closed if $fv(M) = \emptyset$. There are no binders for names so the set $\mathring{a}(M)$ of all names in $M$, is given by the obvious rules, including $\mathring{a}(r) = \{r\}$ and $\mathring{a}(MN) = \mathring{a}(M) \cup \mathring{a}(N)$. If $\mathring{a}(M) = \emptyset$ then $M$ is compile-time syntax. The $\nu n.M$ constructor from the $\nu$-calculus [16] is equivalent to let $n = \text{gensym}()$ in $M$ as $\text{gensym}()$ generates fresh names. The typing judgements is $\Gamma \vdash M : \alpha$, with the STC $\Gamma$ being an unordered mapping from variables to types. Typing rules are standard [13] with the following extensions: $\Gamma \vdash \text{gensym} : \text{Unit} \to \text{Nm}$ and $\Gamma \vdash r : \text{Nm}$.

The operational semantics of our $\nu$-calculus is straightforward and the same as [16]. A configuration of type $\alpha$ is a pair $(G, M)$ where $M$ is a closed term of type $\alpha$, and $G$ a finite set of previously Generated names such that $\mathring{a}(M) \subseteq G$. The standard call-by-value reduction relation, $\to$, has the following key rules.

$$ 
\begin{array}{lclcl}
(G, (\lambda x.M)V) & \to & (G, M[V/x]) & \\
(G, \text{gensym}()) & \to & (G \cup \{n\}, n) & (n \notin G) \\
(G \cup \{n\}, n = n) & \to & (G \cup \{n\}, \text{true}) & \\
(G \cup \{n_1, n_2\}, n_1 = n_2) & \to & (G \cup \{n_1, n_2\}, \text{false}) & (n_1 \neq n_2) \\
(G, M) \to (G', N) & \text{implies} & (G, \mathcal{E}[M]) \to (G', \mathcal{E}[N]) &
\end{array}
$$

Here $M[V/x]$ is the usual capture-avoiding substitution, and $\mathcal{E}[\cdot]$ ranges over the usual reduction contexts of the STLC. Finally, $\downarrow$ is short for $\to^*$.

## 3 Logical Language

This section defines the syntax of the logic. As is customary for program logics, ours is an extension of first order logic with equality. Expressions, ranged over by $e, e', ..., \text{formulae}$, ranged over by $A, B, C, ...$ and Logical Type Contexts (LTCs),
ranged over by $\mathcal{I}', \mathcal{I}', \mathcal{I}_i, \dots$, are given by the grammar below. (Adaptations over [9] highlighted.)

$$ 
\begin{array}{rcl}
e & ::= & x^{\alpha} \mid c \mid \langle e, e \rangle \mid \pi_i(e) \\
\mathcal{I}' & ::= & \emptyset \mid \mathcal{I} + x : \alpha \mid \mathcal{I} + \delta : \mathcal{TC} \\
A & ::= & e = e \mid \neg A \mid A \wedge A \mid e \bullet e = x^{\alpha} \{A\} \mid \forall x^{\alpha} \in (\mathcal{I}') . A \mid \forall \delta . A
\end{array}
$$

Expressions, $e$, are standard, where constants, $c$, range over Booleans and `()`, but do not include names or gensym as constants. Equality, negation and conjunction are standard. Evaluation formulae $e \bullet e' = m\{A\}$ internalise triples [9] and express that if the program denoted by $e$ is executed with argument denoted by $e'$, then the result, denoted by $m$, satisfies $A$. Since the $\nu$-calculus has no recursion, all applications terminate and we do not distinguish partial from total correctness. We write $e_1 \bullet e_2 = e_3$ as shorthand for $e_1 \bullet e_2 = m\{m = e_3\}$.

Given variables represent values, ensuring hidden names cannot be revealed in an unsafe manner requires the idea that a value is *derived* from an LTC if a name free term uses the variables in the LTC to evaluate to said value. Specifically define a name as reachable from said LTC if it can be derived from it, and hidden otherwise.

Freshness is not an absolute notion. Instead, a name is fresh with respect to something, in this case names generated in the past, and future of the computation. Formulae refer to names by variables, and variables are tracked in the STC. Freshness is now defined in two steps: (1) First we characterise freshness of a name w.r.t. the current STC, meaning the name cannot be derived from the variables in the STC. Then, (2) we define freshness w.r.t. all future extension of the current STC, details in Sec. 4. The modal operator is used in [19] in order to express “for all future extensions”, but we found modalities inconvenient, since they don’t allow us to name extensions. We introduce a new quantifier $\forall x^{\alpha} \in (\mathcal{I}') . A$ instead, where $\mathcal{I}'$ ranges over LTCs from which $x$ can be derived. To make this precise, we need LTCs (explained next), a generalisation of STCs.

**LTCs.** Like STCs, LTCs map variables to types, and are needed for typing expressions, formulae and triples (introduced in Sec. 6), LTCs generalise STCs in two ways: they are *ordered*, and they don’t just contain program variables, but also *type context variables* (TCVs), ranged over by $\delta$. TCVs are always mapped to the new type $\mathcal{TC}$, short for *type context*. The ordering in LTCs is essential because $\mathcal{I} + \delta : \mathcal{TC}$ implies $\delta$ represents an *extension* of the LTC $\mathcal{I}'$.

**Restricted universal quantification.** The meaning of $\forall x^{\alpha} \in (\mathcal{I}') . A$ is intuitively simple: $A$ must be true for all $x$ that range only over values of type $\alpha$, derived from $\mathcal{I}'$ that do not reveal hidden names. For example if the model contained the name $r$ but only as $\lambda y.y = r$, then $r$ was hidden and whatever $x$ in $\forall x^{\alpha} \in (\mathcal{I}') . A$ ranged over, it must not reveal $r$. Formalising this requirement is subtle.

**Quantification over LTCs.** Below we formalise the axiomatic semantics of gensym by saying that the result of each call to this function is fresh w.r.t. all
future extensions of the present state (with the present state being included). The purpose of $\forall \delta.A$ is to allow us to do so: $\forall \delta.A$ implies for all future states derived from the current state (included), when the LTC for that state is assigned to the TCV $\delta$, then $A$ holds.

**A convenient shorthand, the freshness predicate.** We express freshness of the name $e$ relative to the LTC $\mathcal{I}$ as $\forall z \in (\mathcal{I}).e \neq z$. and, as this predicate is used pervasively, abbreviate it to $e\#\mathcal{I}$. Intuitively, $e\#\mathcal{I}$, a variant of a similar predicate in [19], states that the name denoted by $e$ is not derivable, directly or indirectly, from the LTC $\mathcal{I}$.

**Typing of expressions, formulae and triples.** We continue with setting up definitions that allow us to type expressions, formulae and triples. The ordered union of $\mathcal{I}$ and $\mathcal{I}'$ with $\text{dom}(\mathcal{I}) \cap \text{dom}(\mathcal{I}') = \emptyset$ is written $\mathcal{I} + \mathcal{I}'$, and should be understood as: every variable from $\text{dom}(\mathcal{I})$ comes before every variable from $\text{dom}(\mathcal{I}')$. Other abbreviations include $\exists x^\alpha \in (\mathcal{I}).A \stackrel{\text{def}}{=} \neg\forall x^\alpha \in (\mathcal{I}).\neg A$, and where types are obvious then $\mathcal{I}+y \stackrel{\text{def}}{=} \mathcal{I}+y : \alpha$ and $\mathcal{I}+\delta \stackrel{\text{def}}{=} \mathcal{I}+\delta : \text{TC}$. For simplicity, where not explicitly required, $\mathcal{I}+\delta$ is written $\delta$. Functions on LTCs are defined as expected including mapping variables, $\mathcal{I}(x)$, and TCVs, $\mathcal{I}^-(\delta)$; obtaining the domain, $\text{dom}(\mathcal{I})$; ordered removal of a variable, $\mathcal{I} \setminus x$; ordered removal of all TCV, $\mathcal{I} \setminus_{TCV}$; and removal of TCV to produce a STC, $\mathcal{I} \downarrow_{TC}$. We define free variables of LTC, $\text{fv}(\mathcal{I}) \stackrel{\text{def}}{=} \text{dom}(\mathcal{I} \downarrow_{TC}) \stackrel{\text{def}}{=} \text{dom}(\mathcal{I} \setminus_{TCV})$, then free variables of formulae defined as expected, with the addition of $\text{fv}(e\#\mathcal{I}) \stackrel{\text{def}}{=} \text{fv}(\mathcal{I}) \cup \text{fv}(e)$, $\text{fv}(\forall x \in (\mathcal{I}).A) \stackrel{\text{def}}{=} (\text{fv}(A)\setminus\{x\}) \cup \text{fv}(\mathcal{I})$, and $\text{fv}(\forall \delta.A) \stackrel{\text{def}}{=} \text{fv}(A)$. Similarly $\text{ftcv}(\mathcal{I})$ and $\text{ftcv}(A)$ define all TCV occurring in $\mathcal{I}$ and unbound by $\forall \delta$. in $A$ respectively, calling $\mathcal{I}$ TCV-free if $\text{ftcv}(\mathcal{I}) \stackrel{\text{def}}{=} \emptyset$. The typing judgement for LTCs, written $\mathcal{I} \vdash \mathcal{I}'$, checks that $\mathcal{I}'$ is an 'ordered subset' of $\mathcal{I}$. Type checks on expressions, formulae and triples use LTC as the base, written $\mathcal{I} \vdash e : \alpha$, $\mathcal{I} \vdash A$ and $\mathcal{I} \vdash \{A\} M :_u \{B\}$ respectively. Fig. 1 gives the rules defining the typing judgements. From now on we adhere to the following convention: All expressions, formulae and triples are typed, and we will mostly omit being explicit about typing.

**Advanced substitutions.** Reasoning with quantifiers requires quantifier instantiation. This is subtle with $\forall \delta.A$, and we need to define two substitutions, $A[e/x]_\mathcal{I}$ (substitutes expressions for variables) and $A[\mathcal{I}_0/\delta]_\mathcal{I}$ (substitutes LTCs for TCVs). First extend the definition $e$ is free for $x^\alpha$ in $A$ in [10], to ensure if $e$ contains destructors i.e. $\pi_i(\quad)$ or $=$, then all free occurrences of $x$ in any LTC $\mathcal{I}_0$ in $A$ must imply $\mathcal{I}_0 \vdash e : \alpha$. Below, we assume the standard substitution $e[e'/x]$ of expressions for variables in expressions, simple details omitted.

We define $A[e/x]_\mathcal{I}$, logical substitution of $e$ for $x$ in $A$ in the context of $\mathcal{I}$, if $e$ is free for $x$ in $A$ with $e$ and $A$ typed by $\mathcal{I}$, by the following clauses (simple cases omitted) and the auxiliary operation on LTCs below. We often write $A[e/x]$ for $A[e/x]_\mathcal{I}$.
<figure><img src="image_3.png" /><figcaption>**Fig. 1.** Typing rules for LTCs, expressions, formulae and triples (see Sec. 6). Simple cases omitted. *M* in the last rule is compile-time syntax.</figcaption></figure>

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

Type context substitution $A[\Pi_0/\delta]_\Pi$ instantiates $\delta$ with $\Pi_0$ in $A$, similar to classical substitution. We often write $[\Pi_0/\delta]$ for $[\Pi_0/\delta]_\Pi$ as $\Pi$ is used for ordering and is obvious. As above, the omitted cases are straightforward and the auxiliary operation on LTCs is included.

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

## 4 Model

We define a *model* $\xi$ as a finite (possibly empty) map from variables and TCV to closed values and TCV-free LTCs respectively.
$$ \xi ::= \emptyset \mid \xi \cdot x : V \mid \xi \cdot \delta : \mathbb{I}' $$

Standard actions on models $\xi$ are defined as expected and include: variable mappings to values, $\xi(x)$, or TCV mapping to LTC, $\xi(\delta)$; removal of variable $x$ as $\xi\backslash x$ (with $(\xi \cdot \delta : \mathbb{I}_1)\backslash x = (\xi\backslash x) \cdot \delta : (\mathbb{I}_1\backslash x)$); removal of TCV $\delta$ as $\xi\backslash \delta$; removal of all TCVs as $\xi\backslash_{-TCV}$; and defining all names in $\xi$ as $\hat{\mathbb{a}}(\xi)$ noting that $\hat{\mathbb{a}}(\mathbb{I}') = \emptyset$.

A model $\xi$ is typed by a LTC $\mathbb{I}'$ written $\xi^{\mathbb{I}}$, if $\mathbb{I}' \vdash \xi$ as defined below, were $\mathbb{I}_d = \mathbb{I}_d\backslash_{-TCV}$ formalises that $\mathbb{I}_d$ is TCV-free.

$$ \frac{\mathbb{I}' \vdash \xi \quad \emptyset \vdash V : \alpha}{\emptyset \vdash \emptyset} \qquad \frac{\mathbb{I}' \vdash \xi \quad \mathbb{I}' \vdash \mathbb{I}_d \quad \mathbb{I}_d = \mathbb{I}_d\backslash_{-TCV}}{\mathbb{I}' \vdash \delta \vdash \xi \cdot \delta : \mathbb{I}_d} $$

The closure of a term $M$ by a model $\xi$, written $M\xi$ is defined as standard with the additions, gensym $\xi \stackrel{\text{def}}{=} \text{gensym}$ and $r\xi \stackrel{\text{def}}{=} r$. Noting that $M\xi\backslash_{-TCV} = M\xi = M\xi \cdot \delta : \mathbb{I}'$ holds for all $\delta$ and $\mathbb{I}'$ as $\mathbb{I}' \downarrow_{-TCV} \vdash M : \alpha$.

The interpretation of expression $e$ in a model $\xi^{\mathbb{I}}$, written $[[e]]_{\xi}$, is standard, e.g. $[[c]]_{\xi} \stackrel{\text{def}}{=} c$, $[[x]]_{\xi} \stackrel{\text{def}}{=} \xi(x)$, $[[\langle e, e' \rangle]]_{\xi} \stackrel{\text{def}}{=} \langle [[e]]_{\xi}, [[e']]]_{\xi} \rangle$, etc.

The interpretation of LTCs $\mathbb{I}_0$ in a model $\xi^{\mathbb{I}}$, written $[[\mathbb{I}_0]]_{\xi}$, outputs a STC. It is assumed $\mathbb{I}'$ types the LTC in the following definition:

$$ [[\emptyset]]_{\xi} \stackrel{\text{def}}{=} \emptyset \qquad [[\mathbb{I}_0 + x : \alpha]]_{\xi} \stackrel{\text{def}}{=} [[\mathbb{I}_0]]_{\xi}, x : \alpha \qquad [[\mathbb{I}_0 + \delta : \text{TC}]]_{\xi} \stackrel{\text{def}}{=} [[\mathbb{I}_0]]_{\xi} \cup [[\xi(\delta)]]_{\xi} $$

Write $M \stackrel{[\mathbb{I}, \xi]}{\rightsquigarrow} V$ as the *derivation of a value* $V$ from term $M$ which is typed by the LTC $\mathbb{I}'$ and closed and evaluated in a model $\xi$. This ensures names are derived from actual reachable values in $\xi$ as if they were programs closed by the model, hence not revealing hidden names from $\xi$. $M \stackrel{[\mathbb{I}, \xi]}{\rightsquigarrow} V$ holds exactly when:

$$ - \hat{\mathbb{a}}(M) = \emptyset $$

$$ - [[\mathbb{I}]]_{\xi} \vdash M : \alpha $$

$$ - (\hat{\mathbb{a}}(\xi), M\xi) \Downarrow (\hat{\mathbb{a}}(\xi) \cup G', V) $$

Model extensions aim to capture the fact that models represent real states of execution, by stating a model is only constructed by evaluating terms derivable from the model.

A model $\xi'$ is a *single step model extension* to another model $\xi^{\mathbb{I}}$, written $\xi \prec \xi'$, if the single new value in $\xi'$ is derived from $\xi$ or the mapped LTC is $\mathbb{I}'$ with TCVs removed. Formally $\xi^{\mathbb{I}} \prec \xi'$ holds if either of the following hold:

- There is $M_y^{\alpha}$ such that $M_y \stackrel{[\mathbb{I}, \xi]}{\rightsquigarrow} V_y$ and $\xi'^{\mathbb{I}+y:\alpha} = \xi \cdot y : V_y$.

- $\xi'^{\mathbb{I}+\delta} = \xi \cdot \delta : \mathbb{I}'\backslash_{-TCV}$ for some $\delta$.

We write $\prec^*$ for the transitive, reflexive closure of $\prec$. If $\xi \prec^* \xi'$ we say $\xi'$ is an extension of $\xi$ and $\xi$ is a contraction of $\xi'$.
A model $\xi$ is constructed by $\mathbb{I}^\xi$, written $\mathbb{I}^\xi \triangleright \xi$, if any TCV represents a model extension. Formally we define $\mathbb{I}^\xi \triangleright \xi$ by the following rules:

$$ \frac{\mathbb{I}^\xi \triangleright \xi \quad \text{exists } M^\alpha . M \underset{\approx}{\overset{[\mathbb{I}^\xi, \xi]}{\rightarrow}} \mathcal{V}}{\mathbb{I}^\xi + x : \alpha \triangleright \xi \cdot x : \mathcal{V}} \quad \frac{\mathbb{I}^\xi \triangleright \xi_0 \quad \xi_0 \prec^* \xi^{\mathbb{I}_2} \quad \mathbb{I}_1 = \mathbb{I}_2 \setminus_{-\text{TCV}}}{\mathbb{I}^\xi + \delta \triangleright \xi \cdot \delta : \mathbb{I}_1} $$

A model $\xi^{\mathbb{I}}$ is well constructed if there exists an LTC, $\mathbb{I}'$, such that $\mathbb{I}' \triangleright \xi$, noting that $\mathbb{I} \models \mathbb{I}'$.

Model extensions and well constructed models represent models derivable by $\nu$-calculus programs, ensuring names cannot be revealed by later programs. Consider the basic model: $y : \lambda a$. if $a = r_1$ then $r_2$ else $r_3$, if $r_1$ could be added to the model, this clearly reveals access to $r_2$ otherwise $r_2$ is hidden. Hence the assumption that all models are well constructed from here onwards.

Contextual equivalence of two terms requires them to be contextually indis-
tinguishable in all variable-closing single holed contexts of Boolean type in any
valid configuration, as is standard [1,17]. When $M_1$ and $M_2$ are closed terms
of type $\alpha$ and $\dot{a}(M_1) \cup \dot{a}(M_2) \subseteq G$, we write $M_1 \cong_{\alpha}^G M_2$ to be equivalent to
$G, \emptyset \vdash M_1 \equiv M_2 : \alpha$ from [1].

## 4.1 Semantics

The satisfaction relation for formula A in a well constructed model $\xi^{\mathbb{I}}$, written
$\xi \models A$, assumes $\mathbb{I} \models A$, and is defined as follows:

$$ \begin{array}{l} - \xi \models e = e' \text{ if } [[e]]_{\xi} \cong_{\alpha}^{\dot{a}(\xi)} [[e')]_{\xi}. \\ - \xi \models \neg A \text{ if } \xi \not\models A. \\ - \xi \models A \land B \text{ if } \xi \models A \text{ and } \xi \models B. \\ - \xi \models e \bullet e' = m\{A\} \text{ if } ee' \underset{\approx}{\overset{[0, \xi]}{\rightarrow}} V \text{ and } \xi \cdot m : V \models A \end{array} $$

$$ - \xi \models e \bullet e' = m\{A\} \text{ if } ee' \underset{\approx}{\overset{[0, \xi]}{\rightarrow}} V \text{ and } \xi \cdot m : V \models A $$

$$ - \xi \models \forall x^{\alpha} \in (\mathbb{I}') . A \text{ if for all } M . M \underset{\approx}{\overset{[\mathbb{I}', \xi]}{\rightarrow}} V \text{ implies } \xi \cdot x : V \models A $$

$$ - \xi \models \forall \delta . A \text{ if for all } \xi' \mathbb{I}' . \xi \prec^* \xi' \text{ implies } \xi' \cdot \delta : (\mathbb{I}' \setminus_{-\text{TCV}}) \models A $$

$$ - \xi \models e \# \mathbb{I}_0 \text{ if there is no } M \text{ such that } M \underset{\approx}{\overset{[\mathbb{I}_0, \xi]}{\rightarrow}} [[e]]_{\xi} $$

In first-order logic, if a formula is satisfied by a model, then it is also satisfied by extensions of that model, and vice-versa (as long as all free variables of the formula remain in the model). This can no longer be taken for granted in our logic. Consider the formula $\forall \delta. \exists z \in (\delta).(z \# \mathbb{I} \wedge \neg z \# \delta)$ Validity of this formula depends on how many names exist in the ambient model: it may become invalid under contracting the model. Fortunately, such formulae are rarely needed when reasoning about programs. In order to simplify our soundness proofs we will therefore restrict some of our axioms and rules to formulae that are stable under model extension and contractions. Sometimes we need a weaker property, where formulae preserve their validity when a variable is removed from a model. Both concepts are defined semantically next.

We define formula A as *model extensions independent*, short *Ext-Ind*, if for all $\mathbb{I}, \xi^{\mathbb{I}}, \xi'$ such that $\mathbb{I} \models A$ and $\xi \prec^* \xi'$ we have: $\xi \models A$ iff $\xi' \models A$.

We define formula A as *thin w.r.t.* x, written A thin w.r.t. x<sup>α</sup>, if for all I
such that I \setminus x \models A and x<sup>α</sup> \in dom(I) we have for all well constructed models
ξ<sup>I</sup> and ξ \setminus x that: ξ \models A implies ξ \setminus x \models A.
## 5 Axioms

Axioms and axiom schemas are similar in intention to those of the logic for the STLC, but expressed within the constraints of our logic. Axiom schemas are indexed by the LTC that types them and the explicit types where noted. We introduce the interesting axioms (schemas) and those used in Sec. 7.

Equality axioms are standard where (eq1) allows for substitution. Most axioms for universal quantification over LTCs (u1)-(u5) are inspired by those of first order logic. The exceptions are (u2) which allows for the reduction of LTCs and (u5) which holds only on Nm-free types. Axioms for existential quantification over LTCs (ex1)-(ex3) are new aside from (ex1) which is the dual of (u1). Axiom (ex2) introduces existential quantification from evaluation formulae that produce a fixed result. Reducing $Π$ in $∃x ∈ (Π').A$ is possible via (ex3) for a specific structure. We use base types $α_b ::= Unit | Bool | α_b × α_b$ as core lambda calculus types excluding functions. Freshness axioms (f1)-(f2) show instances LTCs can be extended, whereas (f3)-(f4) reduce the LTC. Axiom (f1) holds due to f being derived from $Π+x$, and the rest are trivial.

$$ (eq1) \quad \mathcal{I} \vdash A(x) \wedge x = e \quad \leftrightarrow \quad A(x)[e/x]_I \qquad \mathcal{I}_0 \vdash e : \alpha $$

$$ (u1) \quad \mathcal{I} \vdash \forall x^{\alpha} \in (\mathcal{I}_0).A \quad \rightarrow \quad A[e/x]_{\mathcal{I}} $$

$$ (u2) \quad \forall x \in (\mathcal{I}_0 + \mathcal{I}_1).A \quad \rightarrow \quad (\forall x \in (\mathcal{I}_0).A) \wedge (\forall x \in (\mathcal{I}_1).A) $$

$$ (u3) \quad A^{-x} \quad \leftrightarrow \quad \forall x \in (\mathcal{I}_0).A^{-x} $$

$A - \text{Ext-Ind}$

$$ (u4) \quad \forall x \in (\mathcal{I}_0).(A \wedge B) \quad \leftrightarrow \quad (\forall x \in (\mathcal{I}_0).A) \wedge (\forall x \in (\mathcal{I}_0).B) $$

$$ (u5) \quad \forall x^{\alpha} \in (\mathcal{I}_0).A \quad \leftrightarrow \quad \forall x^{\alpha} \in (\emptyset).A $$

$\alpha$ is Nm-free

$$ (ex1) \quad \mathcal{I} \vdash A[e/x]_{\mathcal{I}} \quad \rightarrow \quad \exists x' \in (\mathcal{I}_0).A \quad \mathcal{I} \vdash \mathcal{I}_0 \text{ and } \mathcal{I}_0 \vdash e : \alpha $$

$$ (ex2) \quad \mathcal{I} + x + \mathcal{I}_0 \vdash a \bullet b = c \{c = x\} \quad \rightarrow \quad \exists x' \in (\mathcal{I}_0).x = x' \quad \{a, b\} \subseteq \text{dom}(\mathcal{I}_0) $$

$$ (ex3) \quad \mathcal{I} + x \vdash \forall y \in (\emptyset).\exists z^{Nm} \in (\mathcal{I}_0 + y).x = z \quad \rightarrow \quad \exists z \in (\mathcal{I}_0).x = z $$

$$ (f1) \quad \mathcal{I} + x + f : \alpha \rightarrow \alpha_b \vdash x \# \mathcal{I} \quad \rightarrow \quad x \# \mathcal{I} + f : \alpha \rightarrow \alpha_b $$

$$ (f2) \quad \mathcal{I} \vdash x \# \mathcal{I}_0 \wedge \forall y^{\alpha} \in (\mathcal{I}_0).A \quad \leftrightarrow \quad \forall y^{\alpha} \in (\mathcal{I}_0).(x \# (\mathcal{I}_0 + y) \wedge A) $$

$$ (f3) \quad x \# \mathcal{I}_0 \quad \rightarrow \quad x \neq e \qquad \mathcal{I}_0 \vdash e : \text{Nm} $$

$$ (f4) \quad x \# (\mathcal{I}_0 + \mathcal{I}_1) \quad \rightarrow \quad x \# \mathcal{I}_0 \wedge x \# \mathcal{I}_1 $$

Axioms for quantification over LTCs are also similar to those for the classical universal quantifier except (utc2) which extends the restricted quantifier to any future LTC which can only mean adding fresh names.

$$ (utc1) \quad \mathcal{I} \vdash \forall \delta.A \quad \rightarrow \quad A[\mathcal{I}/\delta]_{\mathcal{I}} $$

$$ (utc2) \quad \mathcal{I} \vdash \forall x^{Nm} \in (\mathcal{I}).A^{-\delta} \quad \leftrightarrow \quad \forall \delta.\forall x^{Nm} \in (\mathcal{I}+\delta).A \quad A - \text{Ext-Ind} $$

$$ (utc3) \quad A^{-\delta} \quad \leftrightarrow \quad \forall \delta.A^{-\delta} \qquad A - \text{Ext-Ind} $$

$$ (utc4) \quad \forall \delta.(A \wedge B) \quad \leftrightarrow \quad (\forall \delta.A) \wedge (\forall \delta.B) $$

Axioms for the evaluation formulae are similar to those of [2]. The interaction between evaluation formulae and the new constructors are shown. All STLC
values are included in the variables of Nm-free type, and if we let $\text{Ext}(e_2, e_2)$ stand for $\forall x \in (\emptyset).e_1 \bullet x = m_1\{e_2 \bullet x = m_2\{m_1 = m_2\}}$ then (ext) maintains extensionality in this logic for the STLC terms. Typing restrictions require $m \notin \text{fv}(A)$ in (e1) and $\text{fv}(e_1, e_2, m) \cap \text{dom}(\mathbb{I}^+ + x) = \emptyset$ in (e2).

$$ (e1) \qquad e_1 \bullet e_2 = m\{A \wedge B\} \quad \leftrightarrow \quad (A \wedge e_1 \bullet e_2 = m\{B\}) \qquad A - \text{Ext-Ind} $$

$$ (e2) \quad e_1 \bullet e_2 = m\{\forall x \in (\mathbb{I}^+).A\} \quad \leftrightarrow \quad \forall x \in (\mathbb{I}^+).e_1 \bullet e_2 = m\{A\} $$

$$ (e3) \qquad e_1 \bullet e_2 = m^{\alpha_b}\{\forall \delta.e_1 \bullet e_2 = m^{\alpha_b}\{A\} \quad A - \text{Ext-Ind} $$

$$ (ext) \qquad \text{Ext}(e_1, e_2) \quad \leftrightarrow \quad e_1 = \alpha_1 \to \alpha_2 \quad e_2 \qquad \alpha_1 \to \alpha_2 \text{ is Nm-free} $$

# 6 Rules

Our logic uses standard triples $\{A\} M :_m \{B\}$ where in this logic, the program $M$ is restricted to compile-time syntax. Triples are typed by the rule in Fig. 1. Semantics of triples is standard: if the pre-condition $A$ holds and the value derived from $M$ is assigned to the anchor $m$ then the post-condition $B$ holds. In detail: let $\xi^{\mathbb{I}}$ be a model.

$$ \xi^{\mathbb{I}} \models \{A\} M :_m \{B\} \quad \text{if} \quad \xi \models A \text{ implies } (M \stackrel{[\mathbb{I}, \xi]}{\rightsquigarrow} V \text{ and } \xi \cdot m : V \models B) $$

The triple is valid, written $\models \{A\} M :_m \{B\}$, if for all $\mathbb{I}$ and $\xi_0^{\mathbb{I}_0}$ we have

$$ \mathbb{I} \models \{A\} M :_m \{B\} \text{ and } \mathbb{I} \triangleright \xi_0 \text{ together imply: } \xi_0 \models \{A\} M :_m \{B\} $$

From here on we will assume all models are well constructed, noting that the construction of models is the essence of $\forall \delta$, as it allows for all possible future names generated. Variables occurring in $\text{dom}(\xi_0) - \text{dom}(\mathbb{I})$ may never occur directly in the triple, but their mapped values will have an effect.

The rules of inference can be found in Fig. 2 and Fig. 3. We write $\vdash \{A\} M :_m \{B\}$ to indicate that $\{A\} M :_m \{B\}$ can be derived from these rules. Our rules are similar to those of [9] for vanilla $\lambda$-calculi, but suitably adapted to the effectful nature of the $\nu$-calculus. All rules are typed. The typing of rules follows the corresponding typing of the programs occurring in the triples, but with additions to account for auxiliary variables. We have two substantially new rules: [GENSYM] and [LET]. The former lets us reason about fresh name creation by gensym, the latter about the let $x = M$ in $N$. Operationally, let $x = M$ in $N$ is often just an abbreviation for $(\lambda x.N)M$, but we have been unable to derive [LET] using the remaining rules and axioms. Any syntactic proof of [LET] requires [LAM] and [APP], which requires the postcondition: $C$ thin w.r.t $p$ for $p$ the anchor of the [LAM] rule. We have not been able to prove this thinness for all models of the relevant type.

In comparison with [9,19], the primary difference with our rules is our substitution. Our changes to substitution only affects [Eq] and [PROJ(i)] which are reduced in strength by the new definition of substitution as more constraints
are placed on the formulae to ensure correct substitution occurs. All other rules remain equally strong. The other difference from [9] is the need for thinness to replace the standard ‘free from’, which is discussed above. Removal of variables via thinness is required in the proof of soundness, for example [APP], which produces $u$ from $m$ and $n$, hence Ext-Ind is insufficient given the order of $\mathcal{I}+m+n+u \models C$, i.e. $u$ introduced after $m$ and $n$. We explain the novelty in the rules in more detail below.

<figure><img src="image_6.png" /><figcaption>**Fig. 2.** Rules for the core language, cf. [2,9,19]. We require *C* thin w.r.t *m* in [PROJ(*i*), LET] and *C* thin w.r.t *m*, *n* in [EQ, APP, PAIR]. We omit LTCs where not essential.</figcaption></figure>

In [GENSYM], $u \bullet () = m\{m\#\delta\}$ indicates the name produced by $u()$ and stored at $m$ is not derivable from the LTC $\delta$. If there were no quantification over LTCs prior to the evaluation we could only say $m$ is fresh from the current typing context, however we want to say that even if there is a future typing context with new names and we evaluate $u()$, this will still produce a fresh name. Hence we introduce the $\forall\delta$. to quantify over all future LTCs (and hence all future names). Elsewhere in reasoning it is key that the post-condition of [GENSYM] is Ext-Ind and hence holds in all extending and contracting models (assuming the anchor for gensym is present), reinforcing the re-applicability of gensym in any context.

Rules for $\lambda$-abstraction in previous logics for lambda-calculi [9,19] universally quantify over all possible arguments. Our corresponding [LAM] rule refines this and quantifies over current or future values that do not reveal hidden names. Comparing the two LTCs typing the assumption and conclusion implies $\mathcal{I}^+\delta+x$ extends $\mathcal{I}^+$ to any possible extension assigned to $\delta$, and extends to $x$ a value
derived from $\mathcal{I}^\Gamma+\delta$. Hence the typing implies precisely what is conveyed in the post-condition of the conclusion: '$\forall\delta.\forall x \in (\delta)$.'. Constraints on $\delta$ and $x$ are introduced by $B$, and $A$ - Ext-Ind implies $A$ still holds in all extensions of $\mathcal{I}^\Gamma$ including $\mathcal{I}^\Gamma+\delta+x$. The rest is trivial when we consider $((\lambda x.M)x)\xi \cong_{\alpha}^{\delta(\xi)} M\xi$.

The STLC's [LET] rule introduces $x$ in the post-condition by means of an '$\exists x.C'$. This fails here as $x$ may be unreachable, hence not derivable from any extending or contracting LTC. The requirement that $C$ thin w.r.t $x$ ensures $x$ is not critical to $C$ so can either be derived from the current LTC or is hidden. Thinness ensures no reference to the variable $m$ is somehow hidden under quantification over LTCs.

The [INVAR] rule is standard with the constraint that $C$ - Ext-Ind to ensure $C$ holds in the extension where $m$ has been assigned. The [LETFRESH] rule is commonly used and hence included for convenience, but it is entirely derivable from the other rules and axioms.

$$ \frac{\frac{A \to A' \quad \{A'\} M :_m \{B'\} \quad B' \to B}{\{A\} M :_m \{B\}} \qquad \frac{C - \text{Ext-Ind} \quad \{A\} M :_m \{B\}}{\{A \land C\} M :_m \{B \land C\}}}{\text{[CONSEQ]}} \qquad \frac{A - \text{Ext-Ind} \quad \mathcal{I}^\Gamma + m : \text{Nm} \vdash \{A \land m \# \mathcal{I}^\Gamma\} \quad M :_u \{C\}}{\mathcal{I}^\Gamma \vdash \{A\} \text{ let } m = \text{gensym() in } M :_u \{C\}}}{\text{[LETFRESH]}} $$

<caption>**Fig. 3.** Key structural rules [CONSEQ] and [INVAR] and for convenience the derived [LETFRESH] rule where $C$ thin w.r.t $m$ is required.</caption>

**Theorem 1.** All axioms and rules are sound.

**Theorem 2.** The logic for the $\nu$-calculus is a conservative extension of the logic [9] for the STLC.

All proofs can be found in the first author's forthcoming dissertation [5].

# 7 Reasoning Examples

**Example 1.** We reason about the core construct gensym() in an LTC $\mathcal{I}^\Gamma$. In Line 2, (utc1) instantiates the postcondition to $b \bullet () = a\{a\#\mathcal{I}^\Gamma+b\}$ and (f4) removes the $b$ from the LTC to ensure the postcondition satisfies the thin w.r.t $b$ requirement in [APP].

$$ 1 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \text{ gensym} :_b \{\forall \delta.b \bullet () = a\{a\#\delta\}\} \qquad \text{[GENSYM]} $$

$$ 2 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \text{ gensym} :_b \{b \bullet () = a\{a\#\mathcal{I}^\Gamma\}\} \quad \text{[CONSEQ], (utc1), (f4), 1} $$

$$ 3 \quad \mathcal{I}^\Gamma + b \Vdash \{b \bullet () = a\{a\#\mathcal{I}^\Gamma\}\} () :_c \{b \bullet c = a\{a\#\mathcal{I}^\Gamma\}\} \qquad \text{[CONST]} $$

$$ 4 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \text{ gensym}() :_a \{a\#\mathcal{I}^\Gamma\} \qquad \text{[APP], 2, 3} $$
**Example 2.** We reason about the comparison of two fresh names, clearly returning false, by applying Example 1 in the relevant LTCs.

<table><tr><td>1</td><td>Π ⊧ {T} gensym() :<sub>a</sub> {a#Π}</td><td>See Example 1</td></tr><tr><td>2</td><td>Π + a ⊧ {T} gensym() :<sub>b</sub> {b#Π + a}</td><td>See Example 1</td></tr><tr><td>3</td><td>Π + a ⊧ {a#Π} gensym() :<sub>b</sub> {a ≠ b}</td><td>[CONSEQ], (f3), 2</td></tr><tr><td>4</td><td>Π ⊧ {T} gensym() = gensym() :<sub>u</sub> {u = false}</td><td>[EQ], 3</td></tr></table>

**Example 3.** Placing name generation inside an abstraction halts the production of fresh names until the function is applied. When $y$ is of type Unit then this specification is identical to that of gensym.

<table><tr><td>1</td><td>Π + δ + y ⊧ {T} gensym() :<sub>m</sub> {m#Π + δ + y}</td><td>See Example 1</td></tr><tr><td>2</td><td>Π ⊧ {T} λy.gensym() :<sub>u</sub> {∀δ.∀y ∈ (δ).u • y = m{m#Π + δ + y}}</td><td>[LAM], 2</td></tr></table>

**Example 4.** Generating a name outside an abstraction and returning that same name in the function is often compared to Example 3 [1,17]. We reason as follows: letting $A_4(p) \stackrel{def}{=} \forall \delta. \forall y \in (\delta). u \bullet y = m\{m#\Pi \wedge p = m\}$.

<table><tr><td>1</td><td>{x#Π} x :<sub>m</sub> {m#Π ∧ x = m}</td><td>[VAR]</td></tr><tr><td>2</td><td>{x#Π} λy.x :<sub>u</sub> {A<sub>4</sub>(x)}</td><td>[LAM], 1</td></tr><tr><td>3</td><td>{x#Π} λy.x :<sub>u</sub> {∃x' ∈ (u).A<sub>4</sub>(x')}</td><td>[CONSEQ], 2</td></tr><tr><td>4</td><td>Π ⊧ {T} let x = gensym() in λy.x :<sub>u</sub> {∃x' ∈ (u).A<sub>4</sub>(x')}</td><td>[LETFRESH], 3</td></tr></table>

Proof of line 3 above, essentially proves $x$ is derivable from $u$:

<table><tr><td>5</td><td>A<sub>4</sub>(x) ∧ ∀y ∈ (∅).u • y = m{x = m}</td><td>(utc1), (u2), FOL</td></tr><tr><td>6</td><td>A<sub>4</sub>(x) ∧ ∃x' ∈ (u).x = x'</td><td>(ex2), (ex3)</td></tr><tr><td>7</td><td>∃x' ∈ (u).(A<sub>4</sub>(x) ∧ x = x')</td><td>(u3), (u4)</td></tr><tr><td>8</td><td>∃x' ∈ (u).A<sub>4</sub>(x')</td><td>(eq1)</td></tr></table>

**Example 5.** In order to demonstrate the subtlety of hidden names, the Introduction used Program (2), which was $M \stackrel{def}{=} \text{let } x = \text{gensym()} \text{ in } \lambda y.x = y$. We now use our logic to reason about $M$.
$$1 \quad \mathcal{I}^\Gamma + x + \delta + y \Vdash \{\mathcal{T}\} \quad x = y :_m \{m = (x = y)\} \qquad [\text{EQ}]$$

$$2 \quad \mathcal{I}^\Gamma + x \Vdash \{\mathcal{T}\} \quad \lambda y.x = y :_u \{\forall \delta. \forall y \in (\delta). u \bullet y = (x = y)\} \qquad [\text{LAM}], 1$$

$$3 \quad \mathcal{I}^\Gamma + x \Vdash \{x \# \mathcal{I}^\Gamma\} \quad \lambda y.x = y :_u \{x \# \mathcal{I}^\Gamma \wedge \forall \delta. \forall y \in (\delta). u \bullet y = (x = y)\} \qquad [\text{INVAR}], 2$$

$$4 \quad \mathcal{I}^\Gamma + x \Vdash \{x \# \mathcal{I}^\Gamma\} \quad \lambda y.x = y :_u \{\forall y \in (\mathcal{I}^\Gamma + u). u \bullet y = \text{false}\} \qquad [\text{CONSEQ}], 3$$

$$5 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \quad M :_u \{\forall y \in (\mathcal{I}^\Gamma + u). u \bullet y = \text{false}\} \qquad [\text{LETFRESH}]$$

$$6 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \quad M :_u \{\forall \delta. \forall y^{Nm} \in (\delta). u \bullet y = \text{false}\} \qquad (\text{utc2})$$

To prove line 4 above we apply the axioms as follows:

$$7 \quad \mathcal{I}^\Gamma + x + u \Vdash x \# \mathcal{I}^\Gamma \wedge \forall \delta. \forall y \in (\delta). u \bullet y = (x = y)$$

$$8 \quad x \# \mathcal{I}^\Gamma \wedge \forall y \in (\mathcal{I}^\Gamma + x + u). u \bullet y = (x = y) \qquad (\text{utc1})$$

$$9 \quad x \# \mathcal{I}^\Gamma + u \wedge \forall y \in (\mathcal{I}^\Gamma + x + u). u \bullet y = (x = y) \qquad (f1)$$

$$10 \quad x \# \mathcal{I}^\Gamma + u \wedge \forall y \in (\mathcal{I}^\Gamma + u). u \bullet y = (x = y) \qquad (u2)$$

$$11 \quad \forall y \in (\mathcal{I}^\Gamma + u). x \# \mathcal{I}^\Gamma + u + y \wedge u \bullet y = (x = y) \qquad (f2)$$

$$12 \quad \forall y \in (\mathcal{I}^\Gamma + u). x \neq y \wedge u \bullet y = (x = y) \qquad (f3)$$

$$13 \quad \forall y \in (\mathcal{I}^\Gamma + u). u \bullet y = \text{false} \qquad (e1)$$

**Example 6.** To demonstrate the release of a hidden variable using Program (3), which was $M \stackrel{\text{def}}{=} \text{let } x = \text{gensym}() \text{ in } \langle x, \lambda y.x = y \rangle$, we reason as follows, with $A_6(p, q) \stackrel{\text{def}}{=} p \# \mathcal{I}^\Gamma \wedge \forall \delta. \forall y \in (\delta). q \bullet y = (p = y)$:

$$1 \quad \{x \# \mathcal{I}^\Gamma\} x :_b \{x = b \wedge x \# \mathcal{I}^\Gamma\} \qquad [\text{VAR}]$$

$$2 \quad \{\mathcal{T}\} \lambda y.x = y :_c \{\forall \delta. \forall y \in (\delta). c \bullet y = (x = y)\} \qquad \text{See Example 4, lines 1-2}$$

$$3 \quad \{x = b \wedge x \# \mathcal{I}^\Gamma\} \lambda y.x = y :_c \{x = \pi_1(\langle b, c \rangle) \wedge A_6(x, c)\} \qquad [\text{CONSEQ}], [\text{INVAR}], 2$$

$$4 \quad \{x = b \wedge x \# \mathcal{I}^\Gamma\} \lambda y.x = y :_c \{A_6(\pi_1(a), \pi_2(a))[\langle b, c \rangle/a]\} \qquad [\text{CONSEQ}], (\text{eq1})$$

$$5 \quad \{x \# \mathcal{I}^\Gamma\} \langle x, \lambda y.x = y \rangle :_a \{A_6(\pi_1(a), \pi_2(a))\} \qquad [\text{PAIR}], 1, 4$$

$$6 \quad \mathcal{I}^\Gamma \Vdash \{\mathcal{T}\} \quad M :_a \{A_6(\pi_1(a), \pi_2(a))\} \qquad [\text{LETFRESH}], 5$$

## 8 Conclusion

We have presented the first program logic for the $\nu$-calculus, a variant of the STLC with names as first class values. Our logic is a conservative extension with two new universal quantifiers of the logic in [9] for the STLC. We provide axioms
and proof rules for the logic, prove their soundness, and show its expressive power by reasoning about well-known difficult examples from the literature.

We are currently unable to reason about this example from [16]:

$$ 
\begin{array}{l}
\texttt{let } F = (\texttt{let } x, y = \texttt{gensym()} \texttt{ in } \lambda f^{\text{Nm}} \rightarrow \text{Nm}.fx = fy) \texttt{ in} \\
\texttt{let } G = \lambda v^{\text{Nm}}.F(\lambda u^{\text{Nm}}.v = u) \texttt{ in } FG
\end{array}
$$

Is this because our logic is too inexpressive, or did we simply fail to find the right proof? Another open question is whether our logic's approach to freshness is independent of the $\nu$-calculus's lack of integers and recursion, or not? For both questions we conjecture the former, and leave them as future work.

## References

1. Benton, N., Koutavas, V.: A Mechanized Bisimulation for the Nu-Calculus. Tech. Rep. MSR-TR-2008-129, Microsoft (2008)

2. Berger, M., Tratt, L.: Program Logics for Homogeneous Generative Run-Time Meta-Programming. Logical Methods in Computer Science (LMCS) 11(1:5) (2015)

3. Berger, M., Tratt, L., Urban, C.: Modelling Homogeneous Generative Meta-Programming. In: Proc. ECOOP. pp. 5:1-5:23 (2017)

4. Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. In: Proc. ICFP. p. 143-156 (2010)

5. Elliott, H.P.: Program Logic for Fresh Name Generation. Ph.D. thesis, University of Sussex (expected 2021), draft.

6. Fernández, M., Gabbay, M.J., Mackie, I.: Nominal Rewriting Systems. In: Proc. PPDP. p. 108-119 (2004)

7. Gabbay, M.J., Pitts, A.M.: A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13, 341-363 (2001)

8. Honda, K.: Elementary structures in process theory (1): Sets with renaming. MSCS 10(5), 617-663 (2000)

9. Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: Proc. PPDP'04. pp. 191-202. ACM Press (2004)

10. Mendelson, E.: Introduction to Mathematical Logic. Wadsworth Inc. (1987)

11. Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, Parts I and II. Information and Computation 100(1) (1992)

12. Odersky, M.: A Functional Theory of Local Names. In: Proc. POPL. pp. 48-59 (1994)

13. Pierce, B.C.: Types and Programming Languages. MIT Press (2002)

14. Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165-193 (2003)

15. Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. CUP (2013)

16. Pitts, A.M., Stark, I.D.B.: Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new? In: MFCS (1993)

17. Stark, I.: Names and Higher-Order Functions. Ph.D. thesis, University of Cambridge (1994), technical report 363, Univ. of Cambridge Computer Laboratory

18. Urban, C., Tasson, C.: Nominal Techniques in Isabelle/HOL. In: Proc. CADE. p. 38-53 (2005)

19. Yoshida, N., Honda, K., Berger, M.: Logical Reasoning for Higher-Order Functions with Local State. Logical Methods in Computer Science 4(2) (2008)