Introduction

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 [1]. Third, a semantics described in Skel can be close to a previously written formulation, be it as inference rules or as an algorithmic specification. Finally, Necro provides a comprehensive and extensible set of tools to manipulate these semantics. For instance, to translate it into an interpreter (Necro ML, see Section 3.2), or to give a formalization in the Coq proof assistant (Necro Coq, see Section 3.3).

Skel is a statically strongly typed language. First introduced in [2], we present its redesign with a syntax close to ML. We also introduce support for polymorphism and higher order, enabling the use of monads in specifications [1].

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 [3]), or when writing a semantics defined with inference rules (e.g. 𝜆-calculus). Skel can be used to describe arbitrary semantics, including ones with partiality and non-determinism.

Necro contains several tools to manipulate skeletal semantics (semantics written in Skel). First, Necro Lib offers 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. 1The 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.

Skeletal Semantics

Skel by Example

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. The branch . . . or . . . end construct is a Skel primitive to deal with non-deterministic choice, similar to McCarthy's ambiguous operator [4]. There is no order in a branching, so any branch which yields a result can be chosen. Overlapping branches provide non-determinism, and non-exhaustive branches provide partiality. For instance the branch end at the end will never yield a result, so ss is partially defined.

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.

Formalism

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 [5] and to Abstract Normal Forms [6]: we separate what is intuitively an evaluated value to what is a computation. This makes the evaluation order unambiguous and the manipulation of skeletal semantics simpler.

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 ) . . . ) + 𝑝 𝑛 ← 𝜏 𝑛 ,

where fields(𝜈) = {𝑓

Typing

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 different 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.

Concrete Interpretation

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 interpreta-tion, which stands for the usual natural semantics of a language [7]. One may also define an abstract interpretation, where unspecified types are given values in some abstract domain and where the results from branches are all collected. Such an interpretation is beyond the scope of this paper.

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 𝑥 ∈ 𝒫(𝑉

𝜏 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.

Polymorphism and Type Inference

Our type system allows for polymorphism, with explicit type annotations specified using angle brackets. Any declared and defined type can be polymorphic. 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.

The Necro Ecosystem

Necro is an ecosystem with several tools to perform different operations on skeletal semantics, as illustrated in Figure 3.

Necro Lib

Necro Lib [8] is an OCaml library file, necro.cma. It provides a parser and a typer, in order to transform a Skel file into a Skel AST. The AST is described in the file main/skeltypes.mli of the repository. It also contains a pretty-printer, which displays the AST in the format of a Skel file; a set of transformers, along with the tool Necro Trans that calls the transformers on an AST and prints the result; and a set of utility functions to manipulate the AST. The necro.cma file is the basis for Necro ML (Section 3.2) and Necro Coq (Section 3.3).

Necro ML

Necro ML [9] is a generator of OCaml interpreters. Given a skeletal semantics, it produces an OCaml functor. This functor expects as arguments an OCaml specification of all unspecified types and terms, it then provides an interpreter that can compute any given skeleton. Skel cannot be shallowly embedded in OCaml, since OCaml does not have an operator fitting the branching construct (pattern matching is deterministic in OCaml). So types and terms are shallowly embedded, but skeletons are deeply embedded. We use an interpretation monad, which specifies, amongst other things, how skeletons are represented, and how let ins, applications and branches are computed.

OCaml Interpreter

When Necro ML is executed on a skeletal semantics, it generates an OCaml file, which contains several modules, functors, and module types. To create an interpreter, one needs to instantiate them, in order to indicate how unspecified types and terms are interpreted, and which interpretation monad is chosen.

Working examples can be found in the test folder of Necro ML's repository.

Interpretation Monad

The interpretation monad is defined as follows, where terms are assumed to be pure while skeletons are monadic (of type 'a t). 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.

module

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 [10]. 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. 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.

Necro Coq

Necro Coq [11] is a tool to embed a given skeletal semantics into a Coq formalization. It can then be used to prove language properties or correctness of a given program.

Structure

Necro Coq uses a deep embedding of Skel. The embedding of Skel is defined in the file files/Skeleton.v, which is presented in Section 3.3.2. The command necrocoq file.sk provides a Coq file that contains the AST of the original skeletal semantics. To give meaning to the skeletons, we then provide a file that defines the concrete interpretation for skeletons and terms.

Skel's Embedding

The embedding is a straightforward deep embedding. It defines a number of variables, which are the data of a given skeletal semantics (its constructors, base types, . . . ), and provides the basic constructs (the definition of a type, a skeleton, . . . ).

Values

The values that are the result of the evaluation of a term or skeleton are deeply embedded as well. The Coq type which supports values is defined with five constructors. Here are the first four. 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.

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: 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 [2]. The purpose of this file is to be able to perform a strong induction on interp_skel in a simple way.

These interpretations are proven (in Coq) to be equivalent, so one can use indifferently 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 suffices to only prove it for Concrete_ss.v:

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 [12]. They reuse the deep embedding provided by Necro Coq and are proven correct in relation to the concrete interpretation.

Unspecified Functional Values

Since Skel allows to declare unspecified terms, we must be able to interpret them. The natural idea would be to ask for a cvalue for each given unspecified term. But for unspecified functions (like the addition), that would mean giving a closure, which is equivalent to specifying the function. We would lose Skel's power of partial specification. Instead, we ask for a relation that, given a list of cvalues as arguments, provides the result of the application of the term to the arguments. For instance, for the addition, it would be {([𝑥; 𝑦], 𝑥 + 𝑦) | 𝑥, 𝑦 ∈ N}.

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.

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 [13] to provide the a posteriori proof of an automatic generic transformation of a big step semantics into a small step semantics.

Related Work

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 [2]. We significantly improve on this approach by having a more expressive language (with higher-order functions and polymorphism) and a set of tools to manipulate skeletal semantics. The Coq formalizations of [2] were written by hand, they can now be automatically generated. Generation of OCaml code was also proposed in [14], but it was only available for the language of [2], which was less powerful than the current language. It also did not consider interpretation monads.

Regarding meta-languages to describe semantics, existing tools are much more complex than Skel. This is the case of Lem [15] and Ott [16]. The simplicity of Skel (the file skeltypes.mli describing Skel's AST is only 114 lines of specification) allows anyone to easily write a tool handling skeletal semantics. This is less immediate with Lem and Ott, as one has to deal with many additional features. For instance, Lem natively defines set comprehension, relations, and maps. Also, Coq generation is done as a shallow embedding, hence functions must be proven to terminate. In addition, shallow embedding of large semantics are not easily manipulated in Coq, due to the space complexity of the induction and inversion tactics.

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 language 5 , 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.

Conclusion

Skel offers 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 [1]. We plan to write a formalization of Python based on an existing precise description [19].

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. 8Finally, Skel and Necro are currently being used to describe semantics style transformations, both at the object level [13] and at the meta-language level [12]. Work has also started to automatically derive control flow analyses from a language description.

A. Typing Rules for Skeletal SemanticsΓ(𝑥) = 𝜏 Γ ⊢ 𝑡 𝑥 : 𝜏 Var val x:𝜏 Γ ⊢ 𝑡 𝑥 : 𝜏 TermUnspec val x:𝜏 = t Γ ⊢ 𝑡 𝑥 : 𝜏 TermSpec Γ ⊢ 𝑡 𝑡 : 𝜏 ctype(C) = (𝜏, 𝜏 ′ ) Γ ⊢ 𝑡 C 𝑡 : 𝜏 ′ Const Γ ⊢ 𝑡 𝑡 1 : 𝜏 1 . . . Γ ⊢ 𝑡 𝑡 𝑛 : 𝜏 𝑛 Γ ⊢ 𝑡 (𝑡 1 , . . . , 𝑡 𝑛 ) : (𝜏 1 , . . . , 𝜏 𝑛 ) Tuple Γ + 𝑝 ← 𝜏 ⊢ 𝑆 𝑆 : 𝜏 ′ Γ ⊢ 𝑡 (𝜆𝑝 : 𝜏 → 𝑆) : 𝜏 → 𝜏 ′ Clos Γ ⊢ 𝑡 𝑡 : 𝜈 ftype(𝑓 ) = (𝜏, 𝜈) Γ ⊢ 𝑡 𝑡.𝑓 : 𝜏 FieldGet Γ ⊢ 𝑡 𝑡 : (𝜏 1 , . . . , 𝜏 𝑚 ) 1 ≤ 𝑖 ≤ 𝑚 Γ ⊢ 𝑡 𝑡.𝑖 : 𝜏 𝑖 TupleGet fields(𝜏 ) = {𝑓 1 : 𝜏 1 , . . . , 𝑓 𝑛 : 𝜏 𝑛 } Γ ⊢ 𝑡 𝑡 1 : 𝜏 1 . . . Γ ⊢ 𝑡 𝑡 𝑛 : 𝜏 𝑛 Γ ⊢ 𝑡 (𝑓 1 = 𝑡 1 , . . . , 𝑓 𝑛 = 𝑡 𝑛 ) : 𝜏 Rec Γ ⊢ 𝑡 𝑡 : 𝜏 ∀𝑖 ∈ 1; 𝑚 , Γ ⊢ 𝑡 𝑡 𝑖 : 𝜏 𝑖 ∀𝑖 ∈ 1; 𝑚 , ftype 𝑓 𝑖 = (𝜏 𝑖 , 𝜏 ) Γ ⊢ 𝑡 𝑡 ← (𝑓 1 = 𝑡 1 , . . . , 𝑓 𝑚 = 𝑡 𝑚 ) : 𝜏 FieldSet Γ ⊢ 𝑡 𝑡 : 𝜏 Γ ⊢ 𝑆 ret 𝑡 : 𝜏 Ret Γ ⊢ 𝑆 𝑆 1 : 𝜏 . . . Γ ⊢ 𝑆 𝑆 𝑛 : 𝜏 Γ ⊢ 𝑆 (𝑆 1 . . . 𝑆 𝑛 ) : 𝜏 Branch Γ ⊢ 𝑆 𝑆 : 𝜏 Γ + 𝑝 ← 𝜏 ⊢ 𝑆 𝑆 ′ : 𝜏 ′ Γ ⊢ 𝑆 let 𝑝 = 𝑆 in𝑆 ′ : 𝜏 ′ LetIn Γ + 𝑝 ← 𝜏 ⊢ 𝑆 𝑆 : 𝜏 ′ Γ ⊢ 𝑆 let 𝑝 : 𝜏 in 𝑆 : 𝜏 ′ Exist Γ ⊢ 𝑡 𝑡 : 𝜏 Γ + 𝑝 1 ← 𝜏 ⊢ 𝑆 𝑆 1 : 𝜈 . . . Γ + 𝑝 𝑛 ← 𝜏 ⊢ 𝑆 𝑆 𝑛 : 𝜈 Γ ⊢ 𝑆 match 𝑡 with|𝑝 1 → 𝑆 1 |. . . |𝑝 𝑛 → 𝑆 𝑛 : 𝜈 Match Γ ⊢ 𝑡 0 : 𝜏 1 → • • • → 𝜏 𝑛 → 𝜏 Γ ⊢ 𝑡 𝑡 1 : 𝜏 1 . . . Γ ⊢ 𝑡 𝑡 𝑛 : 𝜏 𝑛 Γ ⊢ 𝑆 (𝑡 0 𝑡 1 . . .