We present Skel, a meta language designed to describe the semantics of programming languages, and Necro, a set of tools to manipulate said descriptions. We show how Skel, although minimal, can faithfully and formally capture informal specifications. We also show how we can use these descriptions to generate OCaml interpreters and Coq formalizations of the specified languages.
To formally prove properties of a programming language, or programs in that language, it is necessary to have a formal specification of its semantics. We expect the tool and the language used to describe this formalization to be executable, usable, and easily verifiable, that is, close to a paper-written specification.
Necro provides a language (Skel) and a set of tools to formalize and interpret the semantics of
programming languages. Necro fulfills these requirements and more. First, Skel is designed to be
light and its semantics simple. A light language facilitates maintainability and the development
of tools. Second, Skel is powerful enough to express intricate semantical features, as proven by
its use in an ongoing formalization of JavaScript’s semantics [
Skel is a statically strongly typed language. First introduced in [
Skel can be seen as a specification language or as a way to define inductive rules. Both
approaches are useful, respectively when writing a semantics whose formalization is a set of
algorithms, (e.g. ECMA-262 [
Necro contains several tools to manipulate skeletal semantics (semantics written in Skel). First, Necro Lib ofers basic operations (parsing, typing, printing, and simple transformations), in the form of a library to write programs that manipulate the AST describing a semantics. Second, Necro includes the tools Necro ML, Necro Coq, and Necro Debug, which use said library to generate respectively an OCaml interpreter, a Coq formalization, and a step-by-step debugger.
The contributions of this work are the Skel language, the accompanying tools, and many examples of semantics available online.1
The paper is organized as follows. Section 2 introduces Skel. Section 3 presents the Necro ecosystem. Section 4 compares our work to existing approaches. Section 5 concludes the paper.
Let us describe how one specifies a semantics in Skel, using the small-step semantics of calculus as example. A skeletal semantics is a list of declarations, either type declarations or term declarations, where each declaration can be unspecified or specified . When a type is unspecified, we only give its name. For instance, when writing the semantics of -calculus, we might not want to specify how identifiers for variables are internally represented, so we declare type ident.
A specified type may be a variant type (i.e., an algebraic data type, defined by providing the list of its constructors together with their input type), a type alias using the := notation, or a record type (defined by listing its fields and their expected types). For instance, the type of -terms would be defined as follows. type term = | Var ident | Lam (ident, term) | App (term, term)
In this example, (ident, term) is the product type with two components, the first one being of type ident, and the second of type term.
A record type is declared as type pair = ( left: int , right: int ) and an alias as type ident := string. Note that types are all implicitly mutually recursive, so the order in which they are declared does not matter.
We now turn to term declarations. An unspecified term declaration is simply its name and type. To declare a specified term, we also give its definition. An example of a term we might want to let unspecified is substitution, so we would declare val subst: ident → term → term → term.
An example of a specified term is the following. val ss (t:term): term = match t with | App (t1, t2) -> branch let t1' = ss t1 in
App (t1', t2) or let t2' = ss t2 in
App (t1, t2') or (* beta-reduction of a redex *) 1https://gitlab.inria.fr/skeletons/necro-test
Term ::=
Skeleton ::=
Pattern ::=
Type ::= ::= ::= Type decl | | (, . . . , ) | : → | . | . | ( = , . . . , = ) | ← ( = , . . . , = ) 0 1 . . . | let = in | let : in | match with ”|” → . . . ”|” → end | branch or . . . or end | ret | _ | | (, . . . , ) | ( = , . . . , = ) | → | (, . . . , ) val : | val : = type | type = ”|” . . . ”|” | type := | type = ( : , . . . , : ) let Lam (x, body) = t1 in let Lam _ = t2 in (* t2 is a value *) subst x t2 body (* body[x←t2] *) end | _ -> (branch end: term) end
The branch . . . or . . . end construct is a Skel primitive to deal with non-deterministic
choice, similar to McCarthy’s ambiguous operator [
The destructuring pattern matching let Lam (x, body) = t1 in ... asserts that t1 is a lambda-abstraction. If it is not, then the considered branch yields no result. If it is, then x and body will be assigned to the proper values.
The match . . . with . . . end construct is a pattern matching, similar to any other language’s pattern matching. In particular, it is deterministic. Only the first (, ) pair for which the pattern corresponds with the matched value is taken.
Figure 1 contains the syntax of Skel terms and skeletons. It does not include polymorphism,
which will be described in Section 2.5. There are two types of expressions: terms and skeletons.
Our syntax is close to Moggi’s computational -calculus [
A term is either a variable, a constructor applied to a term, a (possibly empty) tuple of terms, a -abstraction, the access to a given field of a term, the access to a member of a tuple, a record of terms, or a term with reassignment of some fields. A skeleton is either the application of Γ + ← ≜ Γ, :
Γ + _ ← ≜ Γ Γ + ← ≜ Γ + ← , where ctype() = (, ) Γ + (1, . . . , ) ← ( 1, . . . , ) ≜ ((Γ + 1 ← 1) . . . ) + ← + ← ≜ , : + _ ← ≜
+ ← ≜ + ← + (1, . . . , ) ← (1, . . . , ) ≜ ( + 1 ← 1) . . . + ← + (1 = 1, . . . , = ) ← (1 = 1, . . . , = ) ≜ ( + 1 ← 1) . . . + ← a term to other terms, a let-binding, an existential (see Section 2.4), a branching, a match, or simply the return of a term. We sometimes omit ret in ret . A pattern is either a variable, a wildcard, a constructor applied to a pattern, a (possibly empty) tuple of patterns, or a record pattern. Finally, a type is either a base type (defined by the user), an arrow type, or a (possibly empty) tuple of types. Term and type declarations have already been described in Section 2.1
Skel is a strongly typed language with explicit type annotations. Every term declaration is given a type, as well as every pattern in a -abstraction. Polymorphism, presented in Section 2.5, also uses explicitly specified type arguments. Specifying every type might seem tedious at first, but it helps to improve confidence on the correctness of the skeletal semantics. A future version of the typer will include an optional type-inference mechanism.
To give the typing rules for Skel, we first define ctype(), which returns the pair of the declared input type and output type for the constructor in its type declaration. For instance, we have ctype(Var) = (ident, term). Similarly, we define ftype( ) to return (, ) where is the type of the field , and is the record type to which the field belongs. For instance, we have ftype(left) = (int, pair). Note that a field name may not belong to two diferent record types, and a constructor name may not be used twice, so these functions are well-defined. Finally, we write fields ( ) for the fields and types of record type .
The typing rules for terms and skeletons are straightforward, we give them in Appendix A. They are respectively of the form Γ ⊢ : and Γ ⊢ : , where Γ is a typing environment (a partial function from variable names to types). To deal with pattern matching in -abstractions and let-bindings, we use the partial function Γ + ← defined at the top of Figure 2.
As such, Skel is a concrete syntax to describe a programming language. The meaning associated
to a Skel description is called an interpretation. We present in this section a concrete
interpretation, which stands for the usual natural semantics of a language [
Every skeleton and term is interpreted as a value. Given sets of values for each unspecified type , we build values for variant and product types in the expected way. For arrow types, we use closures for the specified functions, and we delay the evaluation of unspecified terms until we have all arguments. To this end, for each declaration val x : 1 → . . . → n → , we assume given an arity = arity() ∈ N and a relation JK ∈ ( 1 × · · · × × ).
The rules for the concrete interpretation are straighforward. They are given in Appendix B. They are of the form , ⇓ for terms and , ⇓ for skeletons, meaning that in the environment (partial function mapping variables to values), the term or the skeleton can evaluate to a value .
A construct that is specific to Skel is the existential. To interpret the existential let p: in sk, we take any value of type , and match p to this value, before evaluating the continuation in the extended environment. This pattern matching, also used for the let-in constructs and closures, is defined in Figure 2 as the partial function + ← that returns an extended environment.
The concrete interpretation is relational: a skeleton can be interpreted to 0, 1, or several values. A branching with no branch has no result, causing partiality. A branching with several branches can have several results, causing non-determinism. Pattern-matching can fail, causing partiality. Finally, non-terminating computations also cause partiality.
Our type system allows for polymorphism, with explicit type annotations specified using angle brackets. Any declared and defined type can be polymorphic. (* Unspecified *) type list<_> (* Record *) type pair<a,b> = (left: a, right: b) (* Variant *) type union<a,b> = | InjL a | InjR b (* Alias *) type option<a> := union<a,()>
Terms defined at toplevel can also be polymorphic, but let-bound terms are necessarily monomorphic. val map<a,b> (f: a → b) (l: list<a>): list<b> = branch let Nil = l in
Nil<b> or end let Cons (a, qa) = l in let b = f a in let qb = map<a,b> f qa in Cons<b> (b, qb)
IMP
-calculus
Necro Lib → necro.cma
Type annotations are explicitly given when constructing a term (e.g., Nil<b>) or when using a polymorphic term (e.g., map<a,b> f qa), but they can be locally inferred in patterns, so they are not specified in them (e.g., let Nil = l in . . . ).
The explicit typing is by design, as explicit type annotations reduce the risk of error. In the future, we will add an option to perform type inference. This option could also infer the type of the arguments in constructs of the form p: → sk.
Necro is an ecosystem with several tools to perform diferent operations on skeletal semantics, as illustrated in Figure 3.
Necro Lib [
Necro ML [
Working examples can be found in the test folder of Necro ML’s repository. 3.2.2. Interpretation Monad The interpretation monad is defined as follows, where terms are assumed to be pure while skeletons are monadic (of type 'a t). module type MONAD = sig type 'a t val ret: 'a -> 'a t val bind: 'a t -> ('a -> 'b t) -> 'b t val branch: (unit -> 'a t) list -> 'a t val fail: string -> 'a t val apply: ('a -> 'b t) -> 'a -> 'b t val extract: 'a t -> 'a end
The fail operator takes a string as input which is an error message that should be raised, and the extract operator is a usability construct to extract a result from the monad, typically to display it.
There are several proposed ways to instantiate this monad, and the user can also define their
own. The standard identity monad, which is closest to a shallow embedding, tries each branch
in turn. But it chooses the first branch that succeeds, with no ability to backtrack, which can be
problematic in some cases. A more interesting one is the continuation monad, which keeps as a
failure continuation the branches not taken, and can then backtrack if need be [
{ cont = fun k fcont -> x.cont (fun v fcont' -> (f v).cont k fcont') fcont } let fail s = { cont = fun k fcont -> fcont s } let rec branch l = { cont = fun k fcont -> begin match l with | [] -> fcont "No branch matches" | b :: bs -> (b ()).cont k (fun _ -> (branch bs).cont k fcont) end} let apply f x = f x let extract x = x.cont (fun a _ -> a) (fun s -> failwith s) end
Nevertheless, the continuation monad is not complete w.r.t the concrete interpretation, as it always executes the first branch first, and can therefore be caught in an infinite loop. The following function is an example thereof. val loop (_:()): () = branch loop () or () end
To fix this issue, we propose another interpretation monad called BFS, which does one step in each branch, until it gets a result. The file containing all these monads and some others is available online.2 Note that to change the interpretation monad, the user simply has to swap it at module instantiation, no code needs to be rewritten.
3.3.1. Structure
Necro Coq [
Inductive cvalue : Type := | cval_base : forall A, A -> cvalue | cval_constructor : constr -> cvalue -> cvalue | cval_tuple: list cvalue -> cvalue | cval_closure: pattern -> skeleton -> list (string * cvalue) -> cvalue. 2https://gitlab.inria.fr/skeletons/necro-ml/-/blob/master/necromonads.ml
The cval_base constructor allows values of an unspecified type to be represented in Coq with any given type A. For instance, the value 1, in an unspecified type int, could be stored as cval_base Z 1. The next two constructors are straightforward. The fourth one is a closure constructor, to store -abstractions. The three arguments of the constructor are the bound pattern, the skeleton to evaluate, and the current environment. The fifth constructor is used for unspecified functional terms, it will be presented below. 3.3.4. Interpretation The file Concrete.v3 provides the concrete interpretation for skeletons. It uses Coq’s induction to define the relations interp_skel and interp_term, which relate respectively skeletons and terms in a given environment to their possible interpretations as a value. It mostly follows the semantics of Appendix B. For instance, this is the rule for a let in construct: Inductive interp_skel: env -> skeleton -> cvalue -> Prop := | i_letin: forall e e' p s1 s2 v w, interp_skel e s1 v -> add_asn e p v e' -> interp_skel e' s2 w -> interp_skel e (skel_letin p s1 s2) w
The add_asn e p v e' proposition states that the environment can be extended into ′ by mapping to , that is ′ = + ←
The file Concrete.v defines the interpretation using big-step evaluation, but we also provide
a file Concrete_ss.v which does a small-step evaluation. An alternative is ConcreteRec.v,
which defines interpretation from the bottom up. That is, instead of using Coq’s induction, it
only defines how to do one step, which doesn’t use recursive calls, and then one may iterate this
step. It is closest to the initial definition in [
These interpretations are proven (in Coq) to be equivalent, so one can use indiferently one or the other, and one may even switch between several of them depending on what is more useful at the time. The big step definition is usually the easiest to use. The small step one allows to reason about non-terminating behaviors, and it provides a simple way to prove the subject reduction of Skel (see below). The iterative one allows, as we mentioned, to perform a strong induction. An instance where we need to use this one is to prove an induction property on the semantics of a lambda calculus.4 As Skel is deeply embedded, one evaluation step in the language corresponds to several steps in Necro Coq. Because of this, the inductive interpretation is not convenient to prove that property, whereas this is much simpler using the iterative version with a strong induction on the height of the derivation tree.
As Skel is strongly typed, we also have a file WellFormed.v to check that a term or skeleton is well-formed, i.e., that it can be typed. We prove that the concrete interpretation respects the subject reduction property with regards to well-formedness. Since interpretations are all shown to be equivalent, it sufices to only prove it for Concrete_ss.v: 3https://gitlab.inria.fr/skeletons/necro-coq/-/blob/master/files/Concrete.v 4https://gitlab.inria.fr/skeletons/necro-coq/-/blob/master/test/lambda/EvalInd.v#L55 Theorem subject_reduction_skel: forall sk sk' ty, type_ext_skel sk ty -> interp_skel_ss sk sk' -> type_ext_skel sk' ty.
This translates roughly to: :
→ ′ ′ : where S and S’ are extended skeletons.
With this proven, and since Concrete_ss.v and Concrete.v are equivalent, we have: ∅ ⊢ :
⇓ ∈
Finally, interpretations in the form of abstract machines have been defined in [
There are operational and denotational approaches to represent this in Coq. We choose the operation approach as it does not need to evaluate ahead of time: it just waits to be applied to enough arguments before computing. We thus use the following constructor, which denotes an unspecified functional term that is not fully applied yet. | cval_unspec: nat -> unspec_value -> list type -> list cvalue -> cvalue.
The first nat argument being n means that there are S n arguments missing. We add one,
because there cannot be 0 argument missing, since if there is 0 argument missing, it is not a
partial application. The list of types is the type annotation for polymorphic unspecified terms,
the list of values is the list of arguments that have already been provided.
3.3.6. Applications and Usability
We have considered several applications of Necro Coq, some of them can be found in the test
folder of the repository. For instance, we have proved the correctness of an IMP code that
computes the factorial function (test/certif folder). Necro Coq has also been used to prove
the equivalence between a small-step and a big-step semantics for a -calculus extended with
natural numbers (test/lambda folder). In addition, it has been used in [
We review existing approaches that are generic, in the sense that they can be used to describe and manipulate any semantics.
Our work is an extension of the work undertaken in [
Regarding meta-languages to describe semantics, existing tools are much more complex than
Skel. This is the case of Lem [
The K framework [17] also allows to formally define the semantics of a language and prove programs, and it is designed to be easy to use. It does not allow, however, to prove meta-theory properties of a language5, which is one of our future goals. Furthermore, there are no Coq backend for K at the present time, and since K is a large language, writing new backends is far from trivial.
Finally, another common way to describe a semantics is to implement it both in OCaml and in Coq, or other similar tools, either directly or through tools to transform them (Coq extraction to OCaml or coq-of-ocaml [18] to go the other way). One may then execute the semantics using the OCaml version and prove properties using the Coq one. In this case, the Coq formalization is simpler to manipulate, but changing design choices (such as going from a shallow to a deep embedding) is very costly, as OCaml or Coq AST are not easy to manipulate.
Skel ofers a way to specify semantics of programming languages, using a language light enough to be easily readable and maintainable, yet powerful enough to express many semantical features. We have focused on dynamic semantics, but one may also describe static semantics in Skel. The tools Necro provide, such as Necro ML, help in the process of writing a semantics. Necro Coq allows to manipulate and certify these semantics once written. They give the necessary framework to prove program correctness and language properties.
Skel has been used to write the semantics of a set of basic languages such as IMP, but it has
also been used to formalize more massive languages, such as WASM (unpublished), and an
ongoing formalization of JavaScript [
The Necro ecosystem includes other tools, such as Necro Debug,6 which is a step-by-step execution of a semantics. An example execution can be found online.7. In addition, people can easily produce a new tool using Necro Lib.
Although not mentioned in this paper, Skel allows to split the definition of a semantics in several files, and to access them using an include construct. The OCaml generation tool can handle these multi-file semantics using modules, but at the moment this is not the case for Necro Coq. A future task is to implement this functionality using Coq modules. Once this has been done, the logical next step is to implement a standard library for Skel, defining basic types like lists, with properties on these types proven using Necro Coq. Initial work on this standard library can be found online.8
Finally, Skel and Necro are currently being used to describe semantics style transformations,
both at the object level [
Univ. of Illinois Urbana-Champaign, 2018. [18] N. Labs, coq-of-ocaml, https://clarus.github.io/coq-of-ocaml, ???? URL: https://clarus.
github.io/coq-of-ocaml. [19] R. Monat, Static Type and Value Analysis by Abstract Interpretation of Python Programs with Native C Libraries, Ph.D. thesis, Sorbonne Université, 2021.
Γ() = Γ ⊢ :
Var val x: Γ ⊢ :
TermUnspec val x: = t Γ ⊢ :
TermSpec Γ ⊢ :
ctype(C) = (, ′) Γ ⊢ C : ′
Const Γ ⊢ 1 : 1 . . . Γ ⊢ : Tuple Γ ⊢ (1, . . . , ) : ( 1, . . . , ) Γ + ← ⊢ : ′ Γ ⊢ ( : → ) : → ′
Clos Γ ⊢ :
ftype( ) = (, ) Γ ⊢ . :
FieldGet Γ ⊢ : ( 1, . . . , ) Γ ⊢ . :
∀ ∈Γ J⊢1; ← K, Γ(⊢1 = :1, . . . , ∀ =∈ J1;):K, ftype = ( , ) FieldSet Γ ⊢ : Γ ⊢ ret :
Ret Γ ⊢ 1 : . . . Γ ⊢ : Branch Γ ⊢ (1 . . . ) : Γ ⊢ : Γ + ← ⊢ ′ : ′ Γ ⊢ let = in′ : ′
LetIn ΓΓ⊢+ le← t : ⊢in:: ′′ Exist Γ ⊢ : Γ ⊢ 0 : 1 → · · · → Γ + 1 ← ⊢ 1 : . . . Γ + ← ⊢ : Γ ⊢ match with|1 → 1|. . . | → : → Γ ⊢ 1 : 1 Γ ⊢ (0 1 . . . ) : . . .
Γ ⊢ :
Match
App
First we defined rules to handle environments. We define the relation ̸↦→ which holds if cannot represent the value , and the partial function + match(1, . . . , ) as follows: ̸= ′ ̸↦→ ′
NoMatchTuple
NoMatchSameConstr
NoMatchDiffConstr ̸↦→
0 ≤ ≤ (1, . . . , ) ̸↦→ (1, . . . , ) ̸↦→
0 ≤ ≤ ≤ (1 = 1, . . . , = ) ̸↦→ (1 = 1, . . . , = )
NoMatchRecord + 1 ← = ′ + match(1, . . . , ) = (1, ′)
GetMatchFirst 1 ̸↦→ + match(1, . . . , ) = ( + 1, ′) + match(2, . . . , ) = (, ′)
GetMatchNext Now we define the rules for concrete interpretation: (,)⇓= Var val x : ar,ity⇓() = 0 arity() = ≤ JK(1, . . . , , ) +1 . . . ⇓app AppUnspecCont ⌈, (1, . . . , )⌉ +1 . . . ⇓app