This page provides a detailed discussion of our work on formalising Core Erlang in the Rocq proof assistant, and highlights some of the essentia (an hopyfully influential) results of the project so far.

A short introduction of Core Erlang

Core Erlang is an intermediate language in the compilation pipeline of Erlang (as well as Elixir and Gleam). It is the target of numerous optimization steps of the compiler (such as constant folding, or dead code elimination).

Consider the following simple function computing the factorial of a number:

fact(N) when N =:= 0 -> 1;
fact(N) -> N * fact(N - 1).

Compiling this function to Core Erlang with the options [to_core, no_copt] results in the following code:

'fact'/1 =
    %% Line 4
    ( fun (_0) ->
	  ( case ( _0 -| [{'function',{'fact',1}}] ) of
	      <N> when call 'erlang':'=:='(N, 0) -> 1
	      %% Line 5
	      <N> when 'true' ->
		  let <_1> = call 'erlang':'-'(N, 1)
		  in let <_2> = apply 'fact'/1(_1)
		     in call 'erlang':'*'(N, _2)
	      ( <_3> when 'true' -> ( primop 'match_fail'
			  (( {'function_clause',_3}
			     -| [{'function',{'fact',1}}] ))
		      -| [{'function',{'fact',1}}] )
		-| ['compiler_generated'] )
	    end
	    -| [{'function',{'fact',1}}] )
      -| [{'function',{'fact',1}}] )

While with only [to_core], we get the following, optimized variant (which does not contain the redundant 3rd clause of the case expression):

'fact'/1 =
    %% Line 4
    ( fun (_0) ->
	  ( case ( _0 -| [{'function',{'fact',1}}] ) of
	      <N> when call 'erlang':'=:='(( _0 -| [{'function',{'fact',1}}]), 0) -> 1
	      %% Line 5
	      <N> when 'true' ->
		  let <_1> =
		      call 'erlang':'-'(N, 1)
		  in  let <_2> = apply 'fact'/1(_1)
		      in  call 'erlang':'*'(N, _2)
	    end
	    -| [{'function',{'fact',1}}] )
      -| [{'function',{'fact',1}}] )

Even from these code examples, a number of notable features of Core Erlang appear that do not exist (or behave in a different way) in Erlang. To mention but a few:

Furthermore, numerous other Erlang language features get translated to their more primitive Core Erlang counterpart (or a combination of more primitive Core Erlang expressions). For example, receive expressions are expressed with primitive operations and recursion, list comprehensions are unfolded as an explicit recursive function, and if expressions get translated to case expressions. This means that Core Erlang has far fewer language elements than Erlang, and therefore, it is more tractable to define formally. On the other hand, Core Erlang is more verbose and significantly less readable than Erlang as it is not meant to be a surface language.

For the reasons above, defining a semantics of Core Erlang is more advantageous than targeting Erlang, Elixir or Gleam: 1) we can exploit trusted translation of Erlang, Elixir and Gleam to Core Erlang to indirectly reason about programs written in the original language, 2) the language of Core Erlang is much smaller and simpler to define formally than the higher-level languages.

What is a formal semantics? What is a mechanized semantics?

A formal semantics is a mathematically precise description of program behavior: it defines exactly what program execution does, using mathematical objects and rules rather than prose in a manual or the behavior of a particular compiler. Because the definition is unambiguous, it can settle questions informal descriptions leave open, such as whether two programs always behave the same or whether an optimization preserves meaning.

A mechanized semantics is a formal semantics encoded in a proof assistant (in our case, the Rocq prover) rather than existing only on paper. The syntax, the evaluation rules, and every proof about them—for instance that evaluation is deterministic, or that a transformation preserves the meaning—are checked by the machine down to primitive inference steps. Mechanization rules out the gaps and unstated assumptions that hand-written proofs often hide, and it gives a solid foundation for larger verified work. Furthermore—since Rocq is essentially a functional programming language—definitions and functions are executable, and therefore, a function-based semantics can also serve as an interpreter for the programming language. Nevertheless, we emphasise that the encoding we use is a deep embedding: instead of translating Core Erlang functions to Rocq functions, we model Core Erlang functions as data in Rocq and define explicitly how they are interpreted.

