Thomas Jensen

Vincent Rébiscoul

Alan Schmitt

Building CFA for λ-calculus from Skeletal Semantics

This paper describes a method to define a correct abstract interpretation from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics. We extend it with a notion of program points, in order to differentiate two fragments of the program that are syntactically equivalent but appear at different locations. We introduce a methodology for deriving an abstract interpretation from a Skeletal Semantics that is correct by construction: given a program, abstract states are computed for each program points. We apply our method by defining a Control Flow Analysis for λ-calculus from its Skeletal Semantics.

Introduction

As the complexity of software increases, building static analyses becomes more and more important. Analyzers have improved for years and many companies use them to save time by detecting bugs [START_REF] Calcagno | Moving fast with software verification[END_REF], or prove some properties on their code [START_REF] Cousot | The astrée analyzer[END_REF]. In both cases, the soundness of the analysis is paramount. Methods to develop analyses from a description of a language are useful because they are systematic, even if done by hand. One of the most famous example is Abstract Interpretation [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], which explains how to define an abstract semantics from an operational semantics and how to prove that the abstract semantics is sound using a Galois connection. Other works used abstract interpretation, for example to build an abstract semantics from a big-step semantics [START_REF] Schmidt | Natural-semantics-based abstract interpretation[END_REF].

In order to mechanize the design of sound analyses, one should start from a mechanized semantics. Several tools provide such semantics, such as K [START_REF] Ros | An overview of the k semantic framework[END_REF], a framework to mechanize semantics using rewriting rules. This makes the formal definition of a semantics easier, and allows to mechanically derive objects from the semantics: for example in K, one can automatically derive an interpreter from the mechanization of a language. However, K is not an extensible framework and it is unclear how to derive an analysis from a mechanization in K.

In this paper we describe the first steps towards the generation of analyses from a Skeletal Semantics. Skeletal Semantics [START_REF] Bodin | Skeletal semantics and their interpretations[END_REF] is a recent proposal for machine-representable semantics of programming languages, using a minimalist functional language, Skel. From the Skeletal Semantics of a language, a semantics can be derived by meta-interpretation of Skel, as a bigstep semantics [START_REF] Noizet | Semantics in Skel and Necro[END_REF]. Abstract Interpretation is a powerful framework to build analyses, thus our work focuses on building an abstract interpretation from a Skeletal Semantics. Because both big-step semantics and abstract interpretations stem from the same syntactic object, the proof of soundness of the abstract interpretation is in large part independent from the language considered. Proving the correctness of the abstract interpretation and the big-step semantics given a particular Skeletal Semantics is therefore dependent on small lemmas only.

Our goal is to provide a methodology to easily define several semantics for a language that can be related to one another. Skeletal Semantics [START_REF] Bodin | Skeletal semantics and their interpretations[END_REF] is a recent proposal for machinerepresentable semantics of programming languages The Skeletal Semantics of a language is a partial description of the language. Several meanings, called interpretations, can be given to this description like a big-step semantics [START_REF] Noizet | Semantics in Skel and Necro[END_REF]. However, because the description is partial, some parts are left unspecified, and to fully define a semantics, one needs to provide specifications to the unspecified parts. There are two benefits to this approach. First, the different interpretations are language independent: an interpretation can be used with any Skeletal Semantics. Second, two interpretations can be related to one another: for example, in this paper we present an abstract interpretation that is a correct approximation of the big-step interpretation.

One benefit to this approach is that the interpretations of Skel can be used for any language with a Skeletal Semantics, the definition of a semantics is done by only specifying the language dependent unspecified parts. Because it is often easy to define relations between interpretations, the different semantics of one language can also be related to by proving small lemmas on the specifications that depend on the interpretations. For example, we present a method in this paper to define an abstract interpretation from a Skeletal Semantics that is a sound approximation of the big-step semantics, provided that some lemmas about the Contributions We propose a new interpretation of Skel that includes program points in a systematic way. We define an abstract interpretation for Skel which is correct: the set of all the executions of the big-step semantics is safely over-approximated. We provide a modular methodology to prove correctness at the skeletal meta-level. We give an example of how to define a CFA analysis for λ-calculus using the abstract interpretation of Skel. This work has been implemented in a small OCaml program which takes as inputs a Skeletal Semantics and the definitions of unspecified types and terms, and returns an abstract interpreter.

In Section 2, we introduce the syntax of Skeletal Semantics. In Section 3, we present a big-step semantics (or concrete interpretation) of Skel. In Section 4, we show how to modify the big-step semantics to use program points of a given program. In Section 5, we present an abstract interpretation of Skel, used to define abstract interpretation for any language with a Skeletal Semantics, with a theorem of soundness between the Skel abstract interpretation and big-step semantics. Finally, in Section 6, we use the abstract interpretation to define a CFA analysis for the λ-calculus

Skeletal Semantics and their Syntax

Skeletal Semantics is a recent approach to mechanize semantics for programming languages [START_REF] Bodin | Skeletal semantics and their interpretations[END_REF]. It uses a minimalist, functional, and strongly typed language called Skel [START_REF] Noizet | Semantics in Skel and Necro[END_REF]. The Necro library [START_REF] Noizet | Necro Library[END_REF] is a tool to manipulate Skeletal Semantics. Given Skel code, it can generate Ocaml code, Coq code, step by step debuggers, and more.

The mechanization of a semantics of a language using Skeletal Semantics is done by metainterpretation of the Skel language, therefore interpretations must be provided. In this paper, we will present two interpretations: a big-step semantics and an abstract interpretation.

A Skeletal Semantics is a syntactic object, written in Skel, describing a language. We present the Skeletal Semantics of the call-by-value λ-calculus with environments. We start by defining useful types for our language: It starts with two definitions of unspecified types, and two definitions of specified types. The types refer, in that order, to identifiers, environments, closures, and λ-terms. Having unspecified types is a unique trait of Skel. Keeping some types unspecified is useful because their instantiation can depend on the interpretation of Skel. Specified types are algebraic data types (ADT). The clos type contains only one constructor which parameter is a triplet with an identifier (representing a variable), a λ-term, and an environment, which is a usual definition for a closure. The type lterm is the definition of λ-terms: it can be a λ-abstraction, a variable or an application.

Moreover, a Skeletal Semantics contains terms:

val extEnv : (env, ident, clos) → env val getEnv : (ident, env) → clos

The term getEnv(x, e) is a lookup function: it returns the closure associated to x in e. The term extEnv(e, x, v) returns a new environment equals to e but with the new binding where x maps to v. Terms must be explicitly typed. Moreover, both terms are unspecified : like types, terms do not need to be completely defined in the Skeletal Semantics. In fact, as env is unspecified, functions to access or extend it must be unspecified.

A Skeletal Semantics also contains specified terms: This specified term is the function detailing how a lterm should be computed given an environment. For example, the eval function starts with a branching with three branches, and each branch is guarded by a let-binding doing pattern-matching: this particular branching acts as a case analysis. Indeed, a branching is used to cover several cases: here, there is one case per constructor in the lterm type. The first branch evaluates a λ-abstraction by returning a closure, the second branch evaluates a variable by using the getEnv function. The final branch evaluates an application: first t1 is evaluated, which gives a closure Clos(x, t, s ′ ) representing the function with parameter x and body t, and where environment s' gives meaning to free variables in t. Then t2 is evaluated to another closure w, and s' is extended such that x maps to w, giving a new environment s". Finally, the body of the function t is evaluated with the new environment s". This should not be too surprising for people familiar with the semantics of λ-calculus with environments. Formally, the syntax of Skel is given in Figure 1: it is similar to λ-calculus where the syntax ensures that programs are in A-Normal Form [START_REF] Sabry | Reasoning about programs in continuation-passing style[END_REF]. A specified term is either a variable, a constructor applied to a term, a tuple, or a function. Intuitively, a term is a construct that is fully computed. A skeleton is either an application, a let-binding, a branching, or a term. Intuitively, a skeleton is a computation. Branching is the most exotic construct of the language, it will be explained in more depth later on. Skel uses patterns, notably to perform patternmatching with let-bindings. A term declaration introduces a top-level term. It can either be unspecified, in which case only its name and type are given, or specified, in which case the specification is a term. A type declaration introduces a type that may be unspecified, or it can be the declaration of an algebraic datatype.

