Explicit and Controllable Assignment Semantics
Dimitri Racordon Didier Buchs
cs.PL D.3.3



Despite the plethora of powerful software to spot bugs,
identify performance bottlenecks or simply improve the overall quality of code,
programming languages remain the first and most important tool of a developer.
Therefore, appropriate abstractions, unambiguous syntaxes and intuitive semantics are paramount
to convey intent concisely and efficiently.
The continuing growth in computing power has allowed
modern compilers and runtime system to handle once thought unrealistic features,
such as type inference and reflection,
making code simpler to write and clearer to read.
Unfortunately, relics of the underlying memory model still transpire in most programming languages,
leading to confusing assignment semantics.

This paper introduces Anzen, a programming language that aims to
make assignments easier to understand and manipulate.
The language offers three assignment operators, with unequivocal semantics,
that can reproduce all common imperative assignment strategies.
It is accompanied by a type system based on type capabilities to enforce uniqueness and immutability.
We present Anzen's features informally and formalize it by the means of a minimal calculus.




<ccs2012>
<concept>
<concept_id>10011007.10011006.10011008.10011009.10011010</concept_id>
<concept_desc>Software and its engineering Imperative languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011008.10011024</concept_id>
<concept_desc>Software and its engineering Language features</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011039</concept_id>
<concept_desc>Software and its engineering Formal language definitions</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011041</concept_id>
<concept_desc>Software and its engineering Compilers</concept_desc>
<concept_significance>100</concept_significance>
</concept>
</ccs2012>


[500]Software and its engineering Imperative languages
[500]Software and its engineering Language features
[300]Software and its engineering Formal language definitions
[100]Software and its engineering Compilers



Probabilistic Approximate Logic 
 and its Implementation 

	in the Logical Imagination Engine
    
	Mark-Oliver Stehr1 Minyoung Kim 1 
 
	Carolyn L. Talcott1 Merrill Knapp1 Akos Vertes2 

    April 2019
=============================================================================================





§ INTRODUCTION


Writing software programs is a difficult task.
Moreover, with the dissemination of computer-based technology in all domains, this endeavor is no longer reserved for computer experts.
Consequently, good language design is essential to the production and maintenance of software.
Thanks to the continuing growth in computing power, contemporary programming languages can sit at very high levels of abstractions, letting developers convey their intent with great expressiveness.
Unfortunately, this evolution also brings the potential for more inadvertent behaviors, as the small imperfections in these many layers of abstractions usually have deep consequences on a language's semantics.
This is particularly true for the imperative paradigm, in which the interplay between variables and memory can prove to be a prolific source of puzzling bugs.
For instance, most mainstream object-oriented programming languages have a limited support to express aliasing explicitly, blurring the distinction between object mutation and reference reassignment, and often leading to erroneous assumptions about sharing and immutability.

This paper introduces Anzen, a multi-paradigm programming language that aims to dispel the confusion that surrounds assignment semantics.
Rather than overloading a single assignment operator with different meanings, depending on its operands' types, Anzen provides three distinct operators with unequivocal semantics.
One creates aliases, another performs deep copies and the last deals with uniqueness.
The language further supports high-level concepts, such as generic types and higher-order functions,
and offers capability-based <cit.> memory and aliasing control mechanisms that are enforced by its runtime.
We present Anzen's features informally, by the means of various examples,
and describe its operational semantics formally.
A compiler and interpreter for Anzen are distributed as an open-source software and available at <https://github.com/anzen-lang/anzen>.


§ BACKGROUND AND PROBLEMATIC



In the imperative paradigm, computation is described by sequences of instructions that define how a program operates.
These instructions interact with the state of the program,

whose modifications are expressed by memory assignments.
A memory assignment is a statement of the form “x  v" that instructs the machine to write (i.e. assign) a value to a specific location in the memory.
Here, x is a variable representing a memory address and v is a value.
Programming languages can express vastly different data types, ranging from numbers to more abstract data structures (e.g. a binary tree).
For example, v could denote a number and be stored in memory as a simple sequence of bits, but could also denote a dynamic list represented by multiple  structures chained together.
It follows that the actual semantics of “" has to deal with data representation and properties thereof.

A language only describes programs, whereas their executions are driven by a runtime system that is responsible to process each instruction.
This means that the details of data representation can be eluded at the language level, as long as sufficient information can be derived by the runtime system to actually operate the machine's memory.
Most systems have evolved to divide their memory into a stack, to store local (w.r.t. a function call), small and fixed-sized values, and a heap, to store long-lived and arbitrarily-sized data.
A variable is merely a name denoting an address in the stack,
meaning that it cannot directly refer to heap-allocated objects.
However, addresses thereof are essentially represented as numbers, and therefore do fit into the stack.
This means that heap-allocated values are always manipulated through pointers.
Modern programming languages (e.g. Python or Javascript) are able to hide these implementation constraints so that no distinction has to be made between stack and heap allocated objects.
Thus, a variable can be seen as a container for a value of some kind, without any regard for where this value is stored.




Unfortunately, most execution models do not preserve this abstraction when dealing with assignments, which are implemented as a straightforward “bitwise copy" of the stack-allocated value a variable represents.
Consequently, values stored on the stack get fully copied, whereas values stored on the heap and referred to by a pointer get aliased,
since only the their pointers' values are copied.
<Ref> illustrates both cases.
Although this strategy is efficient and usually matches the developer's intent, it may leads to confusing situations, in particular when mutation is involved.
Consider for instance the two Python snippets below.
On the left, the variable |a|'s value is copied.
Therefore its mutation at line 3 does not impact |x|'s value.
Conversely on the right, the variable |a| represents a heap-allocated dynamic array, whose pointer is copied at line 3.
Consequently the mutation at line 3 also impacts the value that |x| represents.

[
colback=white, frame hidden, left=0pt, right=0pt, boxrule=0pt, frame code=, lower separated=false, sidebyside, sidebyside gap=3mm]
[language=python]
a = 4
x = a
a += 2
print(a, x)
# 6 2

[language=python]
a = [4]
x = a
a += [2]
print(a, x)
# [4,2] [4,2]



Another assignment strategy that has gained popularity in recent years is to “move” values from one variable to another, thereby avoiding any copy or alias creation.
The advantages of this so-called move semantics are twofold.
On the performance front, it allows efficient return-by-value implementations by eluding unnecessary copies <cit.>.
On the memory safety front, it allows to preserve uniqueness, thereby guaranteeing data-race safety <cit.>.
For example, the Rust programming language adopts this approach as its default assignment semantics.
However, since the language can fall back to copy semantics for certain data types, it also bears the potential for similar confusing situations.

