dataesr/scientific-paragraphs-categorization huggingface dataset:
Contributions • We propose new interpretations of the semantic meta-language Skel that integrates the notion of program point in a systematic way. • We define an abstract interpretation for Skel. The abstract interpretation of Skel combined with language-specific abstractions define an analyzer for the object language. • We prove that the abstract interpretation of Skel is a sound approximation of the big-step interpretation of Skel, provided that some small language-dependent properties hold. • We implement a program which, given a Skeletal Semantics, generates an executable abstract interpreter, and we test it on toy languages. We define a basic value analyzer for a small imperative language. A Control Flow Analysis for a λ -calculus is also presented in the long version of this paper  [7].
Skeletal Semantics Skeletal Semantics offers a framework to mechanise semantics of programming languages  [1]. It uses a minimalist, functional, and strongly typed semantic meta-language called Skel  [17] , whose syntax is presented in Figure  1. The actual semantics of a language described in Skel is expressed by providing a (meta-)interpretation of the Skel language itself. In this paper, we will present two such interpretations: a big-step (or concrete) semantics and an abstract interpretation. We illustrate Skel through the definition of the skeletal semantics of a toy imperative language called While. A Skeletal Semantics is a formal description of a language and consists of declarations. We start with some type declarations (production r τ in Figure  1 ). TERM t ::= x | C t | (t,. ,t) | λ p : τ → S SKELETON S ::= t | t 0 t 1.
We now turn to Skel's term declarations (production r t of Figure  1 ), which may also be unspecified or specified. Unspecified terms are typically used for operations on values of unspecified types. For our While language, they are as follows. The types for isZero and isNotZero may be surprising. These partial functions act as filters when used in branches, as detailed below. Specified terms, on the other hand, are signatures associated with a term. A term is either a skeletal variable, a constructor applied to a term, a tuple, or an abstraction. The body of an abstraction is a skeleton, described below. Consider the declaration of term eval_expr. val eval_expr ((s, e): (store, expr) ): int = match e with | Const i → litToInt i | Var x → read (x, s) | Plus (e1, e2) → let v1 = eval_expr (s, e1) in let v2 = eval_expr (s, e2) in add (v1, v2) | Leq (e1, e2) → let v1 = eval_expr (s, e1) in let v2 = eval_expr (s, e2) in lt (v1, v2) | Rand (i1, i2) → rand (i1, i2) end The first line is syntactic sugar for val eval_expr: (store, expr) -> int = λ (s, e): (store, expr) -> where the remainder of the description is the body of the abstraction.
Big-step Semantics with Program Points In this section, we introduce our first contribution, which is the integration of the notion of program point into the framework of Skeletal Semantics. A program point maps-to a precise fragment of a given program. They play an important role in semantics-based program analysis, to indicate places where information about the execution is collected. Program points are essential to abstract interpretation as an abstract interpretation usually computes an abstraction of the state of the execution of the analysed program for each program point. Our formalisation of program points for Skeletal Semantics is modular and works for the big-step semantics of Skel, but also for the abstract interpretation of Skel, presented in Section 5. In Skel, programs are values of an algebraic data type (ADT), such as stmt or expr in the While example.
Pattern-matching of Program Points Replacing some values with program points does not change the interpretation of Skel, except when matching a program point with a pattern. Indeed, a program point pp corresponds to the sub-program prg@ pp if it exists, and it might be matched against a pattern C p. To handle this case, the program point is unfolded, meaning the constructor at prg@ pp is revealed, and the parameters of the constructor are replaced with program points if their type is a program type. To give an example, given prg as before, unfolding ε gives Seq(0, 1): the constructor is revealed and the parameters are program points because they both have type stmt ∈ T. On the other hand, unfolding 00 directly returns x, as identifiers are not program types in this example. This unfolding mechanism is added to pattern matching via the following rule: prg@ pp = C (v ′ 0 ,.
Abstract Interpretation of Skel We present our main contribution in this paper, which is the definition of an abstract interpreter of Skel that is sound with respect to the big-step semantics of Section 4. This abstract interpreter will serve as the foundations of a methodology for building abstract interpreters for object languages from their skeletal semantics. In this methodology, several ingredients must be provided to generate such an abstract interpreter. • An abstract instantiation of unspecified types to sets of abstract values, each of which comes with a concretisation function, a partial order, and an abstract union operator. Our framework automatically extends these definitions to all types. • A state of the abstract interpretation (AI-state in the following) used to carry additional information during the abstract evaluation.
Let σ 0 ∈ V ppt (store) and σ ♯ 0 ∈ V ♯ (store) be the concrete and abstract stores with empty domain. Let E 0 = { s → σ 0 ,t → ε } and E ♯ 0 = s → σ ♯ 0 ,t → ε be a concrete and an abstract Skel environments. We recall that ε is the program point of the root of prg, the analysed program. Let A 0 be the empty mapping from program points and flow tags (In or Out) to abstract stores. Lemma 7 σ 0 ∈ γ store (A 0 , σ ♯ 0 ) Lemma 8 Let Γ = { s → store,t → stmt }, E 0 ∈ γ Γ (A , E ♯ 0 ). The abstract interpreter computes an abstract store that is a correct approximation of the concrete store returned by the big-step semantics. Theorem 2 E 0 , eval stmt (s,t) ⇓ PP σ emp, A 0 , E ♯ 0 , eval stmt (s,t) ⇓ ♯ σ ♯ , A =⇒ σ ∈ γ(A , σ ♯ ) As an example, take prg ≡ x := 0; while (x < 3) x := x + 1. The concrete and abstract interpretations will find that E 0 , eval stmt (s,t) ⇓ PP { x → 3 } emp, A 0 , E ♯ 0 , eval stmt (s,t) ⇓ ♯ { x → [0, +∞] } , A In accordance with Theorem 2, we observe that { x → 3 } ∈ γ(A , { x → [0, +∞] }) The abstract interpreter returns an imprecise result.
Related Work Our work is part of a large research effort to define sound analyses and build correct abstract interpreters from semantic description of languages. At its core, our approach is the Abstract Interpretation  [4, 5]  of a semantic meta-language. Abstract Interpretation is a method designed by Cousot and Cousot to define sound static analyses from a concrete semantics. In his Marktoberdorf lectures  [3] , Cousot describes a systematic way to derive an abstract interpretation of an imperative language from a concrete semantics and mathematically proved sound. We chose to define the Abstract Interpretation of Skel, as it is designed to mechanise semantics of languages. The benefit of analysing a meta-language is that a large part of the work to define and prove the correctness of the analysis is done once for every semantics mechanised with Skel.
However, it is often less precise than defining a language specific abstract interpretation. Moreover, there have been several papers describing methods to derive abstract interpretation from different types of concrete semantics  [4, 20, 13] , we chose to derive abstract interpreters from a big-step semantics of Skel. Schmidt  [20]  shows how to define an abstract interpretation for λ -calculus from a big-step semantics defined co-inductively. The abstract interpretation of Skel and its correctness proof follow the methods described in the paper. However Skel has more complex constructs than λ -calculus, especially branches. Moreover, the big-step of Skel is defined inductively, thus reasoning about non-terminating program is not possible. Also, to prove the correctness of the abstract interpretation of Skel, we relate the big-step derivation tree to the abstract derivation tree, similarly to Schmidt, but a key difference is that our proof is inductive when Schmidt's proof is co-inductive.
Moreover, our method computes an AI-state that collects information throughout the interpretation and allows to use widening using the update functions, rather than computing an Input/Output relation. The idea of defining an abstract interpreter of a meta-language to define analyses for languages has been explored, for example by Keidel, Poulsen and Erdweg  [9]. They use arrows  [6]  as meta-language to describe interpreters. The concrete and abstract interpreters share code using the unified interface of arrows. By instantiating language-dependent parts for the concrete interpretation and the abstract interpretation, they obtain two interpreters that can be proven sound compositionally by proving that the abstract language-dependent parts are sound approximation of the concrete language-dependent parts, similarly to Skel.
Conclusion In this paper, we propose a methodology for mechanically deriving correct abstract interpreters from mechanised semantics. Our approach is based on Skeletal Semantics and its meta-language Skel, used to write a semantic description of a language. It consists of two independent parts. First, we define an abstract interpreter for Skel which is target language-agnostic and is the core of all derived abstract interpreters from Skeletal Semantics. The abstract interpreter of Skel is proved correct with respect to the operational semantics of Skel. Second, for a given target language to analyse, abstractions must be defined. The abstract domains are defined by instantiating the unspecified types and providing comparisons and abstract unions of abstract values. The semantics of the language-specific parts are defined by instantiating the unspecified terms.
By combining the abstract interpreter of Skel and the abstractions of the target language, we derive a working abstract interpreter specialised for the target language, obtained by meta-interpretation of Skel. We prove a theorem which states that the abstract interpreter of the target language is correct if the abstract instantiation of the unspecified terms are sound approximation of the concrete instantiation of the unspecified terms. We illustrate our method to build abstract interpreters on two examples: a value analysis for a small imperative language, and a CFA for λ -calculus (in the long version  [7] ). The approach has been evaluated by an implementation of a tool  [19]  to generate abstract interpreters from any skeletal semantics. It was tested on While and λ -calculus and resulted in executable, sound analyses validating the feasibility of the approach.
The current abstract interpreters that we obtain have limitations to their precision. Part of this imprecision stems from the fact that we generate abstract interpreters for any language based on an abstract interpreter for the Skel meta-language skeletal semantics. An interesting feature of the approach is that some precision can be gained in a generic fashion by improving the underlying abstract interpretation of Skel. For example, our interval analysis for While does not refine the abstract values when entering a part of the program guarded by a condition. Take If(Equal(x, 0), Skip, Assign(x, 0)), evaluated in store where { x → ⊤ }. Our abstract interpreter returns state { x → ⊤ }. Indeed, the condition can be true or false thus both branches of the if construct are evaluated but each one is computed in the store { x → ⊤ } because the condition is not used to refine the abstract values.
Notably, this enables quicker reactions to external events, crucial for critical systems. For instance, let us admit that we wish to satisfy a property ϕ at least once during a time interval  [a,b]. If the property is satisfied in the interval, then there is no need to wait for time b to affirm that the property is indeed verified. This paper introduces preliminary works on the specification and verification of STL operators, using synchronous observers. The rest of the document focuses on discrete times, and non nested temporal Our main contribution concerns the formal verification of the correctness of STL operators. To this end, we provide a three-valued online STL semantics as well as the implementation of each STL operator in the synchronous language Lustre. The soundness of the implementation is expressed as a set of lemmas and automatically proved with the Kind2 model-checker.
(X ,t) ⊧ µ ⇔ µ(t) (1) (X ,t) ⊧ ¬ϕ ⇔ ¬((X ,t) ⊧ ϕ) (2) (X ,t) ⊧ ϕ 1 ∧ ϕ 2 ⇔ (X ,t) ⊧ ϕ 1 ∧ (X ,t) ⊧ ϕ 2 (3) (X ,t) ⊧ ϕ 1 ∨ ϕ 2 ⇔ (X ,t) ⊧ ϕ 1 ∨ (X ,t) ⊧ ϕ 2 (4) (X ,t) ⊧ ϕ 1 U [a,b] ϕ 2 ⇔ ∃t ′ ∈ t + [a,b] ∶ (X ,t ′ ) ⊧ ϕ 2 ∧ ∀t ′′ ∈ [t,t ′ ] ∶ (X ,t ′′ ) ⊧ ϕ 1 (5) (X ,t) ⊧ ◇ [a,b] ϕ ⇔ ∃t ′ ∈ t + [a,b] ∶ (X ,t ′ ) ⊧ ϕ (6) (X ,t) ⊧ ◻ [a,b] ϕ ⇔ ∀t ′ ∈ t + [a,b] ∶ (X ,t ′ ) ⊧ ϕ (7) Section 2 covers the preliminary concepts, including the Signal Temporal Logic, the synchronous language Lustre, the model checker Kind2, and an introduction to three-valued logic. We formalise an online semantics for STL operators in Section 3, and detail its Lustre implementation in Section 4. Finally, Section 5 describes the formal correction of the operators implementation.
(1). Equation (2) (Negation) is the logical negation of ϕ. Equation (3) (And) is the logical conjunction between ϕ 1 and ϕ 2. Equation (4) (Or) is the logical disjunction between ϕ 1 and ϕ 2. It is worth mentioning that, in STL, all temporal operators have to be associated to a bounded, nonsingleton time interval. Equation (5) (Until) describes a temporal operator that is satisfied if  Lustre  [5]  is a synchronous language for modeling systems of synchronous reactive components. A Lustre program L is a finite collection of nodes [N 0 ,N 1 ,. ,N m ]. The nodes satisfy the grammar described in Table  1  in which td denotes type constructors, including enumerated types, and v either constants of enumerated types C or primitive constants such as integers i. Each node is declared by the grammar construct d of Table  1.
Specifying and verifying assume-guarantee contracts with Kind2 The annotation language CoCoSpec  [6]  was proposed for Lustre models to lift the notion of Hoare triple  [12]  and Assume/Guarantee statements as dataflow contracts. A contract is associated to a node and has only access to the input/output streams of that node. The body of a contract may contain a set of assume (A) and guarantee (G) statements and mode declarations. First line of the contract (line 3) defines a local variable clk as an integer, which initially takes the value 0 and is then incrementing at each time. The assume at line 4 indicates to model checker that it has to prove the Lustre node only in the cases where the condition a ≥ 0 is satisfied. If another Lustre node is using timeab, Kind-2 also checks that this node could not provide an input a which runs counter to this assumption.
Three-valued logic We present here the interest of three-valued logic, and introduce Kleene's three-valued logic, which we use in the next section to formalise an online version of STL operators. For most tools, when performing monitoring of STL predicates, for a given value of simulation data, the trajectory is typically finite. It is produced by a simulation engine and stored in a data file. It is then loaded by the monitoring tool and analyzed with respect to the STL specification. In this offline setting, the final outcome indicates whether or not the input signal satisfies the specification. It is a boolean output. Temporal operators are used to evaluate properties that change over time. Most of the time in these situations, we need to wait to decide whether a temporal property is satisfied or violated.
Operators implementation strategy Based on this online semantics, we propose an implementation of Eventually, Always and Until in discrete time. We use the synchronous language Lustre. We recall that all the nodes are available at https://garoche. net/publication/2023_fmas_submission/. Useful constructs for the implementation First, we define the basic nodes needed to implement the temporal operators. Node min returns the minimum value between two variables. Node exist(time :bool; prop: bool) returns True as soon as a property prop has been satisfied during the time interval represented by time. Node forall_a(time: bool ; prop: bool) returns True if a property prop has always been True during the time interval. All these nodes can easily be implemented in Lustre. Regarding the implementation of the nodes detecting whether or not we are in the time slot t + [a,b], and since we work with finite intervals, we can optimize our clock, preventing it from incrementing to infinity.
Conclusion. In this paper, we propose an online discrete implementation of the STL semantics, in the continuity of Balsini's work  [2]. Our contribution is twofold. First, we proposed an implementation based on Kleene's three-valued logic in order to be able to represent indeterminacy. Second, we formally demonstrated the soundness of our implementation, proving the validity of each operator with respect to its semantics. Our approach was the following: we first defined the online STL semantics, and used it to build each STL operator as a synchronous observer in the Lustre language. Finally, we formally demonstrated the correctness of their implementation, using the Kind2 model-checker. We proceed by induction on the size of temporal intervals. We succeed to demonstrate all the proof objectives for each temporal operator implemented.
Polysomnographic sleep architecture parameters are commonly used to diagnose or evaluate treatment of sleep disorders. Polysomnography (PSG) having practical constraints, the development of wearable devices and algorithms to monitor and stage sleep is rising. Beside pure validation studies, it is necessary for a clinician to ensure that the conclusions drawn with a new generation wearable sleep scoring device are consistent to the ones of gold standard PSG, leading to similar interpretation and diagnosis. This paper reports on the performance of Somno-Art Software for the detection of differences in sleep parameters between patients suffering from obstructive sleep apnea (OSA), insomniac or major depressive disorder (MDD) compared to healthy subjects. On 244 subjects (n = 26 healthy, n = 28 OSA, n = 66 insomniacs, n = 124 MDD), sleep staging was obtained from PSG and Somno-Art analysis on synchronized electrocardiogram and actimetry signals.
Mixed model analysis of variance was performed for each sleep parameter. Possible differences in sleep parameters were further assessed with Mann-Whitney U-test between the healthy subjects and each pathology group. All sleep parameters, except N1+N2, showed significant differences between the healthy and the pathology group. No significant differences were observed between Somno-Art Software and PSG, except a 3. 6±2. 2 min overestimation of REM sleep. No significant interaction 'group'*'technology' was observed, suggesting that the differences in pathologies are independent of the technology used. Overall, comparable differences between healthy subjects and pathology groups were observed when using Somno-Art Software or polysomnography. Somno-Art proposes an interesting valid tool as an aid for diagnosis and treatment follow-up in ambulatory settings.
Indeed, sleep stages are dependent on the balance of the autonomic nervous activity, parasympathetic tone being predominant during slow wave sleep while sympathetic tone being predominant during REM sleep  [7, 8]. Somno-Art Software, a cardiac-based sleep scoring algorithm, has recently been evaluated in healthy subjects and pathological sleep profiles  [9, 10]. Good and excellent intraclass correlation (according to  Cicchetti [11]  cutoffs) between Somno-Art Software and PSG for standard sleep architecture and continuity parameters were found in healthy subjects and in patients suffering from insomnia, obstructive sleep apnea (OSA) or major depressive disorder (MDD). Moreover, the scoring provided by Somno-Art Software showed a robust interscorer reliability in the range of visual scorers  [12].
Thus, treating clinicians may also be interested in the performance of Somno-Art Software in detecting differences in sleep parameters characteristic in patients, leading to similar interpretation and diagnosis when using the sleep staging from the Somno-Art Software or gold standard PSG. To do so, the differences of standard sleep parameters extracted from the sleep recordings coming from healthy subjects and patients suffering from OSA, insomnia or MDD were compared. It was hypothesized that comparable findings would be observed with the visual scoring of PSG recordings and the Somno-Art Software analysis.
Dataset Source studies. The present dataset includes 6 studies and comprises data coming from both healthy subjects (two studies) and sleep disordered patients (one study with OSA patients, one with chronic insomniacs and two with depressed patients). The primary objective of the first healthy subjects study was to investigate relationship between daytime activity and night sleep structure and the impact of noise on sleep pattern. For the second one, the primary objective was to investigate the effect of light on sleep, wake, electroencephalogram (EEG) and cognitive performances as a function of homeostatic sleep drive. All recorded nights from these two healthy subjects' studies were included in the dataset. The OSA study included patients diagnosed with OSA syndrome during a clinical evaluation night.
The insomniac study and the 2 depression studies primary objectives were to evaluate the efficacy, safety and tolerability of investigational drugs. Only pre-treatment nights were included in the dataset. For all studies included in the present analysis and before undergoing sleep recordings, a standard screening of patients and healthy subjects' health status was done. More information on the protocol descriptions are detailed in the S1 Appendix. All study protocols were approved by institutional review boards (IRB) (Healthy study 1: Arztekammer Berlin, EudraCT N˚: 2012-001043-44; Healthy study 2: Comitede protection Funding: This study was supported by PPRS SAS. There was no additional external funding received for this study. The funder provided support in the form of salaries for authors LT, DK, GF, AUV.
JYS and JBS participated in the study design, data collection and analysis, decision to publish, and preparation of the manuscript. The specific roles of these authors are articulated in the 'author contributions' section. Competing interests: I have read the journal's policy and the authors of this manuscript have the following competing interests: This study was supported by PPRS SAS. JYS and JBS are shareholders of PPRS SAS. LT, GF, DK and AUV, are employees of PPRS SAS. JBS is a payed consultant of PPRS Research lnc. JYS is shareholder of V-WATCH SA. PB, HC and LS are working in hospitals that have received monetary contribution for running the healthy study 2 and the OSA study. The remaining authors declare that the research was conducted in the absence of any commercial or financial relationships that could be construed as a potential conflict of interest.