A Skeletal Semantics is a set of type definitions and term definitions, that can be specified or unspecified. In the following, for any constructor C of a specified algebraic data type τ , we write C : (τ i , τ ) to state that C belongs to type τ and expects an argument of type τ i .

Big-step Semantics of Skel

To give meaning to a Skeletal Semantics, we provide interpretations of Skel. In this section, we give the big-step semantics of Skel.

The predicate na(τ ) is true when τ is not an arrow type. The arity of a function f , arity(f ), is n if f has type τ 1 → . . . → τ n → τ , where na(τ ). Let S be an arbitrary Skeletal Semantics. We write Funs(S) for the set of pairs (Γ, λp : τ 1 → S 0 ) such that λp : τ 1 → S 0 appears in Skeletal Semantics S. The typing environment Γ gives types to the free variables of λp : τ 1 → S 0 . Typing rules are given in the Appendix B and Funs(•) is formally defined in the Appendix C.

From Types to Concrete Values

We call the interpretation of types the function V(τ ), that given a type τ returns the set of values of that type. These sets are defined with the relation ⊢ • ∈ V(•) in Figure 2. These rules are language independent and are completed with language-dependent rules upon instantiation. The Tuple and ADT rules build tuples and values of ADTs. The Clos rule builds a closure, which is a a triplet (p, S, E). p is the pattern that contains the parameters of the function, S is the body of the function and E an environment for the free variables in S. Note that this environment must be compatible with the typing of the free variables of the function (Rule IEnv). The Def rule builds named closures for application of unspecified and specified terms with arrow type. The closure contains only the name and the arity of the function.

∀1 ≤ i ≤ n ⊢ v i ∈ V(τ i ) ⊢ (v 1 , . . . , v n ) ∈ V(τ 1 × • • • × τ n ) Tuple ⊢ v ∈ V(τ ) C : (τ, τ a ) ⊢ C v ∈ V(τ a ) ADT (Γ, λp : τ 1 → S) ∈ Funs(S) Γ ⊢ E Γ + p ← τ 1 ⊢ S : τ 2 ⊢ (p, S, E) ∈ V(τ 1 → τ 2 ) Clos val f : τ 1 → • • • → τ n → τ [= t] ∈ S na(τ ) ⊢ (f, arity(f )) ∈ V(τ 1 → • • • → τ n → τ ) Def dom Γ = dom E ∀x ∈ dom E, Γ ⊢ E(x) : Γ(x) Γ ⊢ E IEnv
An instantiation of a Skeletal Semantics must define the values belonging to unspecified types. We now show how this is done by example. In the case of λ-calculus, the unspecified types are ident and env, thus we provide rules to build these values.

id ∈ V = { x, y, z... } ⊢ id ∈ V(ident) Ident ⊢ [ ] ∈ V(env) Env-Empty ⊢ id ∈ V(ident) ⊢ c ∈ V(clos) ⊢ e ∈ V(env) ⊢ (id, c) :: e ∈ V(env) Env-Cons
Identifiers are variables from a countable set of variables V, and an environment is an association list: it can be empty or built from a new binding and another environment.

Interpretation of Unspecified Terms

If X is a set, P f (X) is the set of finite parts of X. Now that values are defined, there remains to give definitions to unspecified terms. Take an unspecified term val t :

τ 1 → • • • → τ n → τ such that na(τ ), then an instantiation of t, written t , is a function such that: t ∈ (V(τ 1 ) × • • • × V(τ n )) → P f (V(τ )).
In particular, if val t : τ and na(τ ), then t ⊆ V(τ ). Allowing the specification of a term to be a function returning a set is useful to model non-determinism.

For our λ-calculus, the specifications of unspecified terms are: The interpretation getEnv (x,e) is defined with three equations: the first equation returns the closure when the correct binding is at the head of the environment, the second equation is a recursive call when the first binding is not the correct one, and in last equation, getEnv returns the empty set because the environment is empty. extEnv (e, x, c) returns a similar environment to e, but with a new binding where x is associated to c.

Big-step Semantics

We now define the big-step semantics of Skel. E, S ⇓ v is a relation from a skeletal environment E, mapping skeletal variables to values, and a skeleton S to a value v. The relation is defined in Figure 3a.

There are four rules to evaluate variables, depending on how the variable was defined and its type. If the variable was defined in a 'let' expression, the environment E maps the variable to its value (Rule Var). Otherwise, assuming the Skeletal Semantics is well typed, the variable must be the name of a specified or unspecified term. If this term has an arrow type, we simply return a named closure, whether the variable is specified or not. A named closure is a pair of the name and arity of the function (Rule TermClos). If the variable is declared in the Skeletal Semantics, then it is bound to a closed term t, which is evaluated in the empty environment because it only depends on term declarations of the Skeletal Semantics (Rule TermSpec). If the variable is unspecified, a value of the provided instantiation is returned (Rule TermUnspec). Rules Const and Tuple are usual. Rule Clos returns a skeletal closure. One may observe a similarity between this meta-rule and the corresponding object rule in the λ-calculus; this is because Skel is a meta-language that is an extension of the λ-calculus, but the meta-language and the object language should not be confused.

We now turn to the evaluation of skeletons. Rule LetIn is usual. Rule Branch evaluates a branching by non-deterministically returning the result of the evaluation of a branch. To evaluate an application, we define another relation, defined in Figure 3b with four rules. Rule Base returns the result when all arguments have been processed. Rule Clos is the application of a closure. Rules Spec and Unspec are the application of a named closure to a list of arguments. The first evaluates the corresponding definition while the second one uses the user-provided instantiation. Non-specified functions may be non-deterministic since their instantiation may return a set. Note that we only consider full application of named functions: all arguments must be provided. Extending this semantics to partial application is easy, although verbose, but it is not necessary to describe our contributions. Finally, the pattern matching rules for environment extension are given in Figure 4.

E(x) = v E, x ⇓ v Var val f : τ 1 → • • • → τ n → τ [= t] na(τ ) n ≥ 1 E, f ⇓ (f, n) TermClos val x : τ = t ∈ S na(τ ) ∅, t ⇓ v E, x ⇓ v TermSpec val x : τ ∈ S na(τ ) v ∈ x E, x ⇓ v TermUnspec E, t ⇓ v E, (C t) ⇓ C v Const E, t 1 ⇓ v 1 . . . E, t n ⇓ v n E, (t 1 , . . . , t n ) ⇓ (v 1 , . . . , v n ) Tuple E, (λp : τ → S) ⇓ (p, S, E) Clos E, S 1 ⇓ v ⊢ E + p ← v ⇝ E ′ E ′ , S 2 ⇓ w E, let p = S 1 in S 2 ⇓ w LetIn E, S i ⇓ v E, (S 1 , .., S n ) ⇓ v Branch ∀i ∈ [0..n]. E, t i ⇓ v i v 0 v 1 . . . v n ⇓ app w E, (t 0 t 1 . . . t n ) ⇓ w
v ⇓ app v Base ⊢ E + p ← v 1 ⇝ E ′ E ′ , S ⇓ v v v 2 . . . v n ⇓ app w (p, S, E) v 1 . . . v n ⇓ app w Clos val f : τ 1 → • • • → τ n → τ = t ∈ S na(τ ) ∅, t ⇓ v v v 1 . . . v n ⇓ app w (f, n) v 1 . . . v n ⇓ app w Spec val f : τ 1 → • • • → τ n → τ ∈ S na(τ ) w ∈ f (v 1 , . . . , v n ) (f, n) v 1 . . . v n ⇓ app w
⊢ E + ← v ⇝ E asn-wildcard ⊢ E + x ← v ⇝ (x, v) :: E asn-var ⊢ E + p ← v ⇝ E ′ ⊢ E + C p ← C v ⇝ E ′ asn-constr ⊢ E + p 1 ← v 1 ⇝ E 2 . . . ⊢ E n + p n ← v n ⇝ E ′ ⊢ E + (p 1 , . . . , p n ) ← (v 1 , . . . , v n ) ⇝ E ′ asn-tuple

Program Points and New Values

We present our first contribution, which is a method to use program points in the big-step semantics of a Skeletal Semantics. This methodology is reused later for the abstract interpretation of Skel. Let S be a Skeletal Semantics. It usually contains one or more specified algebraic data types that define the syntax of the language, i.e., programs. We call these types program types. In the case of λ-calculus, lterm is the only program type. Let τ a program type in S and prg ∈ V(τ ) a program, we can refer to sub-terms of prg using program points. A program point is a path from the root of prg to one of its sub-term. Given a program point pp, prg@ pp is the sub-term of prg obtained by following path pp. A program point pp is an element of ppt = N * , the set program points. ϵ is the empty path and i • pp is a path with first element i, and pp is the rest of the path. The @ operator is formally defined as:

v@ϵ = v C(v 0 , . . . , v n-1 )@i • pp = v i @ pp when 0 ≤ i ≤ n -1
To give an example, for λ-calculus, let prg = Lam(x, V ar x). Then, prg@0 = x and prg@1 = V ar x.

Our approach is to replace values of program types with program points. Each program point refers to a sub-term of the main program: prg, which is now a parameter of the interpretation. Let T be the set of program types from S and prg a program. Therefore, all values of τ ∈ T are program points and represent sub-terms of prg . In particular, because prg is a program, its type should be in T .

For each type τ , a set of values is built using previously defined rules 2 except for program types that are defined by the equation:

τ ∈ T =⇒ V ppt prg (τ ) = { pp ∈ ppt | prg@ pp ∈ V(τ ) }
The set V ppt prg (τ ) is the set of program points that refer to sub-terms of prg of type τ . This is an important restriction because if τ ∈ T , then a value v ∈ V ppt prg (τ ) is a program point and therefore necessarily represent a fragment of prg and not an arbitrary program.

T is a set because some languages may have many types for different parts of programs: an imperative language would need at least one type for statements and one type for expressions. Let us give an example with the λ-calculus. We take our program to be prg = App(Lam(x, V ar x), V ar y) and T = { lterm }. The interpretation of the λ-terms is defined in the next equation. The program points are underlined to differentiate them from natural numbers.

V ppt prg (lterm) = { ϵ, 0, 1, 01 } For example, we have prg@1 = V ar y

The interpretation of unspecified types does not change and other types are built using previous rules in Figure 2. However, we assume new specifications of unspecified terms. Indeed, some unspecified terms may depend on types in T , therefore, for all unspecified terms x in S, we suppose that new specifications are provided: x ppt .

Pattern Matching with Program Points

The interpretation of skeletons with program points does not fundamentally change: only the pattern matching is modified and uses an unfolding mechanism. Unfolding matches a program point with a constructor pattern and is described by the following rule.

NC(τ 1 → τ 2 ) = (f, n) val f : τ 1 → τ 2 [= t] ∈ S arity(f ) = n C(τ 1 → τ 2 ) = (p, S, E ♯ ) ∃(Γ, λp : τ 1 → S) ∈ Funs(S), Γ ⊢ E ♯ ∧ Γ + p ← τ 1 ⊢ S : τ 2
prg@ pp = C (v ′ 0 , . . . , v ′ n-1 ) C : (τ 0 × • • • × τ n-1 , τ ) v j = if τ j ∈ T then pp •j else v ′ j T , prg ⊢ E + p ← (v 0 , . . . , v n-1 ) ⇝ E ′ T , prg ⊢ E + C p ← pp ⇝ E ′ asn-unfold
When a program point pp is matched with a constructor pattern C p, prg@ pp is expected to have the form C(v ′ 0 , . . . , v ′ n-1 ). Then, for 0

≤ j ≤ n -1, v j is pp •j if v ′ j has a program type τ j ∈ T , or v ′ j otherwise.
Then the pattern p is matched with (v 1 , . . . , v n ). The unfolding rule exhibits the constructor and its parameters at program point pp, then continues the pattern matching recursively.

We give an example for λ-calculus, let prg = App(Lam(x, V ar x), V ar y). To compute T , prg ⊢ E + Lam(p) ← 0 ⇝ E ′ where p is a pattern, by applying the asn-unfold rule, it comes that: T , prg ⊢ E + p ← (x, 01) ⇝ E ′ Indeed, prg@0 = Lam(x, V ar x) and V ar x has program point 01, therefore p is matched with (x, 01)

The big-step semantics of skeletons and the big-step semantics of skeletons with program points are closely related. We formalize this connection through a theorem presented in Appendix D.

Abstract Interpretation

We define an abstract interpretation of Skel that is sound with respect to the big-step semantics of Section 4. The abstract interpretation is used in the next section to define a Control Flow Analysis for λ-calculus.

We define the abstract values, comparison functions and upper bounds in Section 5.1. We define the state of the abstract interpretation in Section 5.2. We present the interpretation rules of skeletons for an abstract interpretation in Section 5.3, We present how the abstract values are linked to the concrete values by defining concretization functions in Section 5.4. Finally, we formulate a theorem of soundness in Section 5.5. In the following sections, S denotes an arbitrary Skeletal Semantics.

Definition of Abstract Values

The abstract values are defined similarly to the concrete ones. In Figure 5 we define the set of abstract named closures and the set of abstract closures. Abstract named closures are pairs of a name of a function defined in the skeletal semantics and its arity. Abstract closures are a triplet with a pattern, a skeleton and an abstract environment. The abstract environment is defined later in the this section. The rules to define abstract values are presented on Figure 6. The Bottom and Top rules define a least and a greatest element for each type. The Tuple rule define the abstract tuples, that are a set of tuples of abstract values. Because one of our target is CFA analysis for λcalculus, having a set is necessary not to loose too much precision during the analysis. On line 24 of the Skeletal Semantics of the λ-calculus A, eval s t1 returns a closure, Clos(x, t, s) which is essentially a triplet. The relation between identifier, term and environment must be preserved. Values of algebraic types, defined by the rule ADT, are constructors applied to abstract values. Abstract functions, defined by the rule Funs, is the union of a subset of abstract named closures, and a subset of abstract closures. For instance for the λ-calculus, the set {(eval, 2), (s, λl:lterm.S eval , ∅)} belongs to V ♯ (env → lterm → clos), where S eval is the body of the eval specified term. Finally, the rule IEnv defines abstract environments, that are partial functions mapping skeletal variables to abstract values.

⊢ ♯ ⊥ τ ∈ V ♯ (τ ) Bottom ⊢ ♯ ⊤ τ ∈ V ♯ (τ ) Top ∀(v ♯ 1 , . . . , v ♯ n ) ∈ t ♯ ∀1 ≤ i ≤ n, ⊢ ♯ v ♯ i ∈ V ♯ (τ i ) ∧ v ♯ i ̸ = ⊥ τi ⊢ ♯ t ♯ ∈ V ♯ (τ 1 × • • • × τ n ) Tuple ⊢ ♯ v ♯ ∈ V ♯ (τ ) C : (τ, τ a ) v ♯ ̸ = ⊥ τ ⊢ ♯ C v ♯ ∈ V ♯ (τ a ) ADT nc ⊆ NC(τ 1 → τ 2 ) c ⊆ C(τ 1 → τ 2 ) ⊢ ♯ c ∪ nc ∈ V ♯ (τ 1 → τ 2 ) Funs dom Γ = dom E ♯ ∀x ∈ dom E ♯ , Γ ⊢ E ♯ (x) : Γ(x) Γ ⊢ E ♯ IEnv
To compare abstract values, we define partial orders. For every unspecified type τ u , we assume comparison function ⊑ ♯ τu which is an order and with the constraint that ⊤ τu and ⊥ τu are the greatest and smallest elements of V ♯ prg (τ u ) respectively. For every other types, the comparison function is the smallest order that satisfies the following equations:

C v ♯ ⊑ ♯ τa C w ♯ ⇐⇒ v ♯ ⊑ ♯ τ w ♯ with C : (τ, τ a ) t ♯ 1 ⊑ ♯ τ1ו••×τn t ♯ 2 ⇐⇒ ∀(v ♯ 1 , . . . , v ♯ n ) ∈ t ♯ 1 , ∃(w ♯ 1 , . . . , w ♯ n ) ∈ t ♯ 2 , ∀i, 1 ≤ i ≤ n, v ♯ i ⊑ ♯ τi w ♯ i F 1 ⊑ ♯ τ1→τ2 F 2 ⇐⇒ (f, n) ∈ F 1 =⇒ (f, n) ∈ F 2 (p, S, E ♯ 1 ) ∈ F 1 =⇒ ∃(p, S, E ♯ 2 ) ∈ F 2 , E ♯ 1 ⊑ ♯ env E ♯ 2 E ♯ 1 ⊑ ♯ env E ♯ 2 ⇐⇒ Γ ⊢ E ♯ 1 ∧ Γ ⊢ E ♯ 2 ∧ ∀x ∈ dom E ♯ 1 , E ♯ 1 (x) ⊑ ♯ Γ(x) E ♯ 2 (x) v ♯ ⊑ ♯ τ ⊤ τ ⊥ τ ⊑ ♯ τ v ♯
To compare algebraic values, their parameters are compared. Tuples are compared by checking that all tuples of abstract values of the left tuple are smaller than a tuple of abstract values in the right tuple. To compare two functions, all named closures of the left function must be in the right function. Moreover, for all closures in the left function, there must be a closure in the right function with the same pattern and skeleton, but with a bigger abstract environment. Abstract environments are compared using point-wise lifting. For each type, top and bottom are respectively the smallest and greatest elements of the type.