We argue that the problem does not reside in the support of multiple assignment strategies in the same programming language.
On the contrary, those allow to better express intent and offer a tighter control over memory.
Instead, the source of the confusion stems from overloading a single operator with different semantics, defined implicitly by the type of its operands, in order to cater for the abstraction of pointers.
This comes with several important drawbacks:

  
  * This steepens the learning curve for beginners, as aliasing consistently appear as a difficult aspect of programming <cit.>.
  
  * This increases the risk of errors in code refactoring, as seemingly identical statements can have different side-effects.
  
  * This hinders the control over pointers, as purposely creating aliases on stack-allocated values often requires to wrap them in heap-allocated objects, thereby reimplementing the abstraction.

A better approach would be to support these different strategies explicitly, in order to let the developer choose the most appropriate one and express her intent unambiguously.



§ THE ANZEN PROGRAMMING LANGUAGE



Anzen is a typed general purpose language that aims to make assignment semantics explicit.
Although it supports multiple paradigms, Anzen leans towards object orientation and imperative programming.
We introduce the language and its features with a series of examples.



 §.§ Assignment Semantics


Anzen's most distinguishing characteristic is that it features three different assignment operators.
These are independent of their operands' types and provide the following strategies:

  
  * An aliasing operator  assigns an alias on the object on its right to the reference on its left.
    Its semantics is the closest to what is generally understood as an assignment in languages that abstract over pointers (e.g. Python or Java).
  
  * A copy operator  assigns a deep copy of the object's value on its right to the reference on its left.
    If the left operand was already bound to an object, the copy operator mutates its value rather than reassigning the reference to a different one.
  
  * A move operator  moves the object on its right to the reference on its left.
    If the right operand was a reference, the move operator removes its binding, effectively leaving it unusable until it is reassigned.




<Ref> illustrates the three assignment semantics.
Notice that we use the term “memory” rather than “stack” or “heap”.
The reason is that we aim at making a clear distinction between the semantics of Anzen's operators and the actual memory model that is used to implement them.
Whether a reference is a pointer to heap-allocated memory or a simple value allocated on the stack should be irrelevant for the developer.
That way she may focus solely on the semantics of her program, at an abstraction level that does not bother about the specifics of compilation, optimization and/or interpretation.



 §.§ Parameter Passing


There is a tight connection between reference assignments and the passing of parameters in a function call <cit.>, as one can see a parameter as a mere variable assigned to a corresponding argument.
Consequently, just as most runtime systems implement assignments as a straightforward “bitwise copy”, they often do the same for function parameters, which are passed as a bitwise copy the argument's value.
This makes sense from an implementation perspective, as it preserves the symmetry with assignment semantics.
Unfortunately, it may also cause similar confusing situations as those we described in <Ref>.

For instance, although it is technically correct to state that Java adopts a pass-by-value semantics, as mentioned in the language manual <cit.>, the observable behavior is a pass-by-alias (a.k.a. pass-by-reference) for all heap-allocated objects, as mutating such parameters do have side effects on the call site.
Anzen fends off this issue by reusing its three assignment operators to specify the parameter passing strategy explicitly.
The use of an aliasing operator corresponds to a pass-by-alias, while the use of a copy operator corresponds to a pass-by-value policy. Unsurprisingly, the move operator also treats objects as linear resources, and therefore mimics Rust's move semantics.
An example follows:

[language=anzen]title=Parameter passing
fun f(list: @mut List<Int>) 
  list.append(new_element <- 5)
  print(line <- list)


var a: @mut <- List<Int>()
a.append(new_element <- 4)

// `a` is passed by value, therefore the
// mutation of the `list` parameter in
// `f`'s body have no side effects.
f(list := a)
// Prints "[4, 5]"

print(line <- a)
// Prints "[4]"


 Reusing the assignment operators makes the relationship between assignment and parameter passing explicit, which we believe to be beneficial for educational purposes.
 Even the induced syntactic overhead may in fact be seen as an improvement.
 Indeed, whereas it is traditional to identify parameters by their position, one can leverage named parameters to improve the legibility of the code. For instance, the expression |iter(from <- 0, by_steps_of <- 2)| is arguably more self-explanatory than |iter(0, 2)|.
 This peculiarity is often referred to as “named parameters” in other languages (e.g. in Python).

 For the sake of code legibility, arithmetic operators support an infix notation, that assumes a pass-by-value strategy for each operand.
 For example, the expression |2 + 3| is a syntactic sugar for |Int.+(lhs := 2, rhs := 3)|.

 

 §.§ Data Types


 On the top of a handful of primitive types to describe numbers and boolean values, Anzen also supports custom type definitions in the form of structures.
 A structure is an aggregate of named fields, which represent references to other values.
 Borrowing from object-oriented programming languages, methods, constructors and destructors can be declared along with a structure to compartmentalize behavior.
 Inside these functions, a reserved |self| reference allows access to the instance's internals.
 The language does not however support inheritance and polymorphism.














Anzen is a higher-order programming language.
Any identifier that is neither a parameter nor a variable declared within the function's body is captured by closure.
Captured identifiers are in fact aliases on the corresponding variables in the function's declaration context.
It follows that mutating their values will also modify the value within the closure.





















§ ALIASING CONTROL MECHANISMS


Anzen's type system offers some aliasing control mechanisms to enforce uniqueness and immutability at runtime.
This section introduces them informally.



 §.§ Ownership and Uniqueness


Uniqueness <cit.> is a property of a reference that holds if there are no other references (i.e. aliases) on the object to which it is bound.
In order to avoid dangling references, the right operand of a move operator has to be unique,
otherwise aliases would refer to a moved object.
Therefore Anzen's type system has to keep track of reference uniqueness.
This is achieved by the means of a typestate analysis <cit.>.


We first define a notion of object ownership.
A reference is said to bear ownership on the object to which it is bound if it has been initialized using either the copy or the move operator.
Notice that this means an owning reference has necessarily been unique at least once during the program's execution.
Then, we define the following five reference states:
the unallocated state denotes references that are not bound to any object,
the unique state denotes owning references to unaliased objects,
the shared state denotes owning references to aliased objects,
the borrowed state denotes non-owning references, and
the moved state denotes references that have been moved.






<Ref> summarizes how these transitions can take place.
Each cell represents the state in which a reference goes if placed on the left or right side of the operator indicated by the column.
The position of the bullet denotes the side of the operator on which the reference should be.
For instance, ∙ denotes the left operand of a copy assignment.
An example follows:

[language=anzen]title=State transitions
var a, b, c: Int
// `a`, `b` and `c` start unallocated
a := 10
b <- 20
// `a` and `b` get unique
c    - a
// `a` gets shared, `c` gets borrowed
c    - b
// `b` gets shared, `a` gets unique
b <- a
// `a` gets moved




Uniqueness is treated as a fractionable capability, reminiscent to Boyland's proposal <cit.>.
The intuition is that it is initially obtained in full at allocation, but gets fractioned for each alias.
The loss of the uniqueness capability is only temporary, as an owner can later gather all fragments back to rebuild it.
Put another way, each aliasing assignment creates a new fragment of uniqueness, while one is sent back to its owner every time an alias goes out of scope or is reassigned.
Aliases themselves are allowed to further fraction their fragment to allow additional aliases.
However this does not create a hierarchy, and a fragment is always directly sent back to its owner.
This mechanism effectively implements borrowing and reborrowing <cit.>.

As the tracking of uniqueness fragments is performed at runtime, our model does not require an elaborate pointer analysis and does not have to deal with statically nondeterministic situations (e.g. conditional expressions).
Instead the mechanism can be implemented by the means of a simple table associating references to capabilities at runtime.
Incidentally, this explains why shared references cannot be reassigned by alias.
The restriction guarantees that borrowed references can properly return their uniqueness fragment, without any additional bookkeeping.



 §.§ References and Mutability


The term “immutability” can be a placeholder for vastly different concepts, depending on the programming language.
We briefly describe them to establish the vocabulary we use in the remainder of this paper.
A more comprehensive discussion about immutability is given in <cit.>.


  
  Non-reassignability
    is a property of references, indicating that they cannot be reassigned to another object after having being assigned once.
    This is the most common form of immutability found in programming languages that abstract over heap memory management (e.g. Javascript's [language=javascript]|const| or Java's [language=java]|final|).
  
  Reference immutability
    is a property of references, indicating that the object to which they refer cannot be modified through them.
    In other words, an immutable reference is an alias through which the object's mutation is not allowed.
  
  Object immutability
    is a property of objects, indicating that they cannot be modified, by any reference.
    The property can be applied on the bits that constitute the object only, or also transitively applied to the other objects to which it refers.
    The former strategy, called shallow immutability, only prevents fields from being reassigned, whereas the latter, called deep immutability, freezes the entire object's representation.


Anzen supports non-reassignable references and deep object immutability.
Non-reassignable references are declared with the keyword |let|, whereas reassignable references are declared with the keyword |var|.
Object immutability on the other hand is specified with type qualifiers.
|@cst| describes immutable values whereas |@mut| describes a mutating one.
We say that a reference to an immutable (resp. mutable) object is non-mutating (resp. mutating).
<Ref> illustrates all possible combinations of reassignability and object immutability.
Anzen chooses to always prefer immutability over mutability.
Accordingly, omitting the mutability qualifier is interpreted as a |@cst| by default, and parameters are always assumed non-reassignable.



Reassignability is checked statically, meaning that reassigning a reference declared with |let| or a function parameter is rejected during compilation.
On the contrary, object mutability is checked dynamically, meaning that modifying an immutable object triggers an error during execution.

[language=anzen]title=Immutability
let a: @cst <- 42
a := 10
// At runtime: `a` is not mutating

let b: @cst <- 1337
a    - b
// At compilation: `a` is not reassignable


The type system guarantees that mutating references cannot coexist with non-mutating references on the same object.
However, unlike in most systems, there is no restriction on the number of mutating references.
The reasons are twofold.
Firstly, this allows mutable self-referential data structures to be expressed naturally, whereas such an exercise can prove challenging in more constrained type systems <cit.>.
Secondly, Anzen is currently single-threaded, and therefore not susceptible to data races in the presence of multiple mutating references.
Single-threading does not discard concurrency, which is planned to be implemented by the means of cooperative multitasking <cit.> in a future language extension.
Cooperative multitasking differs the more widespread preemptive counterpart in that control is transferred voluntarily between concurrent processes, offering synchronization for free and therefore avoiding data race issues.

Mutual exclusion of mutating and non-mutating references is achieved by associating them with additional capabilities.
Two are defined: the read-write and the read-only capabilities.
At initialization non-mutating references (i.e. those annotated with |@cst|) receive the read-only capability,
whereas mutating references (i.e. those annotated with |@mut|) receive both.
Mutability capabilities are borrowed with the aliasing operator (i.e. |   -|).
In order to avoid inconsistent situations, aliasing is only allowed in two situations:

  
  * If the left operand's type is qualified by |@mut|, the right operand should be mutating and not aliased by non-mutating references.
  
  * If the left operand's type is qualified by |@cst|, the right operand should be non-mutating and/or unique.

The latter case allows unique mutating references to be shared non-mutating temporarily (e.g. for the duration of a function call).
Recall that mutating references receive both mutability capabilities upon allocation.
Hence they can lend the read-only capability to a non-mutating alias, and refrain from using their read-write capability for the duration of the loan.
An alias only holds the capability it borrows, thus preventing it to be reborrowed with an incompatible mutability.
The reader will notice that this model shares a few similarities with the notion of uniqueness that we have discussed in the previous section.
Unique references fraction either of their mutability properties when aliased,
and these fragments are sent back their owner when borrowed references are either reassigned or go out of scope.

|self| is always a non-reassignable reference, but whether or not it designates an immutable object depends on the method's declaration.
By default, methods cannot mutate their internals via |self|, but their definition can be prefixed with |mutating| to turn |self| into a mutating reference.
Object immutability is applied transitively.
In oder words, mutating a field of an immutable structure instance is an illegal operation, and provokes an error at runtime.
Consequently, calling a mutating method on a reference that is not typed with |@mut| is forbidden, as demonstrated below:

[language=anzen]title=Deep immutability
struct Point 
  // ...
  mutating fun move_x(dx: Float) 
    self.x <- self.x + dx
  


let pt: @cst <- Point(x <- 1.0, y <- 1.0)
// `pt` is declared non-mutating
pt.move_x(dx <- 3.14)
// At runtime: `pt` is not mutating




 §.§ Restrictions for Code Legibility


The mechanisms that we have described so far are sufficient to keep track of uniqueness and immutability at runtime.
However, performing the same task can prove very difficult for a developer, since our model offers a very limited syntactic support to determine where uniqueness and immutability properties are obtained, lost and retrieved.
To remedy this situation, we add a few restrictions and annotations to help the developer infer the references' typestate transitions.