The syntax and formal semantics of Core Erlang

In this section, we discuss which features of Core Erlang have been implemented in our formal semantics, and how they behave. Core Erlang has an official language specification, but it was written back in 2000 and became outdated. Therefore, our semantics has been based not only on this specification, but also on other related research, online materials (some are highlighted under “Further reading”), and the official implementation of the Erlang compiler. Here, we summarise the syntax and behavior of Core Erlang informally; however, everything presented here is expressed in mathematics and logic, and also implemented in the Rocq prover.

Sequential features

We will use v (and its indexed variants) to denote values, e for expressions, and p for patterns.

Values (denoted with v)

Values represent the result of computation, and not all values can be explicitly written in Core Erlang code. For example, closures cannot be constructed directly, but they are the result of evaluating a function expression.

Patterns (denoted with p) and pattern matching

Patterns have the same structure as values (except for closures and function identifiers). They can only be used in case expressions (cf. Erlang) to match against values. A pattern matching is either successful or unsuccessful. A successful match contains (sub)values for the variables occurring in the pattern.

Expressions (denoted with e) and their evaluation

An expression of Core Erlang evaluates either to a value sequence or to an exception. An exception is a triple of values (an exception class, exception reason, and further details about the error). Whenever an exception is raised, the evaluation stops, and the exception gets propagated, unless it is handled by a try expression.

A value sequence is essentially a list of values (denoted as <v_1, v_2, ..., v_n>). Most Core Erlang expressions evaluate to a singleton value sequence (i.e. a single value), and non-singleton value sequences can only be used in binding expressions (i.e. in let, try, and case) to express simultaneous bindings. The only expression that constructs a non-singleton value sequence is the value list (denoted as <e_1, e_2, ..., e_n>).

Values are the simplest expressions, and they evaluate to themselves enclosed in a singleton value sequence.

Value lists are constructed as

  <e_1, e_2, ..., e_n>
Evaluation

Value lists evaluate in a left-to-right order. It is expected that all subexpressions evaluate to a singleton value sequence (i.e. e_i evaluates to <v_i>), and then the result is a value sequence containing values from these singletons (i.e. <v_1, v_2, ..., v_n>).

Functions are constructed as

  fun(X_1, X_2, ..., X_n) -> e
Evaluation

A function expression evaluates to a closure which contains the formal parameter list and the body expression.

Lists are constructed as

  [e_1|e_2]
Evaluation

Lists evaluate in a right-to-left order (cf. Erlang), so first e_2 is evaluated to a singleton value sequence (<v_1>), then e_1 (to <v_2>), and the result [v_1|v_2] is constructed from the values of these singleton sequences.

Tuples are constructed as

  {e_1, e_2, ..., e_n}
Evaluation

Tuples are evaluated in a left-to-right order. All subexpressions are expected to evaluate to singleton value sequences—the result tuple is constructed from the values of these singletons.