For each type, an upper bound (or join) is defined. For every non-specified type τ u , we assume an upper bound ⊔ ♯ τu . We define an upper bound ⊔ ♯ τ for every other types.

(C v ♯ )⊔ ♯ τa (C w ♯ ) =C (v ♯ ⊔ ♯ τ w ♯ ) with C : (τ, τ a ) (C v ♯ )⊔ ♯ τa (D w ♯ ) =⊤ τa with C : (τ, τ a ) ∧ D : (τ ′ , τ a ) t ♯ 1 ⊔ ♯ τ1ו••×τn t ♯ 2 =t ♯ 1 ∪ t ♯ 2 F 1 ⊔ ♯ τ1→τ2 F 2 =F 1 ∪ F 2 E ♯ 1 ⊔ ♯ env E ♯ 2 = x ∈ dom E ♯ 1 → E ♯ 1 (x)⊔ ♯ E ♯ 2 (x) v ♯ ⊔ ♯ τ ⊤ τ = ⊤ τ ⊔ ♯ τ v ♯ =⊤ τ v ♯ ⊔ ♯ τ ⊥ τ = ⊥ τ ⊔ ♯ τ v ♯ =v ♯
Joining two algebraic values with the same constructor is joining their parameters, and joining algebraic values with different constructors yield top. Joining abstract tuples our abstract functions is set union. Joining abstract environments is done by point-wise lifting. For each type, top is an absorbing element, and bottom is the neutral element.

State of the Abstract Interpretation

The state of the abstract interpretation A is a machine representable state that contains information collected throughout the abstract interpretation. It is dependent on the analysis and the language, and therefore is non-generic and must be specified. To give an example, when defining a CFA in the next section, the abstract state will contain a mapping from program points to sets of λ-abstraction, that can be viewed as the potential results when evaluating a sub-term at some program point of the analyzed program. We require an order on the abstract states. Intuitively, we should only add information in the states throughout the analysis, and therefore at each step of the analysis, the states should only increase. A state contains several components: A • c is the component c of the abstract state A. The notation { A with c = v } denotes a new state equals to A, excepts for the c component which is equal to v.

The Abstract Interpretation of Skel

The abstract interpretation maintains a callstack of specified function. This is used for loop detection and prevent infinite computations: the idea is to inspect the callstack at each call to a specified function to detect identical nested calls. Callstacks are ordered list of frames, formally defined as:

ϵ ∈ callstack A an abstract state valf : τ 1 → • • • → τ n → τ = t ∈ S na(τ ) v i ∈ V ♯ prg (τ i ) π ∈ callstack (f, A, [v 1 , . . . , v n ]) :: π ∈ callstack
The abstract interpretation of skeletons is given on Figure 7a. The abstract interpretation of skeletons is similar to the big-step interpretation: the evaluation of terms is almost unchanged except that evaluating a closure or a tuple returns a singleton. When evaluating a skeleton (branch, let-binding, or application), a state of the abstract interpretation is carried through the computations. In the Branch rule, all branches are evaluated and joined instead of only one branch being evaluated. The pattern matching now returns sets of environments rather than one, and this will be detailed later, but in consequence the LetIn rule may evaluate S 2 in several abstract environments. The App rule evaluates all terms and pass a list of values to the application relation. There are separate rules to handle applications on Figure 7b. Because the abstraction of a function is a set of closures and named closures, the App-Set rule evaluates each one individually. The Base rule returns the remaining value when all arguments have been processed. Because the extension of environments returns a set of abstract environment, the Clos rule is modified accordingly and the body of the function S is evaluated in all abstract environments. The Spec rule evaluates the call to a specified function by doing three things:

• it uses an update in f (•) function which is language dependent and must be specified. It can modify the arguments and the state of the abstract interpretation.

• the call is performed (a frame is added to the callstack at that point).

• an update out f (•) function can modify the state of the interpretation and the returned value.

These update functions are used to maintain invariants and update the state of the abstract interpretation. An example of their use will be presented in the next section. The update functions must respect the following constraints to ensure soundness:

Remark 1. update in f (A, [v ♯ 1 , . . . , v ♯ k ]) = [v ′♯ 1 , . . . , v ′♯ k ], A ′ =⇒ (v ♯ 1 , . . . , v ♯ k ) ⊑ ♯ (v ′♯ 1 , . . . , v ′♯ k ) ∧ A ⊑ ♯ A ′ update out f (A, [v ♯ 1 , . . . , v ♯ k ], v ♯ ) = v ′♯ , A ′ =⇒ v ♯ ⊑ ♯ v ′♯ ∧ A ⊑ ♯ A ′
The extension of environments, or pattern matching, presented on Figure 8 is modified such that it returns a set of abstract environments. This is necessary because our abstraction of tuples is a finite set of tuples of abstract values. In order not to lose too much precision, we return one abstract environment per tuple of abstract values in our abstract tuple. The rules are similar to the big-step semantics, excepts that there are two rules for tuples: the rule asntuple-singleton extends the environment with a tuple of abstract values, the asn-tuple forwards all tuples of abstract values in t ♯ to the asn-tuple-singleton rule.