First, functions and method signatures must be annotated to specify arguments and return values' expected ownership.
The |@own| qualifier denotes and is assumed by default, while the |@brw| qualifier denotes borrowed references.

The runtime system raises an error if they are not honored.
For instance, the result of a call to a function whose codomain is annotated with |@own| should be safely consumed by move.
Consequently, returning a value by alias in such a function is illegal.

[language=anzen]title=Ownership annotations
fun f(x: @own Int) -> @own Int 
  return    - x
  // At runtime: return value must be
  // passed with ownership



We also prevent functions from forming aliases on their arguments, unless those are annotated with |@esc|.
This mechanism is used to prevent a function from implicitly creating a non-mutating reference on an argument that would live longer than the function call, as this would hinder the ability of a developer to determine when uniqueness and mutability can be expected to be recovered.
The constraint applies on values returned by alias and on aliases formed on captured identifiers.
Note that escaping parameters are necessarily expected to be passed by alias.

[language=anzen]title=Escaping annotations
var i <- 0
fun f(x: @brw Int, y: @esc Int) 
  if x > y 
    i    - x
    // At runtime: `x` cannot escape
   else 
    i    - y
    // Perfectly legal
  



Another restriction prevents methods from returning non-mutating references on mutating fields.
As non-mutating references can assume the object to which they refer remains immutable for its entire lifetime, any mutation of the aliased field has to be forbidden.
However, there is no way to “see” where the non-mutating borrowing took place or where it ends from within a method.
Consequently, it also follows that a method cannot pass an alias to a mutating field to a parameter annotated with |@esc|.
The restriction is enforced on |self| as well, for the same reason.



§ EXAMPLE


We now present an example of Anzen's use to showcase the advantages of its unambiguous assignment semantics and of its aliasing control mechanisms.
We use the so-called “Signing Flaw” security breach of JDK 1.1 as a point of reference.
In Java, all class instances (i.e. instances of |java.lang.Class|) hold an array of signers, which acts as digitally signed identities that Java's security architecture uses to determine the class' access rights at runtime.
The value of this array can be obtained by calling |java.lang.Class.getSigners|.
Before the breach was discovered, the method used to simply return an alias on its array of signers.
Because the returned array was an alias, an untrusted applet could freely mutate it and add trusted signers to its class, therefore fooling the security system into giving it access to restricted code signed by a trusted authority.
The following listing is an excerpt of the flawed implementation:

[language=java]title=Flawed implementation
public class Class 
  public Identity[] getSigners() 
    return this.signers;
  
  private Identity[] signers;



Note that none of the standard protection mechanisms of Java can help solving this issue <cit.>.
Although the property is declared private, its reference is exposed through a method, which breaks the encapsulation principle.
Using Java's non-reassignability (i.e. using Java's [language=java]|final| keyword) would not be of any more assistance.
While it would prevent the property from being reassigned, it would not impose any restriction on the array object itself which, consequently, could still be freely mutated.

