A Soltani

B Benbakhti
email: b.benbakhti@ljmu.ac.uk

J-C Gerbedoen

A Khediri

H Maher

J-P Salvestrini

A Ougazzaden

N E Bourzgui

H A Barkad

A Cost-Effective Technology to Improve Power Performance of Nanoribbons GaN HEMTs

A cost-effective fabrication process is developed to improve the power performance of AlGaN/GaN High Electron Mobility Transistors (HEMTs). This process uses nitrogen ion (N + ) implantation to form multiple parallel NanoRibbons on AlGaN/GaN heterostructures, with thin buffer layer (AlGaN/GaN NR-HEMTs). SRIM simulations of the N + implantation combined with measured current-field characteristics reveal a good electrical isolation beneath the 2-dimensional electron gas (2DEG), resulting in substantial increase of the breakdown field of the NR-HEMTs, when compared to conventional AlGaN/GaN HEMTs. The fabricated AlGaN/GaN NR-HEMTs performed (i) an ON/OFF current ratio more than two orders of magnitude larger and (ii) a buffer leakage current more than one order of magnitude weaker than that of the conventional AlGaN/GaN HEMTs. The on-resistance, RON, and series resistance, RS, of AlGaN/GaN NR-HEMTs are both reduced by one order of magnitude, when compared to those of the conventional AlGaN/GaN HEMTs. These have boosted the drive current density by up to 435%. Furthermore, we have found that the architecture of the AlGaN/GaN NR-HEMTs reduces the destructive impact of electron traps in the device. An optimized AlGaN/GaN NR-HEMT exhibited a better electrostatic integrity, a subthreshold slope of ∼210 mV/dec instead of 730 mV/dec for a conventional GaN HEMT. A higher linearity in the transconductance, gm, of NR-HEMTs is observed, twice of that of a conventional GaN HEMT. These results demonstrate the great interest of developed process technology, of NR-HEMTs, for high-power switching applications.

GaN-based HEMTs are among the most promising candidates for high-power and high-speed electronics [START_REF] Yoshida | ISPSD '03. 2003 IEEE 15th International Symposium on Power Semiconductor Devices and ICs[END_REF] . They are attractive for digital electronics and withstanding high-power under high-temperature environments 2, 3 . In the last decade, diverse fabrication processes, e.g. carbon doped or thick buffer layers, gate with a field-plate 4,5 , MISHEMT structures 6 , were investigated and proposed by several research groups to enhance performance of GaN devices 7, [START_REF] Cai | [END_REF] . Nonetheless, key device limitations such as large buffer leakage currents, 7,4 high on-resistance (RON), 9 low drain current density, and relatively poor gate control of the 2D channel are still holding back a wider application of GaN HEMTs. In addition, the above mentioned fabrication processes are non-planar and, thus, costly 10 . To overcome these issues, other research groups have proposed and/or attempted to use nano-structured channels like nano-mesa channels (tri-gate) HEMT, 11- 14 and nano-strip (NS) channels, 15-17 for power switching and RF applications, respectively. Although, GaN HEMTs with tri-gate have demonstrated an improved gate control, they still suffer from low drain currents, high RON and nonlinear transconductance (gm) 13, 14 . Consequently, they are very difficult to be integrated in power switching applications. However, InAlN/GaN HEMTs with NS, developed for RF applications, have manifested better linearity performance in both gm and transition frequency (fT) when compared to conventional and tri-gate HEMTs 15,17 .

In this paper, we propose a cost-effective technology to fabricate nanoribbon (NR) channels by N + implantation, for AlGaN/GaN HEMTs on Si(111) substrate. The overall aim is to develop a low-cost and a planar GaN device technology for power switching applications. We report on the device fabrication technology and performance assessment of these nanoribbon channel devices, including a low RON, a linear transconductance, a high drain current, and a good gate-to-channel control.

The epi-layers of the processed AlGaN/GaN HEMTs were grown by MetalOrganic Chemical Vapor Deposition (MOCVD) on Si(111) substrate. As illustrated in Fig. 1a, the epi-layers structure consists of a 7 nm thick GaN cap layer, 26 nm thick Al0.25Ga0.75N barrier, 1.5 nm thick AlN spacer and 700 nm thick semi-insulating GaN. A 2-dimensional electron gas (2DEG) sheet carrier density, NS, of 9.7×10 12 cm -2 , an electron mobility, µn, of 1700 cm 2 /V.s, and a sheet resistance, R□, of 381 Ω/□ were determined by Hall effect measurements at room temperature on the as-grown wafer. The length (LNR) and width (WNR) of the targeted NR, highlighted in Fig. 1b, are 2 µm and 250 nm, respectively. The spacing between nanoribbons is 750 nm. The proposed process flow of the device fabrication is summarized in Fig. 2. First, ohmic contacts with Ti/Al/Ni/Au (12/200/40/100 nm) metallization scheme were formed and annealed at 850 °C for 30 s in N2 atmosphere. The mesa isolation was then defined by N + multiple implantations based on different doses and energies. The source/drain contact resistance determined by Transmission Line Model (TLM) measurement is 0.37 Ω.mm. Next, a 300 nm thick CSAR 62 resist layer was deposited and patterned by electron beam lithography (e-beam), using AR 600-546 developer. This is to form mask openings for the subsequent N + ion implantation, allowing for the isolation of the 2DEG and formation of NR channels. To process the gate terminal, the CSAR 62 resist mask was afterward removed, and the gate pattern was defined by the e-beam of PMMA 4% 950K resist. Thereafter, Ni/Au (40/300 nm) metal deposition was performed featuring e-beam exposure and evaporation and annealed at 450 o C for 20 min. Finally, the samples were passivated by SiN/SiO2 (50/100 nm) multilayers using PECVD. All implantation energies have been limited to 50 keV to avoid any polymerization of the resist mask. The implantation conditions are optimized using SRIM software. Table 1 summarizes the implantation energies and the corresponding doses for each sample.

Fig. 3 shows the simulated 2D distribution of the Nitrogen vacancy concentration, induced by the N + implantation, for the three samples. Intensifying the implantation energy leads (i) to an increase of the isolation depth from 120 nm up to 180 nm and (ii) to a lowering of the NR width from 120 nm down to 65 nm.

It is important to note that this device fabrication process is a cost effective technology since:

• nano-metric channels width are achieved by using a photolithography, not by an e-beam, • it uses relatively low implantation energies and doses, less than 50keV and 110 14 at/cm 2 , • it forms an effective electrical isolation beneath the 2DEG channels, • it does not require thick buffer layer and/or high quality of substrate. Fig. 3. Impact of the implantation energies on the isolation depth into the epi-layer and on the effective width of 2DEG. These SRIM simulation results demonstrate the efficiency of the ion implantation to (i) achieve a nano-metric channel width using optical lithography and (ii) to isolate the area beneath the 2DEG.

In order (i) to evaluate the efficiency of N + implantation on the isolation and (ii) to validate experimentally the optimized implantation energies, summarized in Table I, two TLM structures are designed and then fabricated. The breakdown electric fields of these structures are later measured and compared. The first TLM, implemented to check the quality of the isolation, consists of two 100 µm wide ohmic contacts separated by a distance of 10 µm. The active area between the two ohmic electrodes of this TLM is isolated by N + This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset.

PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0080240

implantation with multiple energies of 20, 50, 100 and 150 keV, and doses of 0.25, 1, 1.5, 2.5 × 10 14 at/cm 2 , respectively. The second TLM, designed to validate the optimized implantation conditions, has the same width and length as the first TLM. However, an interdigital fingers (IF) pattern, very similar to the NRs used in the GaN HEMTs, are fabricated in between the ohmic electrodes (see inset of Fig. 4). The space between the interdigital fingers is N + implanted with the energies and doses presented in Table 1.