E ♯ (x) = v ♯ E ♯ , x ⇓ v ♯ Var val f : τ 1 → • • • → τ n → τ [= t] ∈ S na(τ ) E ♯ , f ⇓ { (f, arity(f )) } TermClos val x : τ = t ∈ S ∅, t ⇓ v ♯ na(τ ) E ♯ , x ⇓ v ♯ TermSpec val x : τ ∈ S na(τ ) E ♯ , x ⇓ x ♯ TermUnspec E ♯ , t ⇓ v ♯ E ♯ , C t ⇓ C v ♯ Const E ♯ , t 1 ⇓ v ♯ 1 . . . E ♯ , t n ⇓ v ♯ n E ♯ , (t 1 , . . . , t n ) ⇓ (v ♯ 1 , . . . , v ♯ n ) Tuple π, E ♯ , λp : τ • S ⇓ ♯ (p, S, E ♯ ) Clos π, A, E ♯ , S i ⇓ ♯ v ♯ i , A i π, A, E ♯ , (S 1 . . . S n ) ⇓ ♯ ⊔ ♯ v ♯ i , ⊔ ♯ A i Branch π, A, E ♯ , S 1 ⇓ ♯ v ♯ , A ′ T , prg ⊢ E ♯ + p ← v ♯ ⇝ E ♯ 1 , . . . , E ♯ n π, A ′ , E ♯ i , S 2 ⇓ ♯ w ♯ i , A i π, A, E ♯ , let p = S 1 in S 2 ⇓ ♯ ⊔ ♯ w ♯ i , ⊔ ♯ A i LetIn E ♯ , t i ⇓ v ♯ i π, A, v ♯ 0 v ♯ 1 . . . v ♯ n ⇓ app v ♯ , A ′ π, A, E ♯ , t 0 t 1 . . . t n ⇓ ♯ v ♯ , A ′
v ♯ 0 = n i=1 { w i } π, A, w i v ♯ 1 . . . v ♯ n ⇓ app v ♯ wi , A i π, A, v ♯ 0 v ♯ 1 . . . v ♯ n ⇓ app ⊔ ♯ v ♯ wi , ⊔ ♯ A i App-Set π, A, v ♯ ⇓ app v ♯ , A Base T , prg ⊢ E ♯ + p ← ♯ v ♯ 1 ⇝ E ♯ 1 , . . . , E ♯ m ∀E ♯ i ∈ E ♯ 1 , . . . , E ♯ m π, A, E ♯ i , S ⇓ w ♯ i , A i π, A i , w ♯ i v ♯ 2 . . . v ♯ n ⇓ app u ♯ i , A ′ i π, A, (p, S, E ♯ ) v ♯ 1 . . . v ♯ n ⇓ app ⊔ ♯ u ♯ i , ⊔ ♯ A ′ i Clos val f : τ 1 → • • • → τ n → τ = t ∈ S na(τ ) ∅, t ⇓ v ♯ update in f (A, [v ♯ 1 , . . . , v ♯ n ]) = A ′ , [v ′♯ 1 , . . . , v ′♯ n ] (f, [v ′♯ 1 , . . . , v ′♯ n ]) / ∈ π (f, [v ′♯ 1 , . . . , v ′♯ n ]) :: π, A ′ , v ♯ v ′♯ 1 . . . v ′♯ n ⇓ app w ♯ , A ′′ update out f (A ′′ , [v ′♯ 1 , . . . , v ′♯ n ], w ♯ ) = w ′♯ , A ′′′ π, A, (f, n) v ♯ 1 . . . v ♯ n ⇓ app w ′♯ , A ′′′ Spec val f : τ 1 → • • • → τ n → τ = t ∈ S na(τ ) ∅, t ⇓ v ♯ update in f (A, [v ♯ 1 , . . . , v ♯ n ]) = A ′ , [v ′♯ 1 , . . . , v ′♯ n ] (f, [v ′♯ 1 , . . . , v ′♯ n ]) ∈ π π, A, (f, n) v ♯ 1 . . . v ♯ n ⇓ app ⊥, A ′ Spec-Loop val f : τ 1 → • • • → τ n → τ ∈ S na(τ ) f ♯ (A, v ♯ 1 , . . . , v ♯ n ) = w ♯ , A ′ π, A, (f, n) v ♯ 1 . . . v ♯ n ⇓ app w ♯ , A ′
, prg ⊢ E ♯ + ← ♯ v ⇝ E ♯ asn-wildcard T , prg ⊢ E ♯ + x ← ♯ v ⇝ (x, v ♯ ) :: E ♯ asn-var T , prg ⊢ E ♯ + p ← ♯ v ⇝ ξ T , prg ⊢ E ♯ + C p ← ♯ C v ⇝ ξ asn-constr T , prg ⊢ E ♯ + p 1 ← ♯ v 1 ⇝ ξ 1 . . . T , prg ⊢ ξ n-1 + p n ← ♯ v n ⇝ ξ n T , prg ⊢ E ♯ + (p 1 , . . . , p n ) ← ♯ (v 1 , . . . , v n ) ⇝ ξ n asn-tuple-singleton (v 1 , . . . , v n ) ∈ t T , prg ⊢ E ♯ + (p 1 , . . . , p n ) ← ♯ (v 1 , . . . , v n ) ⇝ ξ v1,...,vn T , prg ⊢ E ♯ + (p 1 , . . . , p n ) ← ♯ t ⇝ (v1,...,vn)∈t ξ (v1,...,vn) asn-tuple prg@ pp = C (v ′ 1 , . . . , v ′ n ) C : (τ 1 × • • • × τ n , τ ) v j = if τ j ∈ T then pp •j else v ′ j T , prg ⊢ E ♯ + p ← ♯ { (v 1 , . . . , v n ) } ⇝ ξ T , prg ⊢ E ♯ + C p ← ♯ pp ⇝ ξ asn-unfold

Concretization Function

To define concretization functions for abstract values, we assume monotonic concretization functions for abstract values of non-specified types. Concretization functions are defined for every specified types, and take the state of the abstract interpretation as a parameter:

γ τ (A, •) : V ♯ prg (τ ) → P f (V ppt prg (τ )).
We also define a function of concretization γ env which maps abstract skeletal environments to concrete skeletal environments.

γ τa (A, C v ♯ ) = C v | C : (τ, τ a ), v ∈ γ τ (A, v ♯ ) γ τ1ו••×τn (A, t ♯ ) = (v ♯ 1 ,...,v ♯ n )∈t ♯ γ τ1 (A, v ♯ 1 ) × • • • × γ τn (A, v ♯ n ) γ τ1→τ2 (A, F ) = { (f, n) | (f, n) ∈ F } ∪ (p, S, E) (p, S, E ♯ ) ∈ F ∧ E ∈ γ env (A, E ♯ ) γ env (A, E ♯ ) = E Γ ⊢ E ∧ Γ ⊢ E ♯ ∧ Γ(x) = τ dom E = dom E ♯ , E(x) ∈ γ τ (A, E ♯ (x)) γ(A, ⊥ τ ) =∅ γ(A, ⊤ τ ) =V ♯ (τ ) Lemma 1.
If for all unspecified types τ u , γ τu is monotonic on both arguments, then for all τ , γ τ is also monotonic on both arguments.

Correctness of the Abstract Interpretation

Definition 1. Let f be an unspecified term of type τ 1 → • • • → τ n → τ where na(τ ). We say that f ♯ is a sound approximation of f ppt iff ∀v i ∈ V ppt prg (τ i ), ∀v ♯ i ∈ V ♯ prg (τ i ), and for all abstract state A, if

v i ∈ γ τi (A, v ♯ i ) f ♯ (A, v ♯ 1 , . . . , v ♯ n ) = A ′ , w ♯ =⇒ f ppt (v 1 , . . . , v n ) ⊆ γ τ (A ′ , w ♯ )
We state the following theorem of correction that states that the abstract interpretation computes a sound approximation of the big-step interpretation.

Theorem 1. Suppose E, S ⇓ v and ϵ, A 0 , E ♯ , S ⇓ ♯ v ♯ , A and Γ ⊢ E and Γ ⊢ E ♯ and Γ ⊢ S : τ and E ∈ γ(A, E ♯ ). Suppose ∀(val x : τ ) ∈ S, x ♯ is a sound approximation of x ppt . Then, v ∈ γ τ (A, v ♯ ).
Therefore, to prove the soundness of the analysis, it is sufficient to prove that the abstract specifications of terms are sound approximation of the concrete specifications of terms. environment of λ-calculus. A 0 is the initial state of the abstract interpretation with empty mappings A 0 • ρ and A 0 • C. The result of the derivation is a value v ♯ , but most importantly a new state of the interpretation A, that contains mappings A • ρ and A • C that are the results of the CFA: A • ρ gives an abstraction of what closures the variables in prg can be bound to, and A • C gives an abstraction of the closures that can appear at a given program point.

Implementation

This work resulted in an implementation of an Abstract Interpreter Generator [START_REF] Rébiscoul | Abstract Interpreter Generator[END_REF]: given a skeletal semantics, a specification of unspecified types and terms, it generates an abstract interpreter. We have used it to try our CFA analysis defined in previous sections, and we experimentally compared its output to another CFA program and we found no differences on the examples we tested. So far, our CFA has not been proven incorrect but it remains to do a formal proof or correction.

Moreover, the Abstract Interpreter Generator has been used to generate an abstract interpreter for a small imperative language, with basic integer arithmetic, conditional branchings and loops. For instance, one can do a basic interval analysis. However, we did not do relational analyses.

Conclusion

We presented our work to generate a CFA analysis for λ-calculus from a skeletal semantics. We presented what are Skeletal Semantics and how they can be interpreted to define a semantics. The strength of this approach is that one only needs to define the unspecified types and terms to mechanize a big-step semantics for a language that has a Skeletal Semantics. An example of how the big-step semantics of λ-calculus could be mechanized using Skeletal Semantics was given using the big-step semantics of Skel. Then we presented our first contribution which is a big-step semantics of Skel with program points. Our second contribution which is an abstract interpretation of Skel, and we stated a theorem of correction. The proof is a work in progress. Our final contribution is a CFA analysis built using the abstract interpretation of Skel for λcalculus. We implemented an abstract interpreter generator that produces an analyzer from a Skeletal Semantics. We used this program to generate a CFA analyzer for λ-calculus. Our analyzer was experimentally tested and gives similar results to other 0-CFA analyzers.

However, when mechanizing a semantics using an intermediate language like Skel, we expect to lose precision compared to a language specific semantics. Moreover, there are several possible definitions of a Skeletal Semantics for given a language, the abstract interpretation precision may depend on the definition of the Skeletal Semantics. It is a language-independent approach to generates an abstract interpretation for languages with a Skeletal Semantics.