There are two ways to prevent this situation in Anzen[
Admittedly, Anzen does not currently support access modifiers (e.g. private), therefore the language is unable to protect the object's internal representation and forbid a direct access to the field.
We only describe protection mechanisms on the method's return value.].
The first is to return a deep copy of signers's value by the means of the mutation operator, therefore removing any potential alias to the internal representation.

[language=anzen]title=Using copies
struct Class 
  fun get_signers()
    -> @mut List<Identity>
  
    return := self.signers
  
  let signers: @mut List<Identity>



The drawback of this first approach is that it involves a deep copy, potentially expensive in terms of time and/or space.
Although optimization techniques such as copy-on-write <cit.> can alleviate this issue, a better angle would be to use a non-mutating alias.
However, as returning non-mutating aliases on mutating fields is prohibited, one cannot simply return |signers| by alias (i.e. replacing |:=| with |   -| at line 5 in the above example).
Instead, one solution is to rely on Anzen's support for higher-order functions and generic types to inverse control, and accept a function that manipulates an immutable reference to the field.
That way, the non-mutating alias can be guaranteed not to escape the method's scope.

[language=anzen]title=Using non-mutating references
struct Class 
  fun do_with_signers<R>(
    f: (s: @brw List<Identity>) -> @own R)
    -> @own R
  
    return <- f(s    - self.signers)
  
  let signers: @mut List<Identity>


let class = Class(signers <- List())
let count <- class.do_with_signers(
  f <- fun(s)  return <- s.count )
print(line <- count)
// Prints "0"


In the above example, the method |do_with_signers| accepts a parameter |f| that is a higher-order function taking a non-mutating reference on a list of identities.
It is called within |do_with_signers|, which passes it a non-mutating reference on the |signers| field.
Since the argument |s| is not escaping, the non-mutating loan of the field is guaranteed to end once the function returns.
Notice that the method has a generic parameter |R|, which types its codomain and that of the higher-order function.
This allows the former to be agnostic of the latter's return value.
The |@own| on |f|'s codomain guarantees that the move operator at line 6 is safe.
The method is called with an anonymous function at line 12 that reads and returns the number of signers in the list.


§ THE A-CALCULUS


We model Anzen with a minimal calculus based on a variant of the λ-calculus with assignments <cit.>, which we extend with terms specific to the assignment operators we presented in <Ref>.
We call such model the 𝒜-calculus (pronounced assignment calculus).
Programs are expressed by a single term t ∈, where  is the set of 𝒜-calculus' terms.

For spatial reasons, we focus on the mechanisms that are necessary to track uniqueness and object immutability.
Hence we fo not formalize reference reassignability, nor the restrictions for code legibility.



  
*Notations
Before we delve into the syntax and semantics of the 𝒜-calculus, we first describe the notations we will use throughout this section.
Let Σ be a set of letters, Σ^* denotes the set of all words over Σ.
Let w∈Σ^* be a word, w_s denotes the the number of occurrences of a letter s in w (e.g. aab_a = 2).
We write Σ^#⊆Σ^* the set of words over Σ without repetition.
That is w∈Σ^#⇔∀ s ∈Σ, w_s ≤ 1.
We write w_1 + w_2 the concatenation of two words and we write ϵ for the empty word.
Let f be a function, (f) and (f) denote its domain and codomain, respectively.
The notation f: A → B denotes a total function from a domain A to a codomain B.
The notation g: A  B denotes a partial function, characterized by (f) ⊆ A.
We overload the empty set symbol ∅ to denote partial functions with empty domains.
Let A = { a_1 … a_n } be a set of pre-images and { b_1 … b_n }⊆ B be a set of images.
The notation a_1 ↦ b_1 … a_n ↦ b_n denotes a function f: A → B such that ∀_i=1^n, f(a_i) = b_i.
Similarly, let the notation { a_i ↦ b_i … a_j ↦ b_j } denotes a partial function f: A  B such that 1 ≤ i ≤ j ≤ n { a_i … a_j }⊆ A.
We borrow the so-called “dot-notation” from object-oriented programming language and sometimes write f.a short for f(a).
Let f be a (total or partial) function from A to B, we write f[a ↦ b] the update of f, which is a function that maps a to b but x to f.x for any other x ∈(f).
More formally:

    ∀ x ∈(f), f[a ↦ b] = 
      b    if  x = a 
    
      f.x    otherwise

We sometimes write updates by intension.
For instance, the notation f[a ↦ b | p(b)] denotes an update for each pre-image a satisfying a predicate p.
Let f be a (total or partial) function whose codomain is another (total or partial) function.
We write f[a.b ↦ c] short for f[a ↦ f.a[b ↦ c]].



 §.§ Types


The type of a term describes two kind of information.
One relates to the data type the term represent (e.g. numbers).
We call this information flow-insensitive, since it does not depend on the evaluation context at runtime.
The other relates to typestate.
It is of course linked to the evaluation context, and is therefore termed flow-sensitive.
Formalizing well-typedness with respect to flow-insenstive typing is beyond the scope of this paper.
For a language as simple as the 𝒜-calculus, this fits the standard Hindley-Milner system <cit.>.
Nonetheless, type signatures are required to type check uniqueness and immutability constraints.


  The set of type qualifiers is given by = _R ∪_M, where:
  
    
  * _R = {, } denotes reference qualifiers, and
    
  * _M = {, } denotes mutability qualifiers.
  



  A set of qualifiers Q ∈() is well-formed if it contains exactly one reference qualifier and exactly one mutability qualifier.



  Assume a set of primitive values (e.g. numbers and booleans), written .
  Assume a countable set of  identifiers, written .
  The set of types  is defined recursively as the minimal set such that:
  
    
  * q ↦ Q, t ↦∈ is an atomic type, where Q ∈() is a well-formed set of qualifiers.
    
  * q ↦ Q, t ↦dom → X →, codom →∈ is a function type, where Q ∈() is a well-formed set of qualifiers and X ⊆ is a set of parameter names.
    
  * q ↦ Q, t ↦ X →∈ is a structure type, where Q ∈() is a well-formed set of qualifiers and X ⊆ is a set of field names.
    
  * μα.τ is a recursive type, where τ∈.
  




 §.§ Abstract Syntax



  Let  be the set of atomic literals and  be the set of identifiers.
  Let = {,   ,   } denote the set of assignment operators.
  The set of terms  is defined recursively as the minimal set such that:
  
    [                         a             ∈, where  a ∈;                         x             ∈, where  x ∈;                       t.x         ∈, where  t ∈ x ∈;                         τ               ∈, where τ∈;                      x:τt       ∈, where  x ∈τ∈ t ∈;                  λ:τ x∙ t       ∈, where τ∈x∈^# t ∈;                      x  t        ∈, where ∈ x ∈ t ∈;                t_1.x  t_2 ∈, where ∈ x ∈ t_1, t_2 ∈;                      t(u)    ∈, where  t ∈u∈ (××)^#;                         t            ∈, where ∈ t ∈;                 t_1t_2t_3 ∈, where  t_1, t_2, t_3 ∈;                 t_1 ; t_2      ∈, where  t_1, t_2 ∈ ]




















All functions are anonymous but can be assigned to variables.
For instance we write ff λ:τ x▹ t to bind the variable f to a function.
Consequently, recursion must be expressed by the means of the Y combinator.
We do not deal with name shadowing.
Instead we assume that all identifiers are declared only once in a given lexical scope.

Scopes are delimited implicitly.

Variables cannot be declared and bound to a value at the once.
Instead, variable declarations merely introduce a name into a new scope, in which initialization must be carried out.
We use parenthesis liberally to delimit scopes and clarify precedence.
Otherwise, sequences of terms are always assumed to be declared in the innermost scope, for instance both assignments are enclosed in the function's body in λ:τ x ∙ x  2; x  3.
Function application is left associative, for instance f(x  1)(y  2)(z  3) = (f(x  1)(y  2))(z  3).
In contrast, the sequence operator ; is right associative, that is t_1 ; t_2 ; t_3 = t_1 ; (t_2 ; t_3).

We bring the reader's attention on the fact that return expressions are made explicit.
This is a departure from most variants of λ-calculi (and functional languages in general), in which return values typically correspond the evaluation of a function's body.
We cannot take the same direction, because our syntax needs to make the return policy explicit, by the means of our assignment operators.
Furthermore, although a sequences of return statements are not syntactically ill-formed, the actual return value of a function is defined by the last return statement it executes. For instance, the function λ:τ∙ 1 ;  2 always returns 2 by move.
In other words, a function never “returns early” and instead ignores non-final return statements.



 §.§ Operational Semantics


Unlike most variants of λ-calculi, the 𝒜-calculus has to factor the presence of memory into the evaluation of a term, because it has to distinguish between values and references thereupon.
Moreover, as we need to assign capabilities to references, we need a mechanism to identify the latter uniquely.
We achieve this using two levels of indirections.
References are uniquely identified by a reference identifier, which refers to memory location at which semantic values are stored.
Note that reference identifiers cannot be substituted with variable identifiers, because we need to identify anonymous references resulting from function calls or the dereferencing of a record field.
So as to avoid formalizing value representation beyond the strict necessary, with respect to assignment semantics, we neglect data sizes and we assume that a location can hold an arbitrary large value.
We make two additional assumptions on the memory model.
First, we consider memory as an infinite resource, and do not formalize allocation failures.
Second and more importantly, we do not distinguish between heap and stack, and assume memory to be automatically garbage collected.

We define the set of semantic values  that describes the data a program may manipulate.
This set includes atomic values, functions and structure instances (a.k.a. records).
While we do treat functions as first-class citizens, we do not let them capture identifiers by closure.
An important consequence of this restriction is that our calculus does not support partial application.
Instead, this can be emulated by the use of functors <cit.>.


  Assume an unbounded set of reference identifiers .
  Let  be the set of atomic literals,  be the set of identifiers and  be the set of types.
  The set of semantic values  is given by the minimal set such that:
  
    
  * ∈ is an undefined value.
    
  * a ∈ a ∈ is an atomic value.
    
  * (X ↦) ∈ is a record, mapping field names from X ⊆ to reference identifiers.
    
  * λ:τ x∙ t ∈ is a function, where τ∈, x∈^# and t ∈.
  



  Let  be the set of reference identifiers.
  The set of type capabilities  is defined as follows:
  
    
  * 𝐫𝐨∈ denotes the read-only capability.
    
  * 𝐫𝐰∈ denotes the read-write capability.
    
  * 𝐛[r] ∈ denotes the borrowing capability, where r ∈ is the reference owning the referred location.
  



  Assume an unbounded set of locations .
  Let  denote semantic values,
  an evaluation context C is function with a domain {ν, ρ, μ, κ}, where:
  
    
  * C.ν: is a table mapping variable names to reference identifiers.
    
  * C.ρ: is a table mapping reference identifiers to memory addresses.
    
  * C.μ: is a table mapping locations to values.
    
  * C.κ: () is a table mapping reference identifiers to set of type capabilities.
  


Let C be a given context, we refer to C.ν as its variable table, to C.ρ as its reference table, to C.μ as its memory table and to C.κ as its capability table.
We say that a context is empty if all its tables are empty (i.e. partial functions with an empty domain).
Furthermore, we use 0 ∈ to represent the null pointer.

We can finally give the operational semantics of the 𝒜-calculus, by the means of big-step inference rules.
All conclusions are of the form Γ, C ⊢ t ⇓ r, C', where C and C' are the evaluation contexts before and after evaluating the term t, respectively, r ∈ is the reference identifier to which the term t evaluates and Γ: is a function that maps terms to their flow-insensitive type.



  §.§.§ Variables Declarations and Dereferencing

As mentioned earlier, variable declarations do not assign anything to the identifier being declared.
Instead, declarations only consist in associating the variable being declared with a new reference identifier, with no capabilities.


  [E-Let] 
    r_x ∉(C.ν) 

    Γ, C[ν.x ↦r_x][ρ.r_x ↦0][κ.r_x ↦∅] ⊢t ⇓r, C'
  
    Γ, C ⊢x:τt ⇓r, C'
  


Dereferencing a variable consists in consulting the variable table to find the corresponding reference identifier.


  [E-Var] 
    x ∈(C.ν)
  
    Γ, C ⊢x ⇓C.ν.x, C
  




  §.§.§ Assignment Semantics

The advantage of evaluating all expressions as reference identifiers emerges when formalizing the assignment operators, whose semantics can be expressed purely in terms of reference and memory table updates.

We define a handful of predicates to facilitate the formalization of the type system's constraints.
Given a two reference identifiers r, s and an evaluation context C,
a predicate contains(s, r, C) indicates whether s denotes a record containing r,
a predicate readable(r, C) indicates whether r is refers to a readable memory location,
a predicate writeable(r, C) indicates whether r is refers to a writeable memory location,
a predicate shared(r, C) indicates whether r is shared, and
a predicate unique(r, C) indicates whether r is unique.
They are formally defined as follows:

    contains(s, r, C) ⇔ s ∈(C.ρ)  i = C.μ.(C.ρ.s) 
          i: X → L ∃ x ∈ X, (i.x = r contains(i.x, r)) 
       readable(r, C)    ⇔ r ∈(C.κ)  C.κ.r ∩{𝐫𝐨, 𝐫𝐰}≠∅
       writeable(r, C)   ⇔ r ∈(C.κ)  C.κ.r ∩{𝐫𝐰}≠∅
         ∄s, (contains(s, r, C) ¬writeable(s, C)) 
       shared(r, C)      ⇔readable(r, C) ∃ s, 𝐛[r] ∈ C.κ.s 
       unique(r, C)      ⇔readable(r, C) ∄s, 𝐛[r] ∈ C.κ.s











Copy assignments consist in taking the value represented by the right operand and store a transitive (a.k.a. deep) copy at the location represented by the left operand.
Therefore, we assume the existence of a function copy available at runtime to perform such an operation.
The right operand obviously has to be readable.
As the assignment is mutating, it requires that the left operand be either writeable or unallocated.


  sep=1.5em
  [E-Copy-Mutating] 
    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 

    readable(right, C_l) 

    writeable(left, C_l) 

    l_l = C_l.ρ.left 

    l_r = C_l.ρ.right 

    C' = C_l[μ.l_l ↦copy(C_l.μ.l_r)]
  
    Γ, C ⊢t_1 t_2 ⇓left, C'
  


If the left operand is unallocated, the assignment must also add a new memory location to memory table's domain.
Furthermore, the capability of the left operand also have to be initialized.
Those will depend on the mutability qualifier of the left operand's type.
If it is declared with the  qualifier, then it will obtain the read-write and the read-only capability, otherwise it will obtain the latter only.
We define this principle with a function ic, formally described as follows:

    ic(τ) = {𝐫𝐰, 𝐫𝐨}   if ∈τ.q 
    {𝐫𝐨}   otherwise

Then we define the evaluation of copy assignments whose left operand is unallocated.


  sep=1.5em
  [E-Copy-Unalloc] 
    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 


    readable(right, C_l) 

    C_l.ρ.left = 0 

    l_l ∉(C_l.μ) 


    l_r = C_l.ρ.right 

    C' = C_l[μ.l_l ↦copy(C_l.μ.l_r)] 

    C” = C'[ρ.left ↦l_l][κ.left ↦ic(Γ(t_1))]
  
    Γ, C ⊢t_1 t_2 ⇓left, C”
  


Move assignments are declared similarly, additionally requiring right operands to be unique before destroying their binding and removing their capabilities.


  sep=1.5em
  [E-Move-Mutating] 
    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 

    unique(right, C_l) 

    writeable(left, C_l) 

    l_l = C_l.ρ.left 


    l_r = C_l.ρ.right 

    C' = C_l[μ.l_l ↦C_l.μ.l_r] 

    C” = C'[ρ.right ↦0][κ.right ↦∅]
  
    Γ, C ⊢t_1 t_2 ⇓left, C”
  


  sep=1.5em
  [E-Move-Unalloc] 
    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 


    unique(right, C_l) 

    C_l.ρ.left = 0 

    l_l ∉(C_l.μ) 


    l_r = C_l.ρ.right 

    C' = C_l[μ.l_l ↦C_l.μ.l_r] 

    C” = C'[ρ.left ↦l_l][κ.left ↦ic(Γ(t_1))] 

    C”' = C”[ρ.right ↦0][κ.right ↦∅]
  
    Γ, C ⊢t_1 t_2 ⇓left, C”'
  


Aliasing assignments consist of an update of the pointer table.
A particular care must be brought to the typestate of the operands, to avoid forming mutating aliases on non-mutating references, and conversely.
To facilitate this task, we define another function B that returns the set of borrowed reference on a particular one, formally described as follows:

    B(r, C) = { s | s ∈(C.κ) {𝐛[r] }∈ C.κ.s }

Then we define the evaluation of aliasing assignments.


  sep=1.5em
  [E-Alias-Cst] 
    ∈Γ(t_1).q 

    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 

    readable(right, C_l) 

    ¬shared(left, C_l) 

    
    ∄s ∈B(right, C_l), writeable(s, C_l) 

    C' = C_l[ρ.left ↦C_l.ρ.right][κ.left ↦{ 𝐫𝐨, 𝐛[right] }]
  
    Γ, C ⊢t_1 t_2 ⇓left, C'
  


  sep=1.5em
  [E-Alias-Mut] 
    ∈Γ(t_1).q 

    Γ, C ⊢t_2 ⇓right, C_r 

    Γ, C_r ⊢t_1 ⇓left, C_l 

    writeable(right, C_l) 

    ¬shared(left, C_l) 

    ∀s ∈B(right, C_l), writeable(s, C_l) 

    C' = C_l[ρ.left ↦C_l.ρ.right][κ.left ↦{ 𝐫𝐰, 𝐛[right] }]
  
    Γ, C ⊢t_1 t_2 ⇓left, C'
  




  §.§.§ Function calls

We already mentioned that there is a tight connection between assignment semantics and the passing of parameters and return values, as a function is seen as a piece of reusable code that is inlined at each of its call sites.
For example:

    x  (λ:τ y ∙ y)(t ; y  x) 
    ≡
    y:τ.dom.yt ; y  x ; x  y

This resemblance is made explicit in our semantics.
We subdivide function calls' evaluations into three steps:

  
  Evaluate the callee
    This step is described by a dedicated evaluation operator ⇓^callee
    that retrieves the function value represented by the callee.
    Unlike ⇓, this operator produces function values (i.e. elements of ) rather than reference identifiers.
  
  Evaluate the arguments
    This step is described by another dedicated evaluation operator ⇓^args
    that processes argument lists recursively.
  
  Evaluate the body
    A function's body is merely a term that should be evaluated in the proper evaluation context.
    Hence this last step is described by ⇓.

The first step consists in getting the memory location represented by the callee, in order to determine the function's parameters and body.


  sep=1.5em
  [E-Callee] 
    Γ, C ⊢t ⇓r, C' 

    readable(r, C') 

    l = C'.ρ.r 

    C'.μ.l = λ:τ x ∙b
  
    Γ, C ⊢t ⇓^callee λ:τ x ∙b , C'
  


Recall that we reuse our assignment operators to specify the parameter passing policy.
The alias operator corresponds to the pass-by-alias semantics, the mutation operator corresponds to the pass-by-value semantics,
and the move operator considers arguments as linear resources.
Consequently, a parameter can be understood as a variable whose declaration and initialization precede the function's body, while an argument describes how its corresponding parameter is initialized.
Therefore, it makes sense to treat each argument as a regular assignment on a freshly declared variable.


  sep=1.5em
  [E-Args-N] 
    Γ, C ⊢x:Γ(x)x t ⇓r_x, C_x 


    Γ, C_x ⊢u ⇓^args C'
  
    Γ, C ⊢(x t) + u ⇓^args C'
  
  [E-Args-0] 
  
    Γ, C ⊢ϵ⇓^args C
  


As any other expression, a function call should be evaluated as a reference identifier.
Unfortunately, this identifier cannot be known at the call site, because it depends on the return statement that will be executed.
The support for multiple return semantics further complicates the task.
One solution is to take a similar path as that we took for the arguments, and interpret return statements as regular assignments to a “virtual” identifier.
Let ∈ be a reserved identifier denoting a virtual return identifier.
Then a return statement is simply an assignment to the return identifier.
In other words, t can be considered equivalent to t.


  sep=1.5em
  [E-Ret] 
    Γ, C ⊢t ⇓r, C'
  
    Γ, C ⊢t ⇓r, C'
  


Sequences of statements are simply executed in order.
Conditional term's evaluation first determines which of the branches should be executed, assuming {𝚝𝚛𝚞𝚎, 𝚏𝚊𝚕𝚜𝚎}∈ are atomic values denoting booleans.


  sep=1.5em
  [E-Seq] 
    Γ, C ⊢t_1 ⇓r_1, C' 

    Γ, C' ⊢t_2 ⇓r_2, C”
  
    Γ, C ⊢t_1 ; t_2 ⇓r_2, C”
  


  sep=1.5em
  [E-Cond-True] 
    Γ, C ⊢t_1 ⇓r_1, C' 

    readable(r_1, C') 

    l = C'.ρ.r_1 

    C'.μ.l = 𝚝𝚛𝚞𝚎 

    Γ, C' ⊢t_2 ⇓r_2, C”
  
    Γ, C ⊢t_1t_2t_3 ⇓r_2, C”
  


  sep=1.5em
  [E-Cond-False] 
    Γ, C ⊢t_1 ⇓r_1, C' 

    readable(r_1, C') 

    l = C'.ρ.r_1 

    C'.μ.l = 𝚏𝚊𝚕𝚜𝚎 

    Γ, C' ⊢t_3 ⇓r_3, C”
  
    Γ, C ⊢t_1t_2t_3 ⇓r_3, C”
  


Finally, the rule E-Call assembles all pieces together.
Unfortunately, name shadowing must be taking into account, as function parameters may have the same name as local variables.
A solution is to leverage the λ-calculus' α-conversion, and rename the callee's parameters so that none of them can clash with the identifiers in the current scope.
We describe this process by finding a substitution σ: such that maps shadowing parameters to fresh names.
More formally:

    σ = subst(λ:τ x∙ t, C) 
    ⇔
    x∈(σ)^#∀ x ∈(σ), σ.x ∉(C.ν)

Let σ be a substitution function and t ∈ be a term, we write t[/σ] the substitution of every identifier x ∈(σ) by its corresponding image in σ.
For example xx  2[/{ x ↦ y }] = yy  2.
The shadowing of the return identifier also has to be handled, in case it is shadowed by another call inside the function's body.
This is formalized by a function restore, defined as follows:

    restore(C_a, C') = 
        C'[ν.↦ C_a.ν.]    if ∈(C_a.ν) 
    
        C'    otherwise

Then we define the evaluation of function calls.


  sep=1.5em
  [E-Call] 
    Γ, C ⊢f ⇓^callee λ:τ x ∙t, C_f 

    σ= subst(λ:τ x ∙t, C_f) 

    (λ:τ' x' ∙u') = (λ:τ x ∙t)[/σ] 

    Γ' = Γ[σ.x ↦Γ.x |x ∈(σ)] 

    Γ', C_f ⊢u[/σ] ⇓^args C_a 

    τ_= τ'.codom 

    Γ'[↦τ_], C_a ⊢(:τ_t') ⇓r, C' 

    C” = restore(C_a, C')
  
    Γ, C ⊢f(u) ⇓r, C”
  




  §.§.§ Values


Literal values are allocated to a new memory location, to which a reference identifier is created, associated with the capabilities corresponding to the term's type.


  sep=1.5em
  [E-Atom] 
    a ∈

    r ∉(C.ν) 

    l ∉(C.μ) 

    C' = C[ρ.r ↦l][μ.l ↦a][κ.r ↦ic(Γ(a))]
  
    Γ, C ⊢a ⇓r, C'
  
  

  [E-Fun] 
    r ∉(C.ν) 

    l ∉(C.μ) 

    C' = C[ρ.r ↦l][μ.l ↦λ:τ x ∙t][κ.r ↦ic(τ)]
  
    Γ, C ⊢λ:τ x ∙t ⇓r, C'
  


Records are instantiated by creating a reference identifier for each of their fields, stored as a function mapping the corresponding field names to them.
This essentially creates a separate variable table, specific to the record's fields.
Therefore, dereferencing a field is similar to how variables are dereferenced, only differing in the table that is consulted.


  sep=1.5em
  [E-New] 
    ∀x ∈(τ), r_x ∉(C.ν) 

    i = x ↦r_x |x ∈(τ) 

    r ∉(C.ν) 

    l ∉(C.μ) 

    C' = C[ρ.r ↦l][μ.l ↦i][κ.r ↦ic(τ)] 

    C” = C'[ρ.r_x ↦0 |x ∈(τ)][κ.t_x ↦∅|x ∈(τ)]
  
    Γ, C ⊢τ ⇓r, C”
  


  sep=1.5em
  [E-Field] 
    Γ, C ⊢t ⇓r, C' 

    readable(r, C') 

    l = C'.ρ.r 

    x ∈(C'.μ.l)
  
    Γ, C ⊢t.x ⇓C'.μ.l.x, C'
  



§ RELATED WORK


While many contemporary programming languages offer a tight control over the assignment semantics (e.g. Rust or C/C++), very few propose different assignment operators rather than overloading a single one with different semantics.
The R language proposes two operators, but those are related to variable visibility rather than assignment semantics <cit.>.
The Go language also features multiple operators, for similar purposes <cit.>.
Highly customizable languages (e.g. Python, C++ or Swift) can let augmented assignment operators such as “|+=|” or “|-=|” be redefined to suit a custom assignment semantics.

Early proposals to formalize assignments semantics include λ_var <cit.>, an extension of the classic λ-calculus that features assignable variables.
These are introduced into an expression by an additional construct xe, which delimits their lexical scope.


A subsequent line of research focus on equipping λ_var with type systems (e.g .<cit.>) to guarantee freedom from side effects for pure applicative terms.
Another approach from the same era formalizes the notion of memory location, in order to support a call-by-value approach <cit.>.
Similar to λ_var the authors propose assignable variables, but those are interpreted as memory locations in terms' reductions.
This semantics is revisited in ClassicJava <cit.> to formalize a subset of Java.
The resounding success of object-orientation in the last couple of decades has pushed into the direction of object-oriented calculi.
Among the most popular is Featherweight Java <cit.>, that aims to provide a minimal calculus for studying the consequences of extensions to the Java language.
Evidently, support for assignments is a natural extension for Featherweight, and is proposed in a variety of models (e.g. <cit.>).
More recently, <cit.> introduces a calculus whose semantics is not defined with an auxiliary memory structure to represent assignable variables' bindings.
Instead, the authors proposes to stay at a higher abstraction level and reduce assignable variables to the value they represent.
The advantage is that aliasing is conveyed at a syntactic level, whereas approaches based on an external store require aliasing information to be derived from variable mappings.
The model is further extended in <cit.> to integrate aliasing control mechanisms.
In comparison, our approach aims to model memory more precisely, at the cost of a more complex operational semantics.

Our type system heavily borrows from the domain of typestate analysis <cit.> and type capabilities <cit.>.
More specifically, our treatment of non-mutating references is reminiscent to <cit.>.
Our work is also related to Ownership Types <cit.>.
While Ownership Types were originally designed to control the exposure of an object's internal representation, a plethora of variants have been to proposed to address different issues, including mutability <cit.>.
In particular, Anzen's restrictions on non-mutating aliases to mutating fields is reminiscent to the owners-as-accessors strategy <cit.>, which proscribes access to a reference unless its owner appears on the call stack (similar to our example involving inversion of control).
The main difference between these approaches and ours is that Anzen performs typestate checking at runtime rather than statically.
While this induces an overhead on execution, it allows for a more precise tracking of uniqueness and immutability by avoiding conservative hypotheses.



§ CONCLUDING REMARKS


We have presented Anzen, a general purpose language that aims to make assignments easier to understand and manipulate.
Although it supports multiple paradigms, Anzen leans towards object orientation and imperative programming.
The most distinguishing feature of the language is its three different assignment operators, that together can reproduce all common imperative assignment strategies explicitly.
One describes aliasing, another describes cloning and the last relates to assignments that preserve uniqueness.

The language is also equipped with a type system to control uniqueness and immutability dynamically, based on type capabilities.
Constraints are specified using type annotations on variable declarations and function signatures.

We have introduced Anzen's features informally, through various simple examples, and illustrated their use to solve a non-trivial problem that caused a security breach in a past implementation of Java.
Then, we have formalized Anzen's semantics and type system by the means of a minimal formal language called the 𝒜-calculus.
An implementation of Anzen's interpreter is distributed as an open-source software and available at <https://github.com/anzen-lang/anzen>.

While we have presented our approach through the lens of a particular language, Anzen's operators and type systems can be adapted to other languages, as we did in <cit.> for a dialect of JavaScript.