Maps are constructed as

  ~{e_1 => e_1', e_2 => e_2', ..., e_n => e_n'}~
Evaluation

Maps are evaluated in a left-to-right order (i.e. first key, first value, second key, second value, etc.). All subexpressions are expected to evaluate to singleton value sequences, and the result map is constructed from the values of these sequences, after duplicate keys are eliminated.

Inter-module call expressions are constructed as

  call e_1:e_2(e_3, e_4, ..., e_n)
Evaluation

The subexpressions of inter-module calls are evaluated in a left-to-right order. All subexpressions are expected to evaluate to singleton value sequences (i.e., <v_1>, <v_2>, <v_3>, …), furthermore, e_1 and e_2 should evaluate to atoms (i.e. v_1 = a_1, and v_2 = a_2), which specify the module and function name used in the call. The semantics then simulates the function called a_2 in module a_1 with the actual arguments v_3, ..., v_n.

Primitive operations are constructed as

  primop a(e_1, e_2, ..., e_n)
Evaluation

Note that the name of primitive operations is expected to be an atom (it is not an expression). The subexpressions of primitive operations are evaluated in a left-to-right order. All subexpressions are expected to evaluate to singleton value sequences (i.e., <v_1>, <v_2>, …). The semantics then simulates the primitive operation called a with the actual arguments v_1, v_2, ....

Function applications are constructed as

  apply e_1(e_2, e_3, ..., e_n)
Evaluation

The subexpressions of applications are evaluated in a left-to-right order. All subexpressions are expected to evaluate to singleton value sequences (i.e., <v_1>, <v_2>, …). The function expression (e_1) is expected to evaluate to a closure (i.e. v_1 is a closure), which is applied to the actual parameters. This means that the closure’s body is evaluated next, after substituting the formal parameters by v_2, ..., v_n. If v_1 is not a closure, or the argument numbers mismatch, an exception is raised.

Pattern matching expressions are constructed as

  case e of
    <p_1_1, p_1_2, ..., p_1_n> when e_1_1 -> e_1_2
    <p_2_1, p_2_2, ..., p_2_n> when e_2_1 -> e_2_2
    ...
    <p_m_1, p_m_2, ..., p_m_n> when e_m_1 -> e_m_2
  end
Evaluation

Note that pattern matching is only done with case in Core Erlang (try does not include patterns, receive is syntax sugar, and there is no match operator). First e is evaluated to a value sequence <v_1, v_2, ..., v_n>. Each clause is expected to contain exactly n patterns, which are pairwise matched against the elements of the value sequence. If all patterns match the values of the sequence, the variables occurring in the patterns will be bound to subvalues, and these bindings are substituted in the guard (after the keyword when) and body expressions (after ->) of the current clause. The guard is expected to evaluate to either <true> (i.e. it succeeds), <false> (i.e. it fails), or an exception, which is propagated (cf. Erlang). If the guard succeeds, the body expression of the current clause is evaluated. If the guard fails, or the patterns of the clause do not match, the next clause is tried. If there are no more clauses, an exception is raised.

Let bindings are constructed as

  let <X_1, X_2, ..., X_n> = e_1 in e_2
Evaluation

First, e_1 is evaluated to a value sequence of length n (which is exactly the number of variables to be bound). Then e_2 is evaluated after substituting the variables by the values of the sequence. If the value sequence has a different length, the behavior is not defined.

Letrec bindings are constructed as

  letrec
    a_1/i_1 = fun(X_1_1, X_1_2, ..., X_1_n) -> e_1
    a_2/i_2 = fun(X_2_1, X_2_2, ..., X_2_n) -> e_2
    ...
    a_m/i_m = fun(X_m_1, X_m_2, ..., X_m_n) -> e_m
  in e
Evaluation

A letrec expression defines recursive functions. First, closures are constructed for each function, which are substituted for their respective function identifiers in e. Note that in this case, the closures also contain a list of all functions defined simultaneously in the same letrec—these functions can be mutually recursive.

Sequencing is expressed as

  do e_1 e_2
Evaluation

Sequencing behaves the same way as a let expression with a single, unused variable. First e_1 is evaluated to a singleton value sequence, then this result is discarded, and the evaluation continues with e_2.

Exception handler expressions are constructed as

  try e_1 of
    <X_1, X_2, ..., X_n> -> e_2
	catch <X_1', X_2', ..., X_m'> -> e_3
Evaluation

First, e_1 is evaluated to a value sequence of length n (if the length is different, the behavior is not defined). Then, e_2 is evaluated after substituting the variables X_1, X_2, ..., X_n by the values of the sequence. However, if e_1 raises an exception, it is handled by catch. In practice, there are three variables in the catch clause that are bound to the three parts of the exception, and e_3 is evaluated after substituting these variables.

The informal description provided here is also expressed in Rocq with a frame-stack semantics (a relation that expresses step-by-step evaluation, and its reflexive, transitive closure).

What’s not formalized from the complete Core Erlang syntax?

Concurrent features

Our semantics of Core Erlang also formalizes a subset of Erlang’s actor model. Here, we enumerate the concurrent features we support.

Mechanization of the semantics of Core Erlang

The entire description above is mechanized in the Rocq prover, in the Core-Erlang-Formalization repository. The abstract syntax is represented in a nameless style: variables and function identifiers are de Bruijn indices (Var := nat), and well-formedness is captured by inductive scoping predicates that track how many binders are in scope. The sequential language is given a substitution-based frame-stack semantics: a small-step relation that uses explicit continuation frames, together with its reflexive-transitive closure describing complete evaluations. The concurrent layer extends this with a process-local relation (message receipts, spawning, links, exit signals for a single process) and an inter-process relation that routes signals between processes running on a node.

Alongside the relational semantics, the development provides an executable interpreter, written as a Rocq function, that is proved equivalent to the frame-stack semantics. Being a plain function, it can be run inside Rocq or can be extracted to OCaml and Haskell. Furthermore, we also applied the semantics in several areas, the most important of which is program equivalence.

Program equivalence in Core Erlang

Program equivalence is used to express when two programs behave the same way, in all possible circumstances. Program equivalence proofs can be used to verify that refactorings or optimizations preserve the behavior, the latter of which is crucial for proving compiler correctness.

For the sequential semantics, we express program equivalence in terms of contextual equivalence (i.e. two equivalent programs should behave the same way in every syntactical context). However, proving contextual equivalence of concrete programs is challenging, and therefore, we also defined a simpler concept (CIU-equivalence) which coincides with contextual equivalence. As an example, we partially verified the clause for do expressions of the constant folding optimization in the Erlang compiler. This means that Core Erlang programs before and after the transformation show the same behavior.

The c_seq clause of the constant-folding pass in sys_core_fold.erl, with part of the code covered by a dashed box labeled 'Not formalized yet'.
The c_seq (sequencing) clause of the constant-folding pass in sys_core_fold.erl. The dashed box marks the sub-case that our equivalence proof does not yet cover.

In the concurrent setup, we rely on barbed bisimulation to prove program equivalence. With these concepts we managed to prove that a sequential and a concurrent variant of list mapping is equivalent (if no exit signals arrive from other processes). This equivalence holds for all function expressions f (with some restrictions), proper lists el, observed PID i, and natural numbers n. (Note that in Core Erlang, receive is syntax sugar.)

Sequential variant

letrec 'map'/2 = fun(F,L) ->
  case L of
    [] when 'true' -> []
    [H|T] when 'true' ->
      [apply F(H)|apply 'map'/2(F,T)]
  end
in
  call 'erlang':'!'(i,apply 'map'/2(f,el))

Concurrent variant

letrec 'map'/2 = fun(F,L) ->
  case L of
    [] when 'true' -> []
    [H|T] when 'true' ->
      [apply F(H)|apply 'map'/2(F,T)]
  end
in
case call 'lists':'split'(n,el) of
 {L1, L2} when 'true' ->
  let S = call 'erlang':'self'() in
   do call 'erlang':'spawn'(fun() ->
        call 'erlang':'!'(S,
                    apply 'map'/2(f, L1)))
      let M2 = apply 'map'/2(f,L2) in
       receive
         M1 when 'true' ->
           call 'erlang':'!'(i,
              call 'erlang':'++'(M1,M2))
       after 'infinity' -> []
end

These snippets roughly correspond to the following Erlang functions.

map(F, L) ->
    case L of
        []      -> [];
        [H | T] -> [F(H) | map(F, T)]
    end.

%% Sequential variant
seq(F, El, I) ->
    I ! map(F, El).

%% Concurrent variant
conc(F, El, I, N) ->
    {L1, L2} = lists:split(N, El),
    S = self(),
    spawn(fun() -> S ! map(F, L1) end),
    M2 = map(F, L2),
    receive
        M1 -> I ! M1 ++ M2
    end.

Further reading