The proof of correction between the big-step semantics and the abstract interpretation must be mechanized. Moreover, our CFA analysis must be compared to other CFA analyses, in particular 0-CFA analysis and verify if we are systematically at least as precise as 0-CFA. Finally, there are not proofs of termination of the abstract interpretation, and this should be addressed.

  ident, lterm, env) type lterm = | Lam (ident, lterm) | Var ident | App (lterm, lterm)

  t1, t2) = l in let Clos (x, t, s') = eval s t1 in let w = eval s t2 in let s'' = extEnv (s', x, w) in eval s'' t end

Figure 1 :

 1 Figure 1: The Syntax of Skeletal Semantics

Figure 2 :

 2 Figure 2: Rules to Build Values

  getEnv (x, (x, c) :: e) = { c } getEnv (x, (y, c) :: e) = getEnv (x, e) x ̸ = y getEnv (x, [ ]) = { } extEnv (e, x, c) = (x, c) :: e

  App(a) Rules for the Big-step Semantics of Skeletons and Terms

  Unspec(b) Rules for Application for the Big-step Semantics

Figure 3 :

 3 Figure 3: Interpretation rules of the Big-step Semantics

Figure 4 :

 4 Figure 4: Rule of Extension of Environment through Pattern Matching

Figure 5 :

 5 Figure 5: Sets of Abstract Named Closures and Closures

Figure 6 :

 6 Figure 6: Rules to Build Abstract Values

App

  (a) Rules for the Abstract Interpretation of Skeletons and Terms

UnspecFigure 7 :

 7 Figure 7: Abstract Interpretation of Skel

Figure 8 :

 8 Figure 8: Extension of Environment through Pattern Matching for Abstract Interpretation

  or let App (t1, t2) = l in let Clos (x, t, s') = eval s t1 in let w = eval s t2 in let s'' = extEnv (s', x, w) in eval s'' t end B Typing Rules of Skeletons and TermsΓ(x) = τ Γ ⊢ x : τ Var val x : τ [= t] ∈ S Γ ⊢ x : τ

Toward a Control Flow Analysis for λ-calculusIn this section we show how the abstract interpretation of Skel can be used to define a Control Flow Analysis (CFA) from the Skeletal Semantics of λ-calculus. A Control Flow Analysis computes an approximation of the Control Flow for higher-order languages. We aim at defining an analysis similar to 0-CFA for λ-calculus. Let t be a λ-term, the result of a 0-CFA for term t is two maps. The first one maps variables of t to an approximation of the values the variable can be bound to. The second one maps sub-terms of t to an approximation of the results of the evaluation of the sub-term.In this section, we call prg the λ-term to be analyzed.

TermDef Γ ⊢ t : τ C : (τ, τ ′ ) Γ ⊢ C t : τ ′ Const ∀i, Γ ⊢ t i : τ i Γ ⊢ (t 1 , . . . , t n ) : (τ 1 , . . . , τ n ) Tuple Γ + p ← τ ⊢ S : τ ′ Γ ⊢ (λp : τ → S) : τ → τ ′ Fun Γ ⊢ S 1 : τ . . . Γ ⊢ S n : τ Γ ⊢ (S 1 . . . S n ) : τ Branch Γ ⊢ S : τ Γ + p ← τ ⊢ S ′ : τ ′

The State of the Abstract Interpretation

For our analysis, the state of the abstract interpretation contains two maps that we call C and ρ:

The C function maps a program point to an approximation of the result of evaluation of the sub-term of prg at the program point. For a program point pp, C(pp) is a set of pairs (x, t), that are really λ-abstractions λx.t. ρ is a function from program points to some abstraction of an environment of λ-calculus. In classic 0-CFA, there is only one global environment, whereas in our analysis, there is one environment per program point. Practically, it means that to evaluate term t, a subterm of the main program prg at program point pp, we use the abstract environment A • ρ(pp).

Specification of the Unspecified Types and Unspecified Terms

As for the big-step semantics with program points, the λ-terms are program types: T = { lterm }.

We give the specifications of the unspecified types.

) is a set of variables. An abstract environment pp e ∈ V ♯ prg (env) is a program point and refers to A • ρ(pp e ) which maps variables to a set of pairs representing λ-abstractions. The definitions of the unspecified terms are:

) contains pairs of the form (y, pp •1) representing λ-abstractions, therefore prg@ pp = Lam(y, t). t has a program point that ends with 1 because it is the second element of the Lam constructor. getEnv type constraint the result to be in V ♯ prg (clos), so we need to attach an environment to our pairs (y, pp •1). Because (y, pp •1) denotes a λ-abstraction defined at program point pp, the associated environment is pp.

extEnv ♯ (A, pp e , x, c) does two things: it modifies the state of the interpretation, and returns a virtual program point. Indeed, extEnv returns a new environment, therefore a program point, but what program point should be returned? We do not know until we evaluate a new lterm with this environment. Therefore, we create virtual program point that will be linked to a real program point later. The extEnv ♯ modifies the abstract state such that ρ(pp v ) contains ρ(pp e ) plus the following constraint: ρ(pp v )(x) = ρ(pp e (x)) ∪ c.

There remains to define our update functions:

The first update function is used before performing the call eval pp e pp t , and the second update function is used after the call was done. pp e has type env and therefore is a program point which refers to A • ρ(pp e ). pp t has type lterm, and therefore is also a program point denoting the sub-term of prg at pp t . Because we want to compute the sub-term at program point pp t , we should use the abstract environment A • ρ(pp t ). Therefore, the abstract state needs to be modified such that A • ρ(pp e ) is included into A • ρ(pp t ), and this is what the first update function does.

The second update function is called after the call is performed. The only thing does is to record the result into the map A • C.

A derivation gives a CFA:

The derivation is implicitly parameterized by the λ-term prg. In the initial environment, l is mapped to the program point ϵ, the root of the λ-term prg. e is mapped to an empty

The set of λ-abstractions in the Skeletal Semantics S is:

D Correction of Big-Step Interpretation with Program Points

Definition 2. To relate element with or without program points, we define the following function γ, such that ∀τ, γ τ ∈ V ppt prg (τ ) → V(τ ). The function γ is parameterized by the global value of type τ ∈ T and satisfies the following constraints.

• γ τ (pp) = prg@ pp and τ ∈ T

Theorem 2. Let γ env (E ′ ) = E, and suppose for all unspecified functions f , γ unspec ( f ppt ) = f , then:

E, S ⇓ v =⇒ ∃v ′ , E ′ , S ⇓ P P v ′ and γ τ (v ′ ) = v


J Legendre
email: julien.legendre@insa-lyon.fr

P.-O Chapuis

Overcoming Non-Radiative Losses with AlGaAs PIN Junctions for Near-Field Thermophotonic Energy Harvesting Overcoming Non-Radiative Losses with AlGaAs PIN Junctions for Near-Field Thermophotonic Energy Harvesting

In a thermophotonic device used in an energy-harvesting configuration, a hot light-emitting diode (LED) is coupled to a photovoltaic (PV) cell by means of electroluminescent radiation in order to produce electrical power. Using fluctuational electrodynamics and the drift-diffusion equations, we optimise a device made of an AlGaAs PIN LED and a GaAs PIN PV cell with matched bandgaps. We find that the LED can work as an efficient heat pump only in the near field, where radiative heat transfer is increased by wave tunnelling. A key reason is that non-radiative recombination rates are reduced compared to radiative ones in this regime. At 10 nm gap distance and for 100 cm.s -1 effective surface recombination velocity, the power output can reach 2.2 W.cm -2 for a 600 K LED, which highlights the potential for low-grade energy harvesting.

Thermophotovoltaics (TPV) is a kind of solid-state heat engine (along with thermoelectrics 1 and thermionics 2 for instance) where a hot emitter radiates towards a photovoltaic (PV) cell, which then converts radiation into electricity. While TPV performs well at high temperature 3 , its capabilities drop as the hot source temperature goes below 1000 K 4 . To alleviate this constraint, near-field enhancements for TPV (NF-TPV) have been extensively studied [5][6][7] (see the review by Song et al. 8 ), and should allow to obtain good performance down to 700 or 800 K 9 . The decrease of the gap distance between the emitter and the PV cell opens indeed new channels for the transport of photons between the two bodies, evanescent waves being now able to participate to the heat transfer 10 .

Another way to increase the power produced by the device is to replace the passive emitter by a light-emitting diode (LED), which is physically similar to a PV cell but used in an opposite fashion (i.e., it emits light instead of producing electricity). In an LED, the electricity consumption allows to enhance the photon emission above the bandgap: this is electroluminescence. When the energy conversion is efficient enough, the LED wall-plug efficiency (WPE), defined as the ratio between the electroluminescent (EL) radiation exchanged and the electrical power fed to the device, can actually exceed unity [11][12][13] . Thermodynamically, this can happen thanks to the low entropy flux associated with EL radiation compared to thermal radiation. The LED works then as a heat pump between its phonon bath (the cold body), and the EL-enhanced electromagnetic field (the hot body) [14][15][16] , the WPE corresponding to the classical coefficient of performance (COP). This is the electroluminescent cooling (ELC) regime.

If the conversion efficiency of the PV cell, which can be seen as a heat engine between the EL radiation field and its phonon bath, is high enough, it is then beneficial to take some electrical power from the PV cell back to the LED to enhance the above-bandgap radiation between the two bodies. The below-bandgap radiation remains unchanged, which is essential to keep the PV cell efficiency high. The combination of an LED and a PV cell in such device, as shown in Fig. (1), is called thermophotonics (TPX) 17 . It can be used both as a heat engine and a heat pump/refrigerator. NF effects allowing to reach ELC more easily, it has been combined with the EL enhancement into a NF-TPX device [18][19][20] . Compared to TPV and NF-TPV, it can be competitive at much lower hot source temperature, down to 450-500 K, and could therefore have applications for low-grade waste heat recovery, as shown in Sec. I of the supplementary material.

In this work, we simulate the performance of a NF-TPX device composed of an AlGaAs PIN LED and a GaAs PIN PV cell (see Fig. (1)). Both the LED and the PV cell are homojunctions.While using heterostructures opens new degrees of freedom for device design, it also comes with its own issues (both in terms of fabrication and physical analysis) and we thus restrict our study to homostructures in the present work. GaAs has been chosen for the PV cell as GaAs-based structures can reach high conversion efficiency, while using Al-GaAs for the LED allows to keep the bandgap of both components matched when at different temperatures, maximising the performance 18 . We place perfect mirror at the back of each component, allowing to improve radiative transfer through cavity effect and preventing radiative losses at the back surface. The impact of mirrors non-ideality on performance was studied by Zhao et al. 18 .

Modelling such devices requires to couple the resolution of the near-field photon transfer between the two components (LED and PV cell) and of the charge transport in both of them. This resolution is performed in 1D. The near-field radiative heat transfer is obtained using the fluctuational electrodynamics framework 21,[START_REF] Rytov | Principles of Statistical Radiophysics[END_REF] . The spectral photon flux density between any layers i and j is then expressed as:

γ i j (ω) = ∆n 0 i j (ω)F i j (ω). (1)
The total photon and heat flux densities are:

γ i j = +∞ 0 γ i j (ω)dω, (2a)
q i j = +∞ 0 hωγ i j (ω)dω. (2b)
In Eq. ( 1), ∆n 0 i j (ω) corresponds to the difference of the modified Bose-Einstein distribution functions between the LED lattice T LED LED q el P LED > 1

Electroluminescent radiation field T el ≡ q el s el

PV cell P PV q el < 1
PV cell lattice T PV q in q el q el q out two layers, expressed as

n 0 i (ω, µ i , T i ) = 1 exp hω-µ i k b T i -1 , (3)
where µ is the photon chemical potential, which accounts for electroluminescent enhancement. It is set to 0 for ω < ω g (no electroluminescence below the bandgap), and can be approximated by µ ≈ eU above the bandgap. The validity of such approximation for NF-TPV applications was discussed by Callahan et al. [START_REF] Callahan | [END_REF] . Here, both components are assumed to be thermal reservoirs, i.e. they remain at constant temperatures. Thus Bose-Einstein distributions are uniform throughout each component, and only above-bandgap photons impact the electrical power generated or consumed.

The second factor in Eq. ( 1), F i j (ω), corresponds to the photon transmission function, and is obtained through the calculation of the electromagnetic transmission coefficient T following Francoeur et al. 24 :

F i j (ω) = 1 4π 2 +∞ 0 T (ω, k || )k || dk || . (4)
The use of such formalism allows to account for frustrated modes (i.e., propagative modes in the components which are tunnelling through the vacuum gap) and surface modes (e.g., surface plasmon polaritons and surface phonon polaritons, which are propagating along interfaces), which enhance the radiative heat transfer in the near field.

The photon flux density being known, the current-voltage (IV) characteristic of each component should be computed. To do so, Poisson (Eq. ( 5)), drift-diffusion (Eq. ( 6)) and continuity (Eq. ( 7)) differential equations are solved in the LED and in the PV cell:

dE dz (z) = - e ε s (n(z) -p(z) + N a (z) -N d (z)) , (5)
J n (z) = en(z)µ n E(z) + eD n dn dz (z), (6a)
J p (z) = ep(z)µ p E(z) -eD p d p dz (z), (6b)
dJ n dz (z) = -e (G(z) -R(z)) , (7a)
dJ p dz (z) = e (G(z) -R(z)) . (7b)
E corresponds to the amplitude of the electric field, ε s to the static dielectric constant, n (resp. p) to the electron (resp. hole) density, N d (resp. N a ) to the donor (resp. acceptor) doping level, J to the current density and µ n (resp. µ p ) to the electron (resp. hole) mobility, and should not be confused with the chemical potential. D n (resp. D p ) is the closely-related electron (resp. hole) diffusion coefficient, obtained using Einstein's relation. G (resp. R) is the electron-hole pair (EHP) generation (resp. recombination) rate. To account for nearfield effects, we assume that the radiative recombination rate equals the above-bandgap (subscript a) emission rate towards the other component, which gives, with Shockley-Read-Hall (SRH) and Auger non-radiative processes:

G(z) -R(z) = - dγ a,net dz (z) -R SRH (z) -R Auger (z), (8a)
R SRH (z) = n(z)p(z) -n 2 i τ p (n(z) + n i ) + τ n (p(z) + n i ) , (8b)
R Auger (z) = (C n n(z) +C p p(z))(n(z)p(z) -n 2 i ). (8c)
This neglects the effect of photon recycling on radiative generation and recombination rates. Since T and µ are considered constant in a component, the net internal photon flux (and thus the radiative G -R rate related to photon recycling) should be null. In a previous paper 19 , we solved a simplified version of this system of coupled and nonlinear equations, with an assumption that restricts the doping levels to large values and cannot handle PIN junctions. Here, we choose to fully solve it, following Gummel's iterative method 25 and its application to TPV by Blandre et al. 26 (see Sec. III of supplementary material for more information on the charge carrier transport model). At boundaries (z = z b ), we assume that charge neutrality holds (dE/dz(z b ) = 0), that majority carriers are at equilibrium (e.g., n n (z b ) = n 0 n (z b )) and that minority carriers recombine following a mechanism similar to SRH, e.g. for electrons:

J n (z b ) = e S n S p (n(z b )p(z b ) -n 2 i ) S n (n(z b ) + n i ) + S p (p(z b ) + n i ) , (9)
where S n , S p are the electron and hole effective surface recombination velocities, and are taken equal to 100 cm.s -1 . A similar expression is used for minority holes. The main material properties given as inputs of the simulations can be found in Table I. Since the variation of non-radiative recombination coefficients with temperature and alloy fraction are currently unknown, they are assumed equal to those of GaAs at 300 K. We only account for alloy-fraction variation in the effective masses.

The device considered is shown in Fig. (1), and the thickness and doping level of each layer was obtained through an optimisation process performed at d = 10 nm and S = 100 cm.s -1 . The optimised device performance is represented in Fig. (2) (in colour). It is compared to the results obtained with an ideal 0D charge carrier transport model (in black), where non-radiative recombinations (both in bulk and at interfaces) are neglected and both components are semi-infinite. Such model has already been extensively used for TPX [17][18][19] . In 2c), a similar approach is used to obtain the variation of the maximum above-bandgap efficiency with the LED voltage, in which below-bandgap heat transfer is not considered to emphasise the heat-to-electricity conversion. It is expressed as η a = P/q in,a = P/(q el,a -P LED ) (see Fig. This device is capable of producing electrical power at a rate of 2.2 W.cm -2 with an above-bandgap efficiency of around 13%, and can deliver decent amount of power (up to 0.18 W.cm -2 ) with an efficiency exceeding 25%. This maximum power output is similar to the results obtained in other articles with a 0D charge transport model where surface recombinations are neglected (but accounting for bulk non-radiative losses), with two different set of materials (AlGaAs-GaAs 18 , CdTe-InP 20 ). The large power output reached here also overcomes the performance obtained in our previous paper using a simplified 1D charge transport model without surface recombinations 19 : using optimised PIN junctions allows to reach similar or higher capabilities, in more realistic conditions.

The variations of the power output with voltages obtained ), whose size depends on the significance of the losses taken into account. 19 . In the considered case however, we see large non-monotonic variations in the low-voltage region, in which the device is not capable of producing power. The study of the LED bulk Internal Quantum Efficiency (IQE), defined as the fraction of radiative recombinations over total bulk recombinations and shown in Fig. (2c), provides a hint about the underlying physics. Indeed, IQE shows similar trends compared to the power output, and forcing it to 1 gives back the usual exponential increase. This means that the performance deterioration at low LED voltage is caused by high non-radiative recombination rates.