Fig. 4 presents the measured current-electric field characteristics of the first TLM (without IF) and the second TLM (with IF for the three samples). It is noted that the breakdown electric field increases as the implantation energy increases in the second TLM structure. It varies from 0.9 MV/cm to 1.35 MV/cm, and 1.64 MV/cm at a current of 1 µA for the sample A, B, and C, respectively. As previously described, using small openings and, even with relatively low N + implantation energies and doses (less 50 keV and 110 14 at/cm 2 ), lead to a deeper material isolation and, thus, higher breakdown electric fields. For large openings, e.g. the first TLM, even a high implantation energy of 150 keV is not sufficient to reach a depth into the epi-layer. This explains the relatively low breakdown field of 0.35 MV/cm measured in the first TLM (without IF). The output current density of the optimized NR-HEMT (NR-HEMT C) is much larger than that of the conventional HEMT. For example, at VDS= 10 V; VGS = 1 V, the maximum current density, ID,Saturation, for NR-HEMT C is as high as 3.9 A/mm, which is approx. ∼460% higher than 0.7 A/mm obtained for the conventional HEMT (Fig. 6b). This is consistent with the expectation that the NR-HEMT structures have better themal management and higher current control This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. All NR-HEMT samples have clearly demonstrated improved off-current (IOFF) and better linearity in the transconductance, gm, as shown in Fig. 7. The NR-HEMT C features a reduction in IOFF of ∼2 orders of magnitude compared to the conventional HEMT, revealing a lower charge trapping effect. The higher linearity in gm of NR channel devices validates the reported mechanism described in 16 . In conventional HEMT, the extrinsic gm drops quickly when increasing the drain current after reaching its peak value, and this issue becomes more important as the gate length scales down. Several theories were proposed over the years to explain this behavior. Palacios et al. 20 , DiSanto et al. 21 , and Trew et al. 22 correlate this behavior with the increase of the source access resistance, RS, and showed that intrinsic devices without the access resistance can have a flat gm. This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset. PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0080240

PLEASE CITE THIS ARTICLE AS

Since the on-state performance of the NR-HEMTs can be affected by the involved isolation technique, both RON and saturation current IDS, Saturation of our fabricated NR-HEMTs (A, B and C) are benchmarked against the state-of-the-art of GaN NR-HEMTs in Fig. 9. The NR-HEMT C performs a low RON of 0.8 and 0.7 Ω.mm at VGS= 0 V and VGS= 1 V, respectively. This is the lowest RON for NR-HEMTs (In,Ga)AlN/GaN on a silicon substrate. The RON for all referenced 13-16,26-32 devices were extracted and/or re-calculated based on the reported data.

The key DC parameters of both NR-HEMTs and conventional HEMT, are extracted and given in Table II. Usually, the smaller the subthreshold slope (SS) is, the higher the off-state performance of the device will be. Conventional HEMT features a SS of 730 mV/decade, while NR-HEMT exhibits a much lower value of 210 mV/decade. This demonstrates a better off-state performance of NR-HEMT. The SS values of the other NR-HEMT samples are lower than those of conventional HEMTs, divulging a reduced electron trapping effect and an enhancement of the gate control capability. The threshold voltage (Vth) of the conventional HEMT is about -7.5 V. However, NR-HEMTs have reduced Vth of about -5.3, -4.8, -4.9 V, respectively. This positive shift of Vth, in respect to the Vth of the conventional HEMT, is the consequence of decreased active area in NR-HEMTs due to the N + implantation, diminution of the effective 2DEG concentration. All Vth values are extracted by a constant-current method, which was defined as the gate voltage where the drain current reached 1 mA/mm.

Ref HEMT NR-HEMTs

In summary, a low-cost process technology, based on N + implantation of nanoribbons and thin GaN buffer layer, has been developed for AlGaN/GaN HEMTs.

The N + implantation conditions, energy and dose, have been simulated/optimized and then evaluated/validated experimentally. We demonstrated that a successive implantations, with low energies of 20 keV followed by 50 keV, leads to an excellent isolation of the area below the 2DEG channel. A nano-metric channel width of 65 nm has been achieved by using the photolithography, a cost effective process. As results, a much higher breakdown field has been observed for the NR-HEMTs when compared to conventional AlGaN/GaN HEMT.

The fabricated/optimized AlGaN/GaN NR-HEMT has shown an ON/OFF current ratio more than two orders of magnitude larger, ∼2 orders of magnitude lower IOFF current. The RON value of this NR-HEMT at VGS= 1 V is as low as 0.7 Ω.mm, around 10 times lower than that of the conventional AlGaN/GaN HEMT. These enhanced static properties have resulted in AlGaN/GaN NR-HEMT with ∼163-435% higher drain current density than that of conventional HEMTs. We found that the optimized process has led to (i) improving the linearity of the transconductance gm, (ii) lowering the RS and (iii) steepening the subthreshold slope of the AlGaN/GaN NR-HEMT. Overall, the results indicate that nanoribbon channels structure fabricated by nitrogen ions implantation can be a favorable way to manufacture devices for high-power switching application.

Fig. 1 .

 1 Fig. 1. (a) Schematic cross-section of the HEMT epi-layers grown by MOCVD on Si (111) substrate. (b) Targeted AlGaN/GaN heterojunction nanoribbon, made by N + ionic implantation.

Fig. 2 .

 2 Fig. 2. Fabrication process flow of the conventional AlGaN/GaN HEMT (left panel) and of the nanoribbon (NR) AlGaN/GaN HEMT (right panel). Both conventional and NR HEMTs are fabricated on the same wafer.

  effect of the N + ion energy on the quality of the isolation, three samples (A, B and C) are considered. All samples are implanted twice. During the first N + implantation, an energy of 20 keV is used for all samples. Then, different ion energies of 30 keV, 40 keV and 50 keV are used throughout the second implantation for the samples A, B and C, respectively.

