dataesr/scientific-paragraphs-categorization huggingface dataset:
Illustrative example We consider in this example the daily log returns of the Standard & Poor's 500 index (S&P 500, for short). The log returns (or simply returns) are defined by r t = 100 log(p t /p t-1 ) where p t is the price index of the S&P 500 at time t. The observations of the S&P 500 index cover the period from January 3, 1950 to February 14, 2019. The length of the series is n = 17, 391. The data can be downloaded with the R package quantmod. The phenomenon of long memory has been widely studied for financial series. Ding et al. [1993]  have shown that the positive powers of the absolute value of returns have more per-sistence than the returns themselves. We choose here the case of squared returns. The mean and the standard deviation of (r 2 t ) t≥1 are 0, 9347 and 5, 0036. As in  Ling [2003] , we consider the centered series (X t ) t≥1 of the squared returns, that is, X t = r 2 t -0, 9347.
The sample autocorrelations of the series (X t ) t≥1 (see Figure  5 ) decrease very slowly and are approximated by the function in blue (which is not integrable on R). This suggests that this series has a long memory. It has been statistically validated in our previous work (see  Boubacar Maïnassara et al. [2021a] ) that the time series (X t ) t≥1 could be adjusted by a weak FARIMA(1, d, 1) model. It is worth emphasizing that the strong FARIMA fitting with the same orders is rejected for this series. The calibration of such models with the LSE is time consuming. Consequently, we propose a remote solution (API REST with the HTTP protocol) to provide fast and similar estimates with the same asymptotic properties as the LSE. In R, we can access to this API with the httr package using the POST command and format our data into JSON (package jsonlite).
Acknowledgments. This research benefited from the support of the  ANR  project  "Efficient inference for large and high-frequency data " ( ANR-21-CE40-0021 ), the " Chair Risques Émergents ou Atypiques en Assurance ", under the aegis of  Fondation du Risque , a joint initiative by  Le Mans University  and MMA company, member of  Covea group  and the " Chair Impact de la Transition Climatique en Assurance ", under the aegis of  Fondation du Risque , a joint initiative by  Le Mans University and Groupama Centre-Manche company , member of Groupama group.
In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI-previously only described in prose in the OCaml manual-as well as the first program logic to reason about the interactions of program components written in OCaml and C.
INTRODUCTION In recent years, there has been tremendous progress on developing verification systems based on program logics (in particular, separation logics), which support the modular verification of complex programs in a rich and diverse array of languages. Notable examples include VST-Floyd  [Cao et al. 2018]  and RefinedC  [Sammler et al. 2021]  for C, RustBelt  [Jung et al. 2017]  and RustHornBelt  [Matsushita et al. 2022]  for Rust, and Cosmo  [Mével et al. 2020]  for multi-core OCaml-all of which are fully mechanized in Coq. The above-cited systems all employ a common recipe: (1) Design an operational semantics for the language, which serves as the "ground truth" about program behavior. (2) Build a (Hoare-style) program logic for the language, which supports higher-level proof rules for compositionally verifying program correctness.
In this paper, we take the first steps towards filling this gap by proposing a recipe for building multi-language program logics. To keep matters concrete, we focus on a specific instance of the problem: verifying multi-language programs written in a combination of OCaml and C. OCaml has structured values (e. g. , sums, pairs, lists, and references), a garbage-collected memory, and a type system providing strong guarantees about its programs. C has integer values and pointers, manually managed memory, and a type system providing only weak guarantees about its programs. Nevertheless, there exists a bridge between the two-the OCaml FFI-which exposes enough of the OCaml runtime to C to convert values, execute callbacks, and share memory.
For one, in C, they reside in memory (with a concrete address where they are stored) whereas, in OCaml, they are conceptually "just values" (i. e. , they are copied when passed around). However, that is not the only difference. The fields of buf are immutable (e. g. , cap cannot change) and the used-reference is mutable. From the perspective of C, however, both records and references have the same representation, runtime blocks. It is up to the programmer to remember that one of them is allowed to be mutated whereas the other is not. Finally, C code can embed its own data into OCaml through custom blocks (here the data-field) and it can access and modify that data as needed whereas the data-field of the record is completely opaque to OCaml. In program code, the differences between OCaml and C are bridged through so-called "glue code", code which uses the OCaml FFI to link up program parts written solely in either OCaml or C.
For program verification, the story is not so clear yet. For instance, when we reason about glue code, how do we reconcile the two very different views that OCaml and C have on values of type buf? To design a multi-language program verification analogue of the single-language recipe, we have to bridge the language gap at two different levels: The operational semantics. At the operational semantics level, the challenge is that no existing multi-language semantics explains how to reconcile the key differences between both languages (i. e. , interacting with the OCaml garbage collector and runtime, registering "roots", executing callbacks, etc. ). However, there are promising starting points. Patterson et al. [2022]  combine a garbage collected language and a language with manual memory management.
Unfortunately, they do so using an elaboration semantics to a shared target language with garbage collection, which does not exist in the case of OCaml and C. Sammler et al. [2023]  propose an approach to multi-language semantics that uses modular combinators to connect languages by composing their operational semantics. As such, their approach fits well with step one of the single-language recipe. Unfortunately, while they consider languages with significant differences (e. g. , different calling conventions and memory models), they do not consider garbage collection or a runtime. The program logic. At the program logic level, the main challenge is preserving language-local reasoning. That is, chunks of code that are solely written in C or solely written in OCaml should enjoy reasoning principles that are fine-tuned to their respective language (without being impacted by the existence of the other language).
However, preserving language-local reasoning is easier said than done. For one, the two program logics will have different views on the same piece of state (e. g. , a buf-value in OCaml will be viewed as nested runtime blocks on the C side). Changes to runtime blocks on the C side (e. g. , updating the block storing the number of used bytes) correspond to changes in the state on the OCaml side (e. g. , changing the used-reference in the buffer). Another, more subtle issue with preserving language-local reasoning is that code written in one language can potentially violate language-specific invariants of the other. For example, OCaml-as a functional language-makes pervasive use of immutable values. When linked with C, the C code can observe the runtime representation of those values and, in principle, mutate their contents, albeit with unknown consequences as far as the OCaml semantics is concerned.
Melocoton In this paper, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. It extends the single-language recipe for program verification to a multi-language setting as follows: (1) As a starting point, we take simplified versions of OCaml and C called C and ML (see §2. 2) and-following the single-language recipe-we define their canonical operational semantics, → C and → ML. Moreover, again following the recipe, we derive language-specific program logics for them. Since both languages have non-trivial state, we derive two separation logics, called Iris C and Iris ML , in the separation logic framework Iris  [Jung et al. 2018 [Jung et al. , 2015]]. (2) We extend the language-local program logics Iris C and Iris ML with reasoning principles for "external calls".
Contributions. The main contribution of this paper is Melocoton, a multi-language program verification system for programs written in OCaml and C. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI-previously only described in prose in the OCaml manual [oca 2023b]-and the first program logic to reason about the interactions of OCaml and C. Melocoton's operational semantics ( §3) is the first multi-language semantics that models interactions with an OCaml-style garbage collector. To define it, we take inspiration from  Sammler et al. [2023] : we define an operational semantics that modularly embeds the semantics of ML and C , and we use angelic and demonic non-determinism to bridge the gap between the two semantics. As mentioned above, the work of Sammler et al.
does not cover the kind of language interactions that are possible through the OCaml FFI, which are what makes interoperability between OCaml and C interesting. To capture them, we use a carefully designed model of the core aspects of the OCaml runtime (e. g. , runtime blocks, garbage collection, "roots", callbacks, etc. ). Melocoton's program logic ( §4) is the first separation logic (and program logic) for a multilanguage setting with different memory models (including garbage collection). We use separation logic to reason about the state of OCaml and C, and we use step-indexing-inherited from Iris-to handle the recursive and higher-order features of OCaml. To soundly combine (1) angelic nondeterminism and (2) the higher-order features of OCaml, as it turns out, we have to use a richer form of step-indexing than what is provided out-of-the box by Iris: we have to use transfinite step-indexing and, thus, define Iris ML+C in Transfinite Iris  [Spies et al.
MELOCOTON BY EXAMPLE We explain the key ideas underlying Melocoton using a motivating example: importing a C compression library into OCaml. We focus on the program logic level of Melocoton and follow the spirit of the multi-language recipe: first develop language-local reasoning principles, then focus on language interoperability. Concretely, we discuss the C library and an OCaml client ( §2. 1), we explain how to reason about them locally ( §2. 2), we discuss the OCaml FFI "glue code" that ties them together ( §2. 3), we explain how to reason about the glue code ( §2. 4), and, finally, we address the view reconciliation problem ( §2. 5). Throughout this paper, we use colors to distinguish different languages: magenta for OCaml, dark blue for C, and light blue for primitives of the OCaml FFI.
To make sure that the capacity of the output buffer outp suffices, the library provides the function snappy_max_compressed_length, which computes an upper bound on the compressed size. The OCaml client. The OCaml client is_compressible wants to use the compression library to check whether an array of characters will shrink in size when compressed. When we implement it in OCaml, the first stumbling block that we encounter is that is_compressible takes in an OCaml array of characters (i. e. , a built-in array managed by the OCaml garbage collector), but the C library function snappy_compress expects two char pointers (i. e. , raw pointers to C buffers of bytes). The issue is the that the two types, char array and char *, are not the same-they are not even part of the same language. To circumvent this problem, we introduce glue code: C code that uses the OCaml FFI to mediate between is_compressible and snappy_compress.
For now, we delay a discussion of the C implementation of the glue code (to §2. 3) and focus on its OCaml interface (Lines 3-9). The interface consists of (1) a small buffer library (loosely inspired by OCaml's Bigarray library [oca 2023a]) and (2) wrappers of the compression functions operating on buffers. The interface declares an abstract  type raw_bytes, a record for buffers buf, and four functions to operate on buffers: buf_alloc allocates an uninitialized buffer of a given capacity (initially using 0 bytes); buf_free frees a buffer (since memory management is manual in C, we have to free allocated buffers); buf_upd updates a range of the buffer using a callback (additionally increasing the number of used bytes if necessary); and buf_get reads a byte of the buffer. The compression functions are wrapped as wrap_max_len (for snappy_max_compressed_length) and wrap_compress (for snappy_compress).
Language-Local Reasoning Before we turn to the implementation of the glue code that connects the OCaml client and the C library, let us first illustrate one of the central ideas of Melocoton: preserving language-local reasoning. Even without knowing the implementation of the glue code (or the OCaml FFI), we can verify the C compression library and the OCaml client already in language-specific program logics. As mentioned in §1, we consider rather idealized versions of C and OCaml in this paper, called C and ML , which are depicted in Fig. 3. We first discuss the language C and verify the compression library in Iris C. Then, we contrast C with ML and verify the client in Iris ML. The language C. The essential features of C are its very simple form of values (i. e. , integers or addresses ) and its flat memory model.
They are non-intrusive and minimal such that ML does not even (need to) know which languages it is interacting with. First, there are foreign values " ", where is an abstract identifier. They can be used by other languages such as C to "embed" their own data into ML. We will use this feature of OCaml to embed the underlying C buffer into OCaml in our running example (in §2. 5). Foreign values are abstract: they can be passed around via function calls, but there is no language construct in ML to inspect their contents. Second, after executing an external function, locations in the heap of ML can store data that is temporarily inaccessible from ML (see §3. 1). Whenever this is the case, the ML heap stores at the respective location and accesses in ML will get stuck. Third, and most interestingly, ML contains a language construct for external function calls call fn ì V.
The syntactic construct call fn ì V has no meaning in the language-local semantics of ML (i. e. , it is stuck 3  in the semantics of ML ). As such, ML does not have to include any rules in its semantics for executing code of other languages (e. g. , C ). Instead, we will assign meaning to external calls in the combined multi-language ML+C (see §3), where external calls in ML are linked with their implementation in C. Verifying the OCaml client. Let us turn to the verification of is_compressible in Iris ML. We prove that given ownership over an array of integers, the function returns an unspecified boolean, meaning {ℓ ↦ → ML ì } is_compressible ℓ @ ∅, Ψ buf {V ′. V ′ ∈ {true, false} * ℓ ↦ → ML ì } ML. This specification is not particularly exciting, but it suffices to illustrate the interaction with the external functions implemented in C.
The resources of Iris ML (e. g. , "ℓ ↦ → ML ì V ") and its reasoning rules (e. g. , read-ml, write-ml, and alloc-ml) are standard. Thus, we focus mainly on the treatment of external function calls. External calls allow us to slice the verification of a program into the language-local parts and the parts that are implemented in another language. In is_compressible, the first time that we call an external function is when we allocate the initial buffers inp and outp with buf_alloc (Line 12). Suppose (for a moment), for the sake of explanation, that buf_alloc was implemented in OCaml. In this hypothetical scenario, the standard way to proceed would be to prove (once) and afterwards apply (multiple times) the Hoare triple: { > 0} buf_alloc( ) @ ∅, Ψ buf {V. buffer ML (V, , [])} ML where buffer ML (V, n, ì m) ≜ ∃ℓ, V ′.
V = ⟨n,ℓ,V ′ ⟩ * ℓ ↦ → ML [| ì m|] * raw_bytes(V ′ , n, ì m) asserts that V is a tuple containing the buffer capacity n, a ML reference ℓ for the used field, and a value V ′ containing the underlying integers ì m. How V ′ stores the integers ì m is irrelevant for the verification of is_compressible, meaning we can stay at the abstraction of "raw_bytes(V ′ , n, ì m)". (As we will see in §2. 5, the definition of raw_bytes uses ML 's "foreign values" and knowledge about the OCaml FFI. ) After applying the Hoare triple, we can then use the buffer that buf_alloc returns to resume the verification of is_compressible. Of course, buf_alloc is not actually implemented in OCaml. Nevertheless, in our proof of is_compressible, we want to stay as close as possible to the language-local reasoning sketched out above.
To do so, we introduce reasoning principles to "skip" external function calls by drawing a boundary at their specification. For example, in the verification of is_compressible, we want to prove the precondition > 0 of buf_alloc to call it and then resume afterwards with the postcondition buffer ML (V, , []). To make this reasoning sound, we take inspiration from the work on open simulations  [Hur et al. 2012 ] and of de Vilhena and Pottier [2021] on a program logic for effect handlers. Concretely, we parameterize Hoare triples by an interface Ψ ∈ Intf (Val) ≜ FnName → list(Val) → (Val → iProp) → iProp that maps each external call to its specification. Formally, an interface Ψ is a "predicate transformer" that takes in a function name fn, a list of argument values ì , and a postcondition and then produces the precondition "Ψ fn ì " required to call fn with arguments ì.
A Primer of the OCaml FFI Having verified the OCaml client and the C compression library (from Fig. 2 ), we now turn to the "glue code" that connects them. Before we can verify any glue code (in §2. 4), we first have to understand the central concepts of the OCaml FFI and how they are used in our example. To explain them, we focus on the implementation of buf_alloc (in Fig. 5 ); the implementation of the remaining glue code functions can be found in the supplementary material  [Guéneau et al. 2023 ]. The representation of OCaml values. In C, all OCaml values-regardless of their type, including buf, raw_bytes, int, and char array-are exposed by the OCaml runtime as runtime values-of type value. They are either integers or pointers to runtime blocks (i. e. , chunks of memory in the heap of the OCaml runtime).
Integers are used to encode OCaml's integers (i. e. , int) and other simple types such as bool and unit. Pointers are used to encode OCaml's structured values (e. g. , pairs, data types with arguments, arrays, etc. ). For example, as depicted in Fig. 1 , a value of the buffer record is represented as a pointer to a runtime block with three values, one storing an integer for the capacity, one storing a reference for the used field, and another storing the underlying C buffer. To embed the C buffer-a raw C pointer which is not of type value-into OCaml, the runtime offers so-called "custom blocks". Custom blocks are runtime blocks that embed native C data (e. g. , pointers) into OCaml as foreign values. 5 Manipulating OCaml values in C. As a function using the OCaml FFI, buf_alloc has to interact correctly with the OCaml runtime primitives (in light blue) and the OCaml garbage collector.
Tiptoeing around the OCaml garbage collector. One fundamental difference between OCaml and C reveals itself only implicitly in the code in Fig. 2 : the presence of the OCaml garbage collector (GC). That is, memory management in OCaml is based on garbage collection, meaning once a runtime allocated object (i. e. , one that is represented as a runtime block) becomes unreachable (i. e. , no part of the OCaml code can access it anymore), the GC can deallocate it to reduce the amount of memory consumed. This is in stark contrast to the manual memory management of C, where memory has to be explicitly allocated and eventually deallocated. One immediate consequence of this difference is that the buffer library needs to provide a buf_free-function to OCaml (Line 5), because otherwise the buffer will stay in memory forever.
An Interface for the OCaml FFI How should we verify glue code such as buf_alloc in Fig. 5 ? On the one hand, the code is written in C, so it would be natural to use the language-local logic Iris C to reason about it. On the other hand, semantically, the code is more concerned with OCaml values (and the runtime representation thereof) than with C data structures, C pointers, and C-specific features. We answer this question with our next key idea: importing a logic for the OCaml FFI into the language-local logic Iris C. Conceptually, "the OCaml FFI" is (1) a lower-level model of OCaml's values and heap that is exposed to C and (2) a set of "runtime primitives" available to C to operate on this lower-level representation. Together, these two parts of the OCaml FFI form a clean abstraction over the actual, underlying C data representation (and the implementation of the garbage collector).
We use them as a "middle ground" between C and OCaml in this work. Concretely, (1) we define a notion of runtime values, runtime heaps, and runtime separation logic resources and (2) we specify the runtime primitives as external functions in Iris C using an interface Ψ FFI. In doing so, we get access to abstract reasoning principles about the OCaml runtime while retaining the language-local reasoning principles of Iris C. The resources of the OCaml runtime. To define the runtime interface, we take the view that memory exposed by the OCaml FFI is an abstract heap of runtime blocks and then relate this heap to both its C and OCaml representations (i. e. , map it to pointers and integers in C and map it to structured values and references in OCaml). We will describe the interface of the OCaml runtime in more detail in §4.
View Reconciliation We have sketched how to verify a mixed OCaml-and-C program from the OCaml side using Iris ML and from the C side using Iris C (including glue code using the OCaml FFI via Ψ FFI ). The last remaining piece of the puzzle is connecting the different parts, which brings us to the view reconciliation problem. Take buf_alloc again for example. We have discussed how to assume a specification about it in Iris ML (in §2. 2) and how to prove a specification for it in Iris C (in §2. 4). However, so far, the two specifications do not match up-the Iris C -specification uses the resources for the runtime and the Iris ML -specification the resources for ML. There is a fundamental challenge here. The two logics, Iris C (extended with Ψ FFI ) and Iris ML , are about entirely different languages, and yet they express views on the same underlying data.