To analyse this in details, we examine the dependence of SRH and Auger recombinations rates with position and voltage. These results can be found in Fig. (3), and are compared with the net radiative generation-recombination rate (which corresponds to the first term on the right of Eq. (8a)). This study is performed for the LED and the PV cell at two different voltages in Fig. (3a), while keeping the opposite component unbiased. In the low-bias case, SRH recombination rates are maximum in the intrinsic layer and minimum in the doped layers, while the opposite is observed for Auger recombinations. This is still true under high bias, however their profile is much more flattened in the i-region, which is due to lower variations in the charge carrier concentrations (see Fig. (S4) in supplementary material, Sec. III). More importantly, the de-pendence of SRH and Auger recombination rates with voltage are different, Auger recombinations being for instance dominant in the LED i-region at high voltage while negligible at low voltage. This is summarised in Fig. (3b), where the variation with voltage of the quantities integrated over the thickness is shown in absolute value. While the radiative and Auger contributions have similar variations up to high voltage, the SRH one increases with a smaller rate, which is well-known for semiconductor devices (visible for instance in two-diode models [START_REF] Würfel | Physics of Solar Cells[END_REF] ). In the PV cell, recombinations only have an impact after reaching a certain voltage, since radiative generation exceeds them under low bias (corresponding to the region where the radiative and Auger terms are flat in Fig. (3b)). However, their effect is significant at any voltage in the LED in which radiative generation is generally negligible -the component works close to dark conditions. Therefore, three main regions can be delimited for the LED, as shown in Fig. (2c) and (3b). In the first, because SRH lifetimes are not high enough, SRH processes dominate recombinations at low voltage and make the IQE really low. In the second, the highest IQE is reached due to lower increase rate of SRH and moderate Auger recombinations. In the third the latter starts to be dominant, causing a decrease of IQE. The issue for TPX devices is that for small LED IQE, the LED is too inefficient to counterbalance the losses in the PV cell. Then, the device cannot produce power anymore: this is what happens between 0.1 and 0.4 V. Such feature was not observed in previous papers. For the ones using 0D models 18,20 , SRH recombination lifetimes considered were high, Yang et al. even stating that SRH recombinations were negligible in their case. In our previous paper 19 , the high FIG. 4. Impact of (a) the effective surface recombination velocity, (b) the gap distance on the device performance. In the latter, the variations of the heat flux are also analysed.

doping levels limited the SRH recombination rate.

The large amount of SRH recombinations at low voltage comes from the significant thickness of the i-region in both components, in which they exceed Auger recombinations as seen in Fig. (3a). In return, it allows to limit Auger recombinations at high voltage and thus to perform better. However, this non-monotonic behaviour will have a large impact if the working conditions are changed. This is shown in Fig. (4), where the effective surface recombination velocity S and the gap distance d are changed for the given device. Similar trends can be observed for both. While previous papers reported a smooth decrease of the performance with the gap distance 18,19 , the power output drops dramatically when using the considered device, respectively around 10 3 cm.s -1 and 100 nm. Indeed, increasing one of these quantities decreases the LED WPE. This is due either to a quicker decrease of the radiative term (directly related to q(d)) compared to the nonradiative ones (indirectly related to q(d) via the carrier concentrations) or to an increase of interface losses. As explained previously, this decreases the region in which the TPX device can deliver power, up to the point where it is no longer beneficial to bias the LED. Then the optimal case is close to TPV (almost no LED bias), as commented in Sec. II of supplementary material. For the device considered, near-field effects are thus necessary to make the thermodynamic machine work, and cannot be interpreted as a bonus to add on top of TPX performance (as it is the case for TPV).

We now study the impact of the gap distance on the total radiated heat flux. While for the gap distances considered, mainly frustrated modes intervene for interband transitions, surface modes are important below the bandgap due to surface phonon and plasmon polaritons. As a consequence, without electroluminescent amplification, the total heat flux increases quicker than the above-bandgap heat flux when the gap distance decreases. In parallel, the above-bandgap heat flux jumps around 100 nm thanks to electroluminescence. Because of these two phenomena, the fraction of radiation located above the bandgap reaches a maximum of 65% around 35 nm, and goes down to 30% at 10 nm gap distance. The full device efficiency can also be computed, and is of course lower compared to its above-bandgap equivalent because of below-bandgap photons. It is equal to 2.4% at 35 nm, and to 0.92% at 10 nm. The complete variations of these quantities with the gap distance are shown in Sec. II of supplementary material (see Fig. S3). While these values are low, it should be possible to partially suppress the below-bandgap resonances, for instance with the use of Pt thin films 20 . This would help to come closer to the above-bandgap efficiency, and limit the heat extraction issue.

In summary, the performance of an AlGaAs-GaAs NF-TPX device was simulated using fluctuational electrodynamics and an iterative resolution of Poisson, continuity and driftdiffusion equations in 1D. Compared to 0D or simplified 1D models, the study of more complex structures becomes achievable, in particular when made of weakly-doped or intrinsic layers. The realistic device considered reaches a power production of 2.2 W.cm -2 with an above-bandgap efficiency of 13% at a 10 nm gap distance. The use of PIN homojunctions allows to increase the device performance through the limitation of Auger recombination losses and shines a light on the drastic impact of SRH recombinations on TPX characteristic at low voltage. In order to obtain even better capabilities, heterojunctions are attractive due to their high carrier selectivity and the possibility to suppress SRH recombinations through fine control of the doping profile [START_REF] Santhanam | [END_REF] .

SUPPLEMENTARY MATERIAL

See supplementary material for a comparison of NF-TPX with other technologies, a more detailed analysis of the gap distance influence, and a description of the charge carrier transport model used.

FIG. 1 .

 1 FIG.1. Physical (left) and thermodynamical (right) description of the near-field thermophotonic device considered, working in an energyharvesting configuration.

  Fig. (2a), the full power-voltage TPX characteristic is shown, which can be simplified into Fig. (2b) by taking for each LED voltage the maximum power output reached for the given PV cell voltage range. In Fig. (

  (1) for definitions of the quantities), where η a is, in fact, really close to the efficiency of the maximum power points found in Fig.(2b), with 1 to 2% absolute difference.

FIG. 2 .

 2 FIG. 2. Capabilities of the device considered. The complete power characteristic and a simplified version are respectively given in (a) and (b). (c) is the simplified efficiency characteristic. The optimised case corresponds to the device shown in Fig. (1), while the ideal case is obtained using a 0D charge transport model and semi-infinite components.

FIG. 3 .

 3 FIG. 3. Comparison of SRH and Auger recombination rates with the generation-recombination radiative term, performed for the LED and the PV cell while the opposite component is unbiased. The study is done (a) as a function of the position for two different voltages, (b) as a function of the voltage for the rates integrated over the depth.

TABLE I .

 I Material properties

	Parameter Dielectric function -Reststrahlen -Interband Bandgap energy e/h rel. eff. mass e/h mobility SRH recomb. coeff. Auger recomb. coeff.	Symbol ε E g m * n/p µ n/p τ n/p C n/p	Value 1.426 eV 3.3 × 10 -6 s 10 -30 cm 6 s -1	Ref. 27,28 29 29 30 31 32 32

ACKNOWLEDGEMENTS

The project TPX-Power has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No. 951976. We thank P. Kivisaari and J. van Gastel for the useful discussions.

DATA AVAILABILITY

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

AUTHOR DECLARATIONS Conflict of interest

The authors have no conflicts to disclose.