Fig. 4 .

 4 Fig. 4. Current-Electric field characteristics of the TLM without interdigital fingers (IF) and with IF (samples A, B, and C). Inset shows the top-view SEM images of the TLM with and without interdigital fingers. Afterwards, two types of transistor are fabricated, (i) conventional HEMT without NRs (ref-HEMT) and (ii) NR-HEMTs using the optimized N + implantation energies and doses. The top views of these transistors, obtained by Scanning Electron Microscope (SEM), are shown in Fig. 5. The DC output characteristics of the conventional HEMT, used as a reference, and of the NR-HEMTs are compared in Fig. 6a. For the NR-HEMTs, the DC current density are normalized by the effective channel width (Weff = WNR × NNR, where WNR is the NR width

Fig. 5 .

 5 Fig. 5. Top view SEM images of (a) the AlGaN/GaN NR-HEMT and (b) conventional AlGaN/GaN HEMT. The length and width of NR are 2 μm and 250 nm, respectively. The gate length and source-todrain spacing are 450 nm and 5 μm, respectively.

Fig. 6 .

 6 Fig. 6. (a) IDS-VDS DC output characteristic of the fabricated conventional and NR AlGaN/GaN HEMTs. VDS sweeping is from 0V to 10 V and VGS values are for 1 V, -3 V and -7 V. (b) The extracted values of the on-resistance, RON, and the drain saturation current, IDS, Satutration.

  DOI: 10.1063/5.0080240 when compared to the conventional HEMTs 15-19 . The RON of the conventional HEMT and NR-HEMTs A, B, and C at VGS= 0 V, extracted from IDS-VDS sweeps in the linear region (Fig. 6b), are 8.3, 2.8, 1.5 and 0.8 Ω.mm, respectively. The NR-HEMT has demonstrated a much smaller RON, in contrast to the conventional HEMT.

Fig. 7 .

 7 Fig. 7. IDS-VGS and transconductance, gm, transfer characteristics of the fabricated conventional HEMT and NR-HEMTs, measured at the drain bias VDS= 8 V.To quantitatively evaluate the linearity performance of the different samples, a figure of merit namely gatevoltage-swing (GVS) is derived. It is based on the gate voltage range, where a device parameter, i.e. gm, stays larger than 80% of its maximum value[START_REF] Liu | The 5th European Microwave Integrated Circuits Conference[END_REF] . The corresponding GVS values of the conventional HEMT device is 2 V (from -4 to -2 V). The NR-HEMT C device shows a better linearity of GVS = 4 V (from -3.5 to 0.5 V).The measured source resistance, RS, as a function of gate current, IGS, for the different samples is shown in Fig.8. The measurement setup adopts the gate current injection method 24,25 , as illustrated in the inset of Fig.8. Initially, as IGS increases from 0.01 mA/mm up to IGS ≃ 1 mA/mm, RS values of all samples drop down

Fig. 8 .

 8 Fig. 8. RS-IGS transfer characteristics of the investigated NR-HEMTs and conventional HEMT. The inset illustrates the used gate-currentinjection technique.

Fig. 9 .

 9 Fig. 9. Summary on the static on-resistance, Ron, and on the saturation current, Isat, of state-of-the-art AlGaN/GaN NR-HEMTs. (a) VGS=0V, (b) VGS=1V.

  Figure of merit GVS a (V)

  -Swing (GVS), where the device parameter remains ≥80% of its maximum value.

TABLE I .

 I Implantation energies and N + doses for each sample

TABLE II .

 II The main DC characteristics of the benchmarked devices (A, B and C) versus the conventional HEMT.

This is the author's peer reviewed, accepted manuscript. However, the online version of record will be different from this version once it has been copyedited and typeset.PLEASE CITE THIS ARTICLE AS DOI: 10.1063/5.0080240

Acknowledgment

This work has been supported by GANEX (a public funded 'Investissements d'Avenir' program managed by the French ANR agency), by the French council region of Lorraine "Region Lorraine" and by the ANR project Cleaning ANR-15-CE09-0019.

Data Availability

The data that support the findings of this study are available from the corresponding author upon reasonable request.


Necro Louis Noizet

Alan Schmitt

Stating and Handling Semantics with

Keywords: Skel, Necro, semantics, skeletal semantics, OCaml, Coq, formalization Skel, Necro, sémantique, sémantique squelettique, OCaml, Coq, formalisation

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

Introduction

In order to formally prove properties of a programming language, or programs in said 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.

• Skel is designed to be light: it is easy to understand its semantics. Also, a light language guarantees an easy maintainability and facilitates the development of tools to handle it.

• Skel is powerful enough to express intricate semantical features, as proven by its use in an ongoing formalization of JavaScript's semantics [START_REF] Khayam | Jskel: Towards a formalization of javascript's semantics[END_REF].

• A semantics described in Skel can be close to a previously written formulation, be it as inference rules or as an algorithmic specification.

• Necro provides a comprehensive and extensible set of tools to manipulate said semantics.

For instance, to translate it into an interpreter (Necro ML, see Section 4.2), or to give a formalization in the proof assistant Coq (Necro Coq, see Section 4.3).

Skel is a statically strongly typed language. First introduced in [START_REF] Bodin | Skeletal Semantics and their Interpretations[END_REF], we redesigned it, with a syntax closely based on ML, whose simplicity and expressiveness are well-known. We also added support for polymorphism and higher order.

One can think of Skel as a kind of programming language, or one can think of it as a language to define inductive rules. Both approach make sense, and they are both interesting respectively when writing a semantics whose formalization is a computational one, (e.g. ECMA-262 [16]), or when writing a semantics defined with inferrence rules (e.g. λ-calculus). Since it has been created to talk about semantics, Skel allows to talk about partiality and non-determinism Necro contains several tools to manipulate skeletal semantics (semantics written in the language Skel). First, necrolib offers basic functionalities (parsing, typing, printing, and simple transformations). It is provided as a library to enable anyone to manipulate the AST to produce whatever tool they desire. Furthermore, we also provide the tools necroml, necrocoq, and necrodebug, that use said library, and generate respectively an OCaml interpreter, a Coq formalization, and a debugger.

Let us describe how one specifies a semantics in Skel using the simple imperative language IMP as example.

A skeletal semantics is a list of declarations. There are two kinds of declarations, namely type declarations and term declarations. These declarations can be either declaration of an unspecified type/term, or a specified one, in which case we give its definition.

When a type is unspecified, we only give its name. For instance, when writing the semantics of IMP, we might not want to specify how literals or integers are internally represented, so we declare:

type literal type int

When a type is specified, there are several ways to formalize its definition. One can declare a variant type (i.e., an algebraic data type), by giving the list of its constructors together with their input type. One can declare a type alias with the := notation. One can also declare a record type by listing its fields and their expected types.

For instance, keeping with the semantics of IMP, the type of expressions and statements would be defined that way: In this example, (expr, expr) is the product type with two components of type expr, see Figure 1 for more details.

An example for a record type is the following:

type euler_int = ( re: int , im: int ) And finally, an example of alias is the following:

type nat := int
Note that types are all implicitely mutually recursive, so the order in which they are given does not matter. Now let us present term declarations. To declare an unspecified term, we just give its name and type. To declare a specified term, we must also give its definition.

An instance of unspecified term is the addition. Since the type int was not specified, it is impossible to specify the addition, so we would declare: If it is not, then the first branch gives no result. Here, the two branches are exhaustive and don't overlap, so neg will only yield one result. In general, overlapping branches provide nondeterminism, and non-exhaustive branches provide partiality.

val add: int → int → int
Note that the first line, as is usual with OCaml for instance, is syntactic sugar for the following:

val neg: boolean → boolean = λ b : boolean →
The file while_better.sk, on the Necro Test repository1 gives IMP's semantics. The eval_stmt term is a more complete example. We extract the part that evaluates a while loop: The first line ensures that the evaluated statement is a While loop, and it extracts its components, using a destructuring pattern matching. The second line evaluates the expression and makes sure it is a boolean. Depending on the value of the boolean (first line of each inner branch), either the loop body is evaluated before evaluating the whole loop again, or the current state is returned.

Term t ::= x i | C t | (t, . . . , t) | λp : τ → S | t.f | (f = t, . . . , f = t) | t ← (f = t, . . . , f = t)

Skeletal semantics

In this Section, we introduce the formalism, typing, and semantics of Skel.

Formalism

Figure 1 contains the syntax of Skel terms and skeletons. This BNF does not include polymorphism for simplicity, it will be described in Section 2.4.

As we can see, there are two types of expressions, namely terms and skeletons. This is close to an Abstract Normal Forms [START_REF] Sabry | Reasoning about programs in continuation-passing style[END_REF]. The point is to separate what is intuitively an evaluated value to what is a computation. This way, the order of evaluation is always trivial as there is only one way to do an evaluation step in a skeleton.

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, a record of terms, or a term with reassignment of some fields.

A skeleton is either the application of a term to other terms, a let-binding, an existential (see Section 2.3), a branching, or simply the return of a term. We sometimes write ret t instead of t, to clearly state that we consider the skeleton and not the term.

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

Typing

Skel is a strongly typed language. As we can see in Section 2.1, there are a lot of type annotations. Every term declaration is given with a type, as well as every λ-abstraction. The reason is that, by design, Skel is meant to be explicitly typed. Polymorphism is ignored in this Section, but it is presented in Section 2.4, and we will see that the type arguments are also explicitly specified. Specifying every type might seem tedious at first, but it helps to improve confidence on the correction of the skeletal semantics. However, a future version of the typer may include a typeinference mechanism, for those adventurous or confident enough, as explained in Section 2. [START_REF] Danvy | Abstracting control[END_REF] To be able to give the typing rules for Skel, we must first define ctype(C) which returns the pair of the declared input type and output type for the constructor C in the type declaration list. For instance, if we define the type expr as shown in Section 1, we would have ctype(Const) = (literal, expr).

In the same way, we define ftype(f ) which returns (τ, ν) where τ is the type of the field f , and ν is the record type to which the field f belongs. For instance, if we define the type euler_int as shown in Section 1, we would have ftype(re) = (int, euler_int).

A field name cannot belong to two different record types, and a constructor name cannot be used twice, so the ftype and ctype function are well-defined.

The typing rules for terms and skeletons are given in Appendix A. They are respectively of the form Γ ⊢ t t : τ and Γ ⊢ S S : τ , where Γ is a typing environment (a partial functions from variable names to types).

They are pretty straightforward, and very similar to what exists in other functional languages. To type a λ-abstraction and a let-binding, we use a pattern-typing defined thereafter, using the partial function Γ + p → τ :

Γ + x → τ ≜ Γ, x : τ Γ + → τ ≜ Γ Γ + C p → ν ≜ Γ + p → τ , where ctype(C) = (τ, ν) Γ + (p 1 , . . . , p n ) → (τ 1 , . . . , τ n ) ≜ (Γ + p 1 → τ 1 ) . . . + p n → τ n Γ + (f 1 = p 1 , . . . , f n = p n ) → ν ≜ (Γ + p 1 → τ 1 ) . . . + p n → τ n , where fields(ν) = {f 1 : τ 1 , . . . , f n : τ n }
An empty branch can therefore be typed to any given type, but since Skel is strongly typed, it will reject any empty branching whose type is not explicitly specified.

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 interpretation, that corresponds to the usual natural semantics of a language [START_REF] Kahn | Natural semantics[END_REF]. One may also define an abstract interpretation, where unspecified types are given values in some abstract domain and Inria where the results from branches are all collected. Defining such an interpretation is beyond the scope of this paper Every skeleton and term is interpreted as a value, so we need to define the set in which we choose those values.

First, for every unspecified type b, we assume a set V b . For every variant type b ′ , the set V b ′ is the set freely generated by the constructors with their types. For tuple types, we use the cartesian product: the set V (τ1,...,τn) is V τ1 × • • • × V τn . For a record type, the set is a family of values. For instance, if b ′′ has fields {f 1 : τ 1 , . . . , f n : τ n }, we have

V b ′′ = {(f 1 = v 1 , . . . , f n = v n ) | v i ∈ V τi }.
For arrow types, we use relations, as the same skeleton can be evaluated to zero, one, or several values, because of branchings. So

V τ →ν = R(V τ , V ν ) = P(V τ × V ν ).
Next, we need to give a meaning to every unspecified term. So for each declaration val x : τ , we assume given a set of value x ⊆ V τ .

The rules for the concrete interpretation are given in Appendix B. They are of the form E, t ⇓ t v for terms and E, S ⇓ S v for skeletons, meaning that in the environment E (partial function matching variables to values), the term t (resp. the skeleton S) can evaluate to a value v.

In the App rule, the R * notation is used to represent the uncurried version of the relation. We define:

R * (v 1 , . . . , v n , w) ≜ ∃R 2 , . . . , R n , R(v 1 , R 2 ) ∧ R 2 (v 2 , R 3 ) • • • ∧ R n (v n , w)
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.

In the rules for the existential, as well as in the rules for let-in and closures, we use the partial function E + p → v. It is defined as follows.

E + x → v ≜ E, x : v E + → v ≜ E E + C p → C v ≜ E + p → v E + (p 1 , . . . , p n ) → (v 1 , . . . , v n ) ≜ (E + p 1 → v 1 ) . . . + p n → v n E + (f 1 = p 1 , . . . , f n = p n ) → (f 1 = v 1 , . . . , f n = v n ) ≜ (E + p 1 → v 1 ) . . . + p n → v n
As we can see, the concrete interpretation is relational. A skeleton or a term can be interpreted to 0, 1, or several values. The sources of partiality and non-determinism are threefold.

• A branching with no branch has no result, and can cause partiality; a branching with several branches can have several results and cause non-determinism.

• Unspecified terms can have any arbitrary number of interpretation, so they can cause both partiality and non-determinism.

• Pattern-matching can fail, and is therefore a source of partiality.

Polymorphism and type inference

For practical reasons, including the definition of monadic binders in Section 3, the type system also provides polymorphism. All type annotations are explicit. They are specified using angle brackets. Unspecified types, variant types, record types, and aliases can all 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.

The explicit typing is by design, considering that explicit type annotations reduce the risk of error. In the future, we will possibly add an option that would allow the typer to perform type inference. This option would possibly also infer the type of the arguments in λp:τ → sk constructs.

3 Monads in Skel 3.1 Custom binders Some executable semantics specifications, such as ECMA-262 [16], make extensive but implicit use of monads, for instance to carry state, propagate exceptions, or suspend computations. Skel has a built-in system to handle monadic binds, making it easier to use them, and making the written Skel code easily readable and close to the specification [START_REF] Khayam | Jskel: Towards a formalization of javascript's semantics[END_REF].

Assume that a term bind<a,b> is defined, with the type m<a> → (a → m<b>) → m<b> where m<•> is a monad, for instance the state monad. Then, one can use the following notation:

let p =%bind s1 in s2
In this case, the type arguments for bind are inferred (they can also be explicitly given if desired), and the result is semantically the same as bind s1 (λp → s2) (with all the proper type annotations added).

For instance, we can rewrite the semantics of IMP within a state monad, which makes the code more easily readable, and avoids mistakes in state manipulations. Here is the monad: Note that a semicolon construct s1; s2 is syntactic sugar for let _ = s1 in s2. Monadic notation also applies to this sequencing operator.

The type of bind does not have to be the type of a monadic bind to be used as notation, it can be any type as long as the second argument is an arrow type, and it is interpreted in the exact same way. This may be necessary when handling several monads at the same time, or when a bind-like operator is not monadic.

Necro Trans

Necro Lib (cf. Section 4.1) provides a tool, called Necro Trans, which performs transformations on skeletal semantics. One of the provided transformers inlines custom binders. This allows to remove all monads out of a semantics. Along with the explode transformer, which duplicates code so as to push all branches to the same level, an option monad can be inlined and still provide readable code. In the same way, using the eta transformer, which performs η-expansion and then some β-reduction, we can inline a state monad and still get something readable.

For instance, here is a part of the semantics of IMP, using state monads: which is close to what would have been written by hand and is easily understandable. This is useful for instance when debugging a semantics, using necrodebug (see Section 4.4).

The Necro Ecosystem

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

Necro Lib

Necro Lib [START_REF] Noizet | Necro Library[END_REF] is Necro's centerpiece. It generates an OCaml library file, necro.cma. This library 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 (Section 3.2), which 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 the tools Necro ML (Section 4.2), Necro Coq (Section 4.3), and Necro Debug (Section 4.4).

Inria

Necro ML

Necro ML [START_REF] Crance | Necro Ocaml Generator[END_REF] is a generator of OCaml interpreters. Given a skeletal semantics, it produces an OCaml functor. This functor expects as arguments a specification (written in OCaml) 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 corresponding to the branching construct (pattern matching is deterministic in OCaml). So types and terms are shallowly embedded, but the skeletons are deeply embedded. We use an interpretation monad that specifies, among 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 and module types.

• The TYPES module type contains all unspecified types. The user must produce a module for them.

• The MONAD module type is the module type for the interpretation monad mentioned above and detailed in Section 4.2.2. It states how let-ins, branches, and applications are computed.

• The UNSPEC module type contains all types, specified and unspecified, the signature of unspecified terms, and the interpretation monad. The latter is present since the choice of monad can have an effect on the definition of the unspecified terms.

• The Unspec functor takes the instantiation of the unspecified types and the chosen monad, and it produces a default module of type UNSPEC containing all type information and a default implementation of unspecified terms. This implementation simply raises a NotImplemented error. It is not meant to be used as is, but to be overridden with the actual implementation of the unspecified terms.

• The INTERPRETER module type is the module type for the interpreter of the described language. It extends the UNSPEC type with the signature for specified terms.

• The MakeInterpreter functor takes the instantiation of unspecified types and unspecified terms, typically derived from the application of the Unspec functor, and it produces an interpreter for the language.

In summation, to produce an interpreter, the user only has to do the following:

• write a module of type TYPES, to implement the unspecified types;

• choose an interpretation monad of type MONAD or write their own; the proposed interpretation monads are in file necromonads.ml of Necro ML's repository;

• apply the Unspec functor then override all unspecified terms with their actual implementation;

• apply the MakeInterpreter functor to generate the code for the specified terms.

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

Interpretation monad

The interpretation monad is defined in the following way, 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

There is some similarity between bind and apply. The difference is that bind is used to translate let-in constructs, therefore it expects a skeleton of type 'a t, and apply is used to translate application to a term, and therefore expects a value of type 'a (remember that skeletons are deeply embedded, while terms are only shallowly embedded).

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. It is defined as follows. This monad is the easiest to use, and it works perfectly fine in most cases. However, the issue with this monad is that we always take the first branch that succeeds, but if we find out later that it was not the right branch, there is no way to get back to another branch. For instance, for the following code, calling fail () will raise the Branch_fail exception even though () is a valid interpretation. As we mentioned, the main problem is the inability to backtrack. To fix this, we propose a continuation monad, which uses failure continuations to keep track of all branches that were not taken, therefore giving the possibility to backtrack if a branch fails [START_REF] Danvy | Abstracting control[END_REF]. This time, the execution of the same example will choose the first branch, but it keeps in its failure continuation the content of the second branch. Then, when executing f x, it will fail, and unstack its failure continuation. It will then backtrack to the second branch, and succeed with the result ().

Nevertheless, the continuation monad is not complete in relation to the concrete interpretation, as it always begins by executing the first branch, 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 the proposed monads is available online2

Necro Coq

Necro Coq [START_REF] Noizet | Necro Gallina Generator[END_REF] is a tool that allows to embed a given skeletal semantics into a Coq formalization. It can then be used to prove correction of a given program or to prove language properties.

Interpretation

The file Concrete.v provides the concrete interpretation for skeletons. It uses Coq's induction to define the relations interp_skel and interp_term, which relates skeletons (respectively 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 e can be extended into e ′ by mapping p to v, that is e ′ = e + p → v

The file Concrete.v provides the interpretation using big-step evaluation, but we also provide a file Concrete_ss.v which does a small-step evaluation.

Another 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 we may iterate this step. It is closest to the initial definition in [START_REF] Bodin | Skeletal Semantics and their Interpretations[END_REF]. The purpose of this file is to be able to perform a strong induction on interp_skel in a very easy fashion.

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 given moment.

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 may want to use this one is, given the skeletal semantics of lambda-calculus, if we want to derive the induction property for lambda-terms. This property is the following:

(∀x ∈ X, P x ) → (∀M N ∈ Λ, P M → P N → P M N ) → (∀x ∈ X, ∀M ∈ Λ, P M → P λx•M ) → ∀M ∈ Λ, P M .
Since Skel is deeply embedded, one evaluation step in the language matches 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 equivalent, it is sufficient to 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:

S : τ S → S ′ S ′ : τ
where S and S' are extended skeletons.

Extended skeletons can be actual skeletons, in which case the type_ext_skel property is equivalent to well_formed_skel defined in the file WellFormed.v. They can also be values, signaling that the computation is over, in which case the type_ext_skel property asserts that the value is in V τ With this theorem proven, and since Concrete_ss.v and Concrete.v are equivalent, we have the following:

∅ ⊢ S : τ S S ⇓ v v ∈ V τ

Unspecified functional values

There is one other issue that needs to be addressed. 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 which, 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 {([x; y], x + y) | x, y ∈ N}.

There are operational and denotational approaches to represent this in Coq. The file Concrete.v (as well as its variants Concrete_ss.v and ConcreteRec.v) provides an implementation for the operational approach.

In these files, there is a constructor for unspecified functional terms that are 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.

The file Concrete2.v (as well as Concrete2_ss.v and Concrete2Rec.v) provides an implementation for the denotational approach.

In these files, unspecified functions are defined using the following extensive constructor:

| cval_func: forall A, (A -> cvalue * cvalue) -> cvalue
This is basically the same as using a relation, but in a declarative way instead of predicative, to agree with Coq's positivity requirements. As we have not identified that one approach is better than the other, we provide both and let the user choose the most convenient for the task at hand.

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 correction 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 lambda-calculus extended with natural numbers (test/lambda folder).

In addition, it has been used in [START_REF] Ambal | Automatic Transformation of a Big-Step Skeletal Semantics into Small-Step[END_REF] to provide the a posteriori proof of an automatic generic transformation of a big step semantics into a small step semantics.

Inria

Necro Debug

In the process of writing a semantics, it is usual and natural to make mistakes. To track them, any good language should provide a way to debug a code written using it. This is what Necro Debug offers. It is a relatively recent tool, and is therefore still in its infancy, but it is already usable.

Necro Debug [START_REF] Noizet | Necro Ocaml Debugger[END_REF] is a debugger generator. Given the skeletal semantics of a language and the AST of a program written in this language, it provides a step by step execution, using an abstract machine interpretation of Skel. We provide two user interfaces. One is in a terminal, and the second one is an HTML page, using js_of_ocaml.

To use it, it is required to provide the interpretation for unspecified types and terms, in the same way that they would be provided in Necro ML with the ID monad. The user can also provide a printing function for unspecified types, or use the default value, which prints for instance <int> for every value of type int. The user can therefore use the same instantiation for the debugger and necroml, and only needs to extend it with printing functions in the debugger.

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 [START_REF] Bodin | Skeletal Semantics and their Interpretations[END_REF]. We significantly improve on their 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 [START_REF] Bodin | Skeletal Semantics and their Interpretations[END_REF] were written by hand, they can now be automatically generated. Generation of OCaml code was also proposed in [START_REF] Courant | Necro: Animating Skeletons[END_REF], but it was only available for the language of [START_REF] Bodin | Skeletal Semantics and their Interpretations[END_REF], which was less powerful than the current language.

On the process of formalizing semantics, several tools already exist, but they are heavier and more complex than Skel. This is the case of Lem [START_REF] Mulligan | Lem: Reusable engineering of real-world semantics[END_REF] and Ott [15]. The lightness of Skel (the file skeltypes.mli describing Skel's AST is only 108 lines of specification) allows anyone to easily write a tool handling skeletal semantics. This is more complex with Lem and Ott, as they provide 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 [START_REF] Li | Isak: A complete semantics of K[END_REF] 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. 3 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 [START_REF]Nomadic Labs. coq-of-ocaml[END_REF] to go the other way). One may then execute the semantics using the OCaml version and ++++e 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.

Conclusion

The language 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 feature. The tools Necro provide, especially Necro ML and Necro Debug, help in the process of writing a semantics. Necro Coq and Necro Trans allow to manipulate and certify these semantics once written. They give the necessary framework to prove program correction 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 in the JSkel project [START_REF] Khayam | Jskel: Towards a formalization of javascript's semantics[END_REF].

Though we did not mention it in this paper, Skel allows to define semantics in several files, but in this case, Necro Coq is not yet able to generate a Coq formalization. A future task is to implement this functionality in Necro Coq. 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.

Another tool that is under implementation is Necro Tex, a generator of formatted T E X rules corresponding to a skeletal semantics.

Inria

A Typing rules for Skeletal Semantics

= t n ) ⇓ t (f 1 = v i , . . . , f n = v n ) Rec E, t ⇓ t (f 1 = v 1 , . . . , f n = v n ) ∀i, E, t i ⇓ t w ji i ̸ ∈ {j 1 , . . . , j m } → w i = v i E, t ← (f j1 = t 1 , . . . , f jm = t m ) ⇓ t (f 1 = w 1 , . . . , f n = w n ) FieldSet E, t ⇓ t v E,

  ident, expr) | Seq (stmt, stmt) | If (expr, stmt, stmt) | While (expr, stmt)

  Assuming we have defined booleans to be type boolean = | True | False, a simple example of a specified term is the following. val neg (b:boolean): boolean = branch let True = b in False or let False = b in True end The branch ... or ... end construct is a Skel primitive to deal with non-deterministic choice. The destructuring pattern matching let True = b in asserts that b is equal to True.

Figure 1 :

 1 Figure 1: The syntax of Skel (without polymorphism)

(

  * Unspecified *) type list<_> (* Variant *) type union<a,b> = | InjL a | InjR b (* Record *) type pair<a,b> = (left: a, right: 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 let Cons (a, qa) = l in let b = f a in let qb = map<a,b> f qa in Cons<b> (b, qb) end

  type st<a> := state → (a, state) val bind<a, b> (a:st<a>) (f:a → st<b>): st<b> = Inria λ s : state → let (a, s) = a s in f a s val ret<a> (a:a): st<a> = λ s : state → (a, s) Using this monad, we can rewrite the evaluation of a while loop presented in Section 1 as follows. val eval_stmt (t:stmt): st<()> = branch let While (cond, t') = t in let Bool b =%bind eval_expr cond in branch let True = b in eval_stmt t' ;%bind eval_stmt t or let False = b in ret<()> () end or ... end

Figure 2 :

 2 Figure 2: The Necro ecosystem

  module ID = struct exception Branch_fail of string type 'a t = 'a let ret x = x let rec branch l = begin match l with | [] -> raise (Branch_fail "No branch matches") | b1 :: bq -> try b1 () with Branch_fail _ -> branch bq end let fail s = raise (Branch_fail s) let bind x f = f x let apply f x = f x let extract x = x end

module

  ContPoly = struct type 'b fcont = string -> 'b type ('a,'b) cont = 'a -> 'b fcont -> 'b type 'a t = { cont: 'b. (('a,'b) cont -> 'b fcont -> 'b) } let ret (x: 'a) = { cont = fun k fcont -> k x fcont } let bind (x: 'a t) (f: 'a -> 'b t) : 'b t = { 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

  TermUnspec E, t ⇓ t v E, (C t) ⇓ t C v Const E, t 1 ⇓ t v 1 . . . E, t n ⇓ t v n E, (t 1 , . . . , t n ) ⇓ t (v 1 , . . . , v n ) Tuple R ⊆ {(v, w) | v ∈ V τ ∧ (E + p → v), S ⇓ S w} E, (λp : τ → S) ⇓ t R Clos E, t ⇓ t (f 1 = v 1 , . . . , f n = v n ) E, t.f i ⇓ t v i FieldGet E, t ⇓ t (v 1 , . . . , v m ) 1 ≤ i ≤ m E, t.i ⇓ t v i TupleGet ∀i, E, t i ⇓ t v i E, (f 1 = t 1 , . . . , f n

	B Concrete Interpretation of Skeletal Semantics
		E(x) = v		val x:τ = t	∅, t ⇓ t v
		E, x ⇓ t v	Var	E, x ⇓ t v	TermSpec
		val x : τ	v ∈ x
		E, x ⇓ t v
		val x:τ (= t)
	Var	Γ ⊢ t x : τ

Γ(x) = τ Γ ⊢ t x : τ

  ret t ⇓ S v Ret E, S i ⇓ S v E, (S 1 . . . S n ) ⇓ S v Branch E, S ⇓ S v E + p → v, S ′ ⇓ S w E, let p = S in S ′ ⇓ S w Exist ∀i E, t i ⇓ t v i E, t 0 ⇓ t R R * (v 1 , . . . , v n , w) E, (t 0 t 1 . . . t n ) ⇓ S w

	App
	Inria

LetIn

v ∈ V τ E + p → v, S ⇓ S w E, let p : τ in S ⇓ S w

RR n°9449

https://gitlab.inria.fr/skeletons/necro-test/-/blob/FSCD2022/while_better.sk Inria

https://gitlab.inria.fr/skeletons/necro-ml/-/blob/FSCD2022/necromonads.ml RR n°9449

https://sympa.inria.fr/sympa/arc/coq-club/2020-02/msg00066.html RR n°9449

Term Γ ⊢ t t : τ ctype(C) = (τ, τ ′ ) Γ ⊢ t C t : τ ′ Const ∀i, Γ ⊢ t t i : τ i Γ ⊢ t (t 1 , . . . , t n ) : (τ 1 , . . . , τ n ) Tuple Γ + p → τ ⊢ S S : τ ′ Γ ⊢ t (λp : τ → S) : τ → τ ′ Clos Γ ⊢ t t : ν ftype(f i ) = (τ, ν) Γ ⊢ t t.f i : τ FieldGet Γ ⊢ t t : (τ 1 , . . . , τ m ) 1 ≤ i ≤ m Γ ⊢ t t.i : τ i TupleGet fields(τ ) = {f 1 : τ 1 , . . . , f n : τ n } ∀i, Γ ⊢ t t i : τ i Γ ⊢ t (f 1 = t 1 , . . . , f n = t n ) : τ Rec Γ ⊢ t t : τ ∀i, Γ ⊢ t t i : τ i ∀i, ftype f i = (τ i , τ ) Γ ⊢ t t ← (f 1 = t 1 , . . . , f m = t m ) : τ FieldSet Γ ⊢ t t : τ Γ ⊢ S ret t : τ Ret Γ ⊢ S S 1 : τ . . . Γ ⊢ S S n : τ Γ ⊢ S (S 1 . . . S n ) : τ Branch Γ ⊢ S S : τ Γ + p → τ ⊢ S S ′ : τ ′ Γ ⊢ S let p = S in S ′ : τ ′ LetIn Γ + p → τ ⊢ S S : τ ′ Γ ⊢ S let p : τ in S : τ ′ Exist ∀i Γ ⊢ t t i : τ i Γ ⊢ t 0 : τ 1 → • • • → τ n → τ Γ ⊢ S (t 0 t 1 . . . t n ) : τ

Inria

Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

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 4.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, presented in Section 4.3.4

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 with the basic constructs (the definition of a type, a skeleton, . . . ).

For instance, here is the mutual definition of terms and skeletons:

Values

The values used to store 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.

Inductive cvalue : Type

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 (here, 1 is in the scope of Z, which means it is equal to Zpos xH)

The next two constructors are straightforward. The fourth one is a closure constructor, to store lambda-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 in Section 4.3.5.

Inria


Maciej Malinowski

Thanh Van Tran

Morgane De Robichon

Nadège Lubin-Germain
email: nadege.lubin-germain@u-cergy.fr

Angélique Ferry
email: angelique.ferry@u-cergy.fr

Mild Palladium-Catalyzed Cyanation of Unprotected 2-Iodoglycals in Aqueous Media as Versatile Tool to Access Diverse C2-Glycoanalogues

Keywords: unprotected glycosides, palladium catalysis, cyanation, aqueous media, 2-iodoglycals Scheme 1. Different strategies for palladium-catalyzed crosscouplings on 2-iodoglycals

Access to unprotected 2-cyano-glycals via a mild palladium-catalyzed cyanation of protecting groups-free 2-iodoglycals in aqueous media has been developed. Diverse glycal substrates including disaccharide-type were successfully obtained in good to excellent yields. These unprotected 2-cyano-glycal scaffolds were successfully derivatized to different C2-glycoanalogues.

Introduction

The ubiquitous involvements of carbohydrate derivatives in biological responses has motivated the chemist community to develop synthetic tools to reach natural and unnatural analogues. [1] Design of unnatural mimics was largely explored in order to circumvent drawbacks of natural sugars. The main issue encountered by these biomolecules is related to their poor stability due to the sensitivity of natural CÀ O and CÀ N bonds. Enzymatically and chemically stable C-branched glycosides possessing an unnatural CÀ C bond were thus highly investigated. [2] Among the current synthetic routes to form CÀ C bonds on sugars, metal-catalyzed crosscouplings emerged as new powerful tools. In particular, during this last decade, 2-iodoglycal substrates attracted attention, due to their suitable reactivity in palladium-catalyzed processes. By this way, diverse C2-glycoanalogues were reached via classical Suzuki, Sonogashira, Heck, etc. cross-couplings. More recently, carbonylative reactions applied to 2-iodoglycals emerged (Scheme 1). [3] All these methodologies were carried out almost exclusively on O-protected iodoglycals (mostly acetylated or benzylated) except a single example of thiolation described by Messaoudi et al. on unprotected 2-iodo-d-glucal in organic media leading to moderate yield. [3h] Indeed, the use of unprotected carbohydrates as starting substrates raises many solubility and purification challenges as well as side reactivities due to the presence of numerous free hydroxyl groups. [4] Nevertheless, access to unprotected glycoanalogues in an acceptable scale is crucial for biological applications. Most of the current literature involving 2-iodoglycals does not deal with the deprotection of the obtained C2-glycals. However, deprotection may become challenging depending on the sensitivity of the introduced function. Indeed, peracetylated sugars are usually deprotected in basic conditions, [5] which are incompatible with many functionalities. Similarly, hydrogenolysis, commonly used to remove benzyl protecting groups, [3i] could be deleterious in the presence of unsaturated functions. These limitations can constitute a dead end if the functional group introduced on the sugar reacts both with base and in the presence of hydrogen. One of the best examples is certainly the nitrile group. Moreover, nitrile is a particularly interesting functionality, which can be derivatized in many functions such as amide, carbonyl, tetrazole, amine, etc. Thus, C2-cyanoglycals appear to be potential versatile structures to access diverse glycoside derivatives. The first and only description of a procedure to synthesize such compounds in a protected version was by Hall et al. in 1973 using chlorosulfonyl isocyanate as cyanating reagent. This method was applied only on few examples in poor to modest yields. [6] Our strategy to reach these analogues was the opposite of the described literature on 2-iodoglycals. We decided to explore a new concept, to set the deprotection step before the introduction of the sensitive function (nitrile in our case). In consequence, this strategy required the development of both cyanation and subsequent derivatization steps on unprotected polar glycals (Scheme 1). Herein, we describe an access to diverse protecting groups-free C2-glycoanalogues via a key mild palladium-catalyzed cyanation reaction in aqueous media on unprotected 2-iodoglycals.

Results and Discussion

The introduction of a nitrile group on aromatic substrates via palladium-catalyzed cross-coupling was largely explored in organic media [7] and was studied, to a lesser extent, in aqueous media at temperatures generally higher than 100 °C. [8] In terms of cyanating reagent, our choice turned to a non-toxic, inexpensive cyanide source namely potassium ferrocyanide (K 4 [Fe (CN) 6 ]). This reagent attracted more and more attention thanks to its non-hazardous properties and was already successfully used in many cyanation reactions. [7a] We started our methodology investigation on 2-iodo-d-glucal 1 a, obtained in two steps from the commercially available peracetylated d-glucal (Table 1, for detailed study see SI). [3g] Inspired by Buchwald cyanation conditions applied to aromatic compounds, 1 a was reacted in the presence of a palladium precatalyst, a ligand, a sub-stoichiometric amount of base and K 4 [Fe(CN) 6 ] in a mixture (1:1) of 1,4-dioxane/water at 100 °C under argon atmosphere. [9] These conditions led to the formation of traces of the desired product 2 a (Table 1, entry 1). The use of tBuOH as organic co-solvent instead of 1,4-dioxane led to a good 62% yield in 2 a (Table 1, entry 2). Moreover, the solvent ratio of (1:1) appears to be crucial for the reactivity (Table 1, entries 3 and4). Indeed, it was shown that cyanation reactions using K 4 Table 1. Optimization of the cyanation reaction on 1 a. [a] Entry T (°C) Solvent (ratio) Precatalyst (eq) Ligand (eq) KOAc (eq) Yield (%) [b] 1 100 1,4-dioxane/H [a] Conditions: 1 (0.165 mmol), K 4 [Fe(CN) 6 ] (0.4 equiv.), "Pd" (X equiv.), ligand (X equiv.), KOAc (X equiv.), organic solvent/H 2 O (0.760 mL), under Ar, T°C, 16 h. [b] Determined by 1 H NMR using DMF as internal reference (see SI). [c] Corresponds to 56% isolated yield. [d] Under air atmosphere. [e] Corresponds to 85% isolated yield.

FULL PAPER asc.wiley-vch.de

[Fe(CN) 6 ] are optimal when cyanide anions are slowly delivered avoiding poisoning of the palladium complex. [8a] A decrease of the temperature to 75 °C yielded 2 a in a good 72% (Table 1, entry 5). Unreactive argon atmosphere was also a crucial parameter since only 11% of 2 a were obtained under air atmosphere (Table 1,entry 6). Satisfyingly, we could halve both the amounts of precatalyst and ligand without significant loss of yield (Table 1,entry 7). On the other hand, only a slight excess of base compared to precatalyst amount is needed and furnished the best result (2 a 90% yield, 85% isolated) (Table 1, entry 8). Indeed, the role of the base is assumed to be only the precatalyst activator. However, when the amounts of precatalyst, ligand and base were halved again, a modest yield of 44% was observed (Table 1,entry 9). The use of other couples of precatalysts/ligands was tested without any improvement (Table 1, entries 10-12). With the best conditions in hand (Table 1, entry 8), various unprotected 2-iodoglycals were engaged (Table 2). Several pyranoside glycal monosaccharides such as 2-iodo-d-galactal, 2-iodo-d-xylal as well as 2iodo-l-rhamnal could be converted into their cyanated analogues in excellent yields (Table 2,2 b,2 c,2

d).

Glycal disaccharide (2-iodo-d-lactal) presenting six free hydroxyl groups required the use of 8 mol% of Pd-XPhos-G3, 16 mol% of ligand XPhos and 10 mol% of KOAc to obtain 2 e in an excellent 83% yield (32% in standard conditions). Furanoside 2-iodo-d-ribal led successfully to the desired product 2 f in good yield (76% in standard way, 91% when the amount of catalytic system is doubled). Protected 2-iodo-dglucals (perbenzylated or persilylated) were also successfully engaged despite lower yields and required a higher reaction temperature (Table 2, 2 g and2 h). These results can be explained by a lower solubility of protected glycals in the media but also by stereoelectronic effects. In case of peracetylated 2-iodo-dglucal, only starting material or degradation was observed at temperatures between 75-130 °C (Table 2,2 i). This absence of reactivity could be correlated with the disarming effect of a fully ester protected sugar postulated in glycosylation reactions, which could reduce considerably the electron density of the double bond. [10] This hypothesis is supported by the fact that the presence of only one ester group on the primary hydroxyl group led to improved reactivity (Table 2,2 j). The mechanism of the reaction is expected to proceed via a classical Pd(0)/Pd(II)-catalytic cycle (Scheme 2). At first, the active Pd(0)-XPhos species (A) is generated. Secondly, an oxidative addition of Pd (0) (step 1) to the glycal CÀ I bond occurs to form Pd (II) complex B. Slow dissociation of K 4 Fe(CN) 6 produces cyanide anion, which forms complex C by ligand exchange. Finally, product 2 is obtained after reductive elimination with simultaneous reformation of Pd(0) species (A).

This methodology is thus an easy access to protecting groups-free 2-cyano-glycals. These scaffolds are interesting frameworks, which might be derivatized to many C2-glycoside derivatives (Table 3). Under hydrogen atmosphere in the presence of supported palladium catalyst, 2 a was converted into 2 e 83% [b] 2 f 76% (91%) [b] 2 g 51% [c] (65%) [b] 2 h 44% [c] 2 i 0% 2 j 71% [d] [a] Conditions: 2 (1 equiv.), K 4 [Fe(CN) 6 ] (0.4 equiv.), Pd-XPhos-G3 (4 mol%), XPhos (8 mol%), KOAc (5 mol%), t-BuOH/ H 2 O (1:1), under Ar, 75 °C, 16 h. [b] 8 mol% of [Pd], 16 mol% of XPhos and 10 mol% of KOAc were used. [c] Reactions were performed at 130 °C. [d] Reaction was performed at 90 °C.

Scheme 2. Proposed cyanation mechanism.

3 a where both nitrile and glycal double bond were reduced (Table 3, conditions A). Only one isomer was observed in 1 H-and 13 C-NMR and was isolated in 75% yield (Table 3, 3 a). The C2-manno-configuration of 3 a arising from an attack of H 2 by the less hindered face of the sugar, was assigned regarding both 1 Hcoupling constants and NOESY correlations (see SI). These conditions were applied successfully to 2 d furnishing 3 b in an excellent 83% yield as a single isomer with an axial CH 2 À NH 2 group (Table 3,3

b).

The selective reduction of the nitrile group without affecting the double bond was achieved by using NaBH 4 reagent in the presence of a cobalt salt in aqueous media (Table 3, conditions B). [11] Both 2 a and 2 c could be transformed by this method into the corresponding amino-glycal 4 in moderate to good yields (Table 3, 4 a and4 b). Compounds 3 and 4 are interesting platforms bearing a nucleophilic amine which can be used in peptide synthesis to reach original glycopeptide analogues. Nitriles 2 a and 2 f were then converted into their corresponding amide analogues 5 a and 5 b in good yields (Table 3, conditions C). [12] Heterocycles such as tetrazoles are also accessible from nitriles 2 by a cycloaddition reaction with sodium azide in good yields (Table 3, conditions D, 6 a and 6 b). [13] Finally, access to ketone derivatives from the 2-cyanoglycals 2 was possible by reaction with Grignard reagents, [14] exemplified on compounds 2 a and 2 d in very good yields (Table 3, 7 a and 7 b, conditions E). This method is complementary to our previous work dealing with carbonylative Suzuki-Miyaura cross-coupling on 2-iodoglycals which was applicable only for the synthesis of aryl and alkenylketones. [3l] Nevertheless, in this last work we faced to deprotection issues due to the sensitivity of the ketone function.

Conclusion

In summary, nitrile group was successfully introduced on unprotected 2-iodoglycals via a palladium-catalyzed process in aqueous media under mild conditions. dor l-pyranoside-, d-furanoside-, and disaccharide-type iodoglycals could be converted into their cyanated derivatives in good to excellent yields. The reactivity of the nitrile group allowed the possibility to reach five protecting groups-free C2-glycoanalogue families possessing amine, amide, tetrazole or ketone functionalities. The development of a strategy setting the deprotection step at an early stage of a synthesis provides unprotected glycosides bearing a sensitive functionality in an easier way.

Experimental Section General Experimental Methods

All chemical operations were carried out using standard sealed tubes. Acetonitrile was purified before use by distillation under an argon atmosphere. Tetrahydrofuran (THF) was distilled over Na/benzophenone under Ar. Other solvents were used without further purification. Commercially available chemicals were used as received unless otherwise stated. Pd-XantPhos-G3 was purchased from Sigma Aldrich, Pd-XPhos-G3, Pd-tBuXPhos-G3, Pd-BrettPhos-were synthesized from palladium dimer according to described procedure. [START_REF] Bruno | 920 FULL PAPER Mild Palladium-Catalyzed Cyanation of Unprotected 2-Iodoglycals in Aqueous Media as Versatile Tool to Access Diverse C2-Glycoanalogues[END_REF] Reactions were monitored by thin-layer chromatography on silica gel plates (60 F254

FULL PAPER

asc.wiley-vch.de aluminium sheets) which were rendered visible by ultraviolet and/or spraying with vanillin (15%) + sulfuric acid (2,5%) in EtOH followed by heating. 1 H NMR (400 MHz), 13 C NMR (100.5 MHz) were recorded at 298 K unless otherwise stated. Chemical shifts are given in ppm (δ) and are referenced to the internal solvent signal or to TMS used as an internal standard.

Multiplicities are declared as follows: s (singlet), bs (broad singlet), d (doublet), t (triplet), q (quadruplet), dd (doublet of doublet), ddd (doublet of doublet of doublet), dt (doublet of triplet), m (multiplet). Coupling constants J are given in Hz.

Infrared spectra (IR) were recorded on a FT-IR system using diamond window Dura SamplIR II, and the data are reported in reciprocal centimeters (cm À 1 ) in the range 4000-600 cm À 1 . Optical rotations were measured on a polarimeter at 589 nm.

[α] is expressed in deg • cm 3 • g À 1 • dm À 1 , and c is expressed in g/ 100 cm 3 . HRMS were determined on a TOF mass analyzer coupled with electrospray ionization (ESI) or atmospheric pressure chemical ionization (APCI).

General Experimental Procedures

General procedure for iodination: To a stirred solution of peracetylated glycal in dry MeCN (3 mL per 1 mmol of 2iodoglycal) at 80 °C under argon were added NIS (1.2 eq) and AgNO 3 (0.2 eq) successively and stirred for 2 h. After consumption of starting material (TLC monitoring), the reaction mixture was filtrated on Celite ® , washed with EtOAc and concentrated to give a crude product which was purified by silica gel column chromatography using indicated system.

General procedure for deacetylation: Peracetylated 2-iodoglycal was dissolved in methanol (6 mL per 1 mmol of 2-iodoglycal), then K 2 CO 3 was added (0.1 eq). The resulting mixture was stirred at room temperature for 2 hours. After that time solvent was removed under vacuum. The crude was purified by flash chromatography using indicated system.

General procedure for cyanation with product isolation (C1): 2-Iodoglycal, K 4 Fe(CN) 6 *3H 2 O (0.4 eq), Pd-XPhos-G3 (0.04 eq), XPhos (0.08 eq), CH 3 COOK (0.05 eq) were added to a sealed tube. Then tBuOH (230 μL per 0.1 mmol of glycal iodide) and H 2 O (230 μL per 0.1 mmol of 2-iodoglycal) were added under argon. The resulting mixture was stirred at 75 °C for 18 hours. After completion of the reaction, solvent was removed under vacuum, the crude was purified by flash chromatography using indicated system.

Procedure for condition screening cyanation with NMR yield determination (C2): The reaction was performed according to the procedure C1 starting from 2-iodoglucal (45 mg, 0.165 mmol). However, after quenching reaction, the mixture was filtered through a pad of Celite ® and thoroughly washed several times with methanol. Volatiles were evaporated off then internal standard (DMF) was added (12.8 μL, 0.165 mmol) to the crude. To determine the yield analytical signals were integrated on 1 H NMR spectrum (7.99 ppm -DMF singlet set as reference which was compared with product's 7.29 ppm singlet signal (proton in anomeric position on the glycal double bond)).

  Conditions: A: 2 (1 equiv.), H 2 (4 bar), Pd(OH) 2 /C (20 mol%), HCl 1 M, i-PrOH, r.t., 18-72 h. B: 2 (1 equiv.), NaBH 4 (4.1 equiv.) CoCl 2 .6H 2 O (cat.), THF/H 2 O (2:1), 0 °C to r.t., 2-6 h. C: 2 (1 equiv.), CuI (2 equiv.), DBU (2 equiv.), Cs 2 CO 3 (0.5 equiv.), CH 3 NO 2 /H 2 O (1:10), 100 °C, 90 min. D: 2 (1 equiv.), NaN 3 (1.1 equiv.), CuI (0.2 equiv.), DMF, 100 °C, 18 h. E: 1) 2 (1 equiv.), MeMgBr (6 equiv.), THF, 65 °C, 18 h; 2) HCl 1 M, 65 °C, 30 min.

Table 2 .

 2 Glycal scope.[a]

	2 b 92%	2 c 90%	2 d 100%

Table 3 .

 3 Access to diverse C2-glycoanalogues from 2.[a]

Adv. Synth. Catal. 2020, 362, 1 -7 © 2020 Wiley-VCH Verlag GmbH & Co. KGaA, Weinheim 2

Adv. Synth. Catal. 2020, 362, 1 -7 © 2020 Wiley-VCH Verlag GmbH & Co. KGaA, Weinheim

Acknowledgements

This work has benefited from the facilities and expertise of the Small Molecule Mass Spectrometry platform of ICSN (Centre de Recherche de Gif -http://www.icsn.cnrs-gif.fr). M.M. and A. F. thank the Fondation de la Maison de la Chimie for the financial support.