bluuebunny/crossref_metadata_2025_split huggingface dataset:
Interaction between time, ASPECTS, and clinical mismatch
Authors: Desai Shashvat M , Tonetti Daniel A , Molyneaux Bradley J , Atchaneeyasakul Kunakorn , Rocha Marcelo , Jovin Tudor G , Jadhav Ashutosh P 
Published: April 2020

BackgroundImaging-based patient selection for neurothrombectomy is reliant on the identification of irreversibly damaged brain tissue (core) and salvageable tissue (penumbra). The DAWN trial used the clinical-core mismatch (CCM) paradigm (clinical deficit out of proportion to infarct volume). We aim to determine the prevalence of CCM in large vessel occlusion (LVO) strokes and study the impact of time and the Alberta Stroke Program Early CT Score (ASPECTS) on the likelihood of mismatch.MethodsWe performed a retrospective observational analysis of internal carotid artery/middle cerebral artery M1 occlusions with available advanced imaging (relative cerebral blood flow/MRI). We used automated software for infarct volume analysis and ASPECTS determination. The prevalence of CCM and the impact of time and ASPECTS were analyzed.ResultOne hundred and eighty-five LVO strokes were included. Mean age was 71±15 years and median National Institutes of Health Stroke Scale score was 17 (range 12–21). Mean ischemic core volume was 50±69 mL. Within 0–24 hours, CCM was present in 53% and ranged from 63% in 0–3 hours to 25% at 21–24 hours (p=0.03). Prevalence of mismatch reduced 1.6% for every 1 hour increase in time to imaging. CCM prevalence by ASPECTS groups was: ASPECTS 9–10: 77%, ASPECTS 6–8: 65%, ASPECTS 0–5: 13% (p<0.01), with a 6.4% decrement for every 1 point decrease in ASPECTS. The prevalence of mismatch did not diminish over time among ASPECTS groups and higher ASPECTS was an independent predictor of CCM (OR 1.4 (95% CI 1.1 to 1.7), p<0.001).ConclusionsCCM is present in 57% and 50% of LVO strokes in the 0–6 and 6–24 hour window, respectively. The prevalence of mismatch declines with increasing time (1.6%/hour) and decreasing ASPECTS (6.4%/point). Among ASPECTS groups the prevalence of mismatch does not decline over time. These data support the use of an ASPECTS-based paradigm for late window patient selection.
COVID-19 outbreak and its monetary implications for dental practices, hospitals and healthcare workers
Authors: Farooq Imran , Ali Saqib 
Published: April 2020

AbstractThe novel COVID-19 came under limelight few months back (December 2019) and has recently been declared a pandemic by WHO. It has resulted in serious financial implications being faced by dental practices, hospitals and healthcare workers. Dental practice currently is restricted to provision of emergency dental care whereas, many hospitals have also cancelled elective procedures to save finances for COVID-19 treatment which is expensive and unpredictable. In addition, healthcare workers are also facing financial challenges in this difficult time. Competent authorities should step in to help dental practices, hospitals and healthcare workers in order to ensure the provision of all types of healthcare efficiently in these testing times and beyond.
The blackholic quantum
Authors: Rueda J. A. , Ruffini R. 
Published: April 2020

AbstractWe show that the high-energy emission of GRBs originates in the inner engine: a Kerr black hole (BH) surrounded by matter and a magnetic field $$B_0$$B0. It radiates a sequence of discrete events of particle acceleration, each of energy $${{\mathscr {E}}} = \hbar \,\varOmega _{\mathrm{eff}}$$E=ħΩeff, the blackholic quantum, where $$\varOmega _{\mathrm{eff}} =4(m_{\mathrm{Pl}}/m_n)^8(c\,a/G\,M)(B_0^2/\rho _\mathrm{Pl})\varOmega _+$$Ωeff=4(mPl/mn)8(ca/GM)(B02/ρPl)Ω+. Here M, $$a=J/M$$a=J/M, $$\varOmega _+=c^2\partial M/\partial J=(c^2/G)\,a/(2 M r_+)$$Ω+=c2∂M/∂J=(c2/G)a/(2Mr+) and $$r_+$$r+ are the BH mass, angular momentum per unit mass, angular velocity and horizon; $$m_n$$mn is the neutron mass, $$m_{\mathrm{Pl}}$$mPl, $$\lambda _{\mathrm{Pl}}=\hbar /(m_{\mathrm{Pl}}c)$$λPl=ħ/(mPlc) and $$\rho _{\mathrm{Pl}}=m_{\mathrm{Pl}}c^2/\lambda _{\mathrm{Pl}}^3$$ρPl=mPlc2/λPl3, are the Planck mass, length and energy density. Here and in the following use CGS-Gaussian units. The timescale of each process is $$\tau _{\mathrm{el}}\sim \varOmega _+^{-1}$$τel∼Ω+-1, along the rotation axis, while it is much shorter off-axis owing to energy losses such as synchrotron radiation. We show an analogy with the Zeeman and Stark effects, properly scaled from microphysics to macrophysics, that allows us to define the BH magneton, $$\mu _{\mathrm{BH}}=(m_{\mathrm{Pl}}/m_n)^4(c\,a/G\,M)e\,\hbar /(M c)$$μBH=(mPl/mn)4(ca/GM)eħ/(Mc). We give quantitative estimates for GRB 130427A adopting $$M=2.3~M_\odot $$M=2.3M⊙, $$c\, a/(G\,M)= 0.47$$ca/(GM)=0.47 and $$B_0= 3.5\times 10^{10}$$B0=3.5×1010 G. Each emitted quantum, $$\mathcal{E}\sim 10^{37}$$E∼1037 erg, extracts only $$10^{-16}$$10-16 times the BH rotational energy, guaranteeing that the process can be repeated for thousands of years. The inner engine can also work in AGN as we here exemplified for the supermassive BH at the center of M87.
SPARK
Authors: Jennings Trevor J. 
Published: April 2020

Level -Intermediate
SPARK is an annotated sub-language of Ada which is unambiguous and suitable for rigorous static analysis. It has been extensively used in industrial applications where safety and security are paramount, such as miltary aerospace, rail signaling, and high-grade cryptographic systems.
The design of SPARK aligns closely with rigorous engineering approaches such as PSP/TSP, Six- Sigma, and the principles of the Lean Engineering movement in taking a "zero tolerance" approach to defect reduction.
In this light, SPARK is far more than "just a programming language" - it offers a distinct engineering mindset and discipline for the development of high-assurance systems.
The tutorial, which is extracted from the four-day "Software Engineering with SPARK" course will cover: The rationale and design goals of SPARK, the core SPARK language, and SPARK analyses including information flow, exception freedom, and formal verification, and the impact of SPARK on software process. The tutorial will also cover the "Libre" release of the SPARK technology and the research topics that this opens, such as more advanced forms of analysis and proof, modelchecking, and language extensions.
Firepile
Authors: Nystrom Nathaniel , White Derek , Das Kishen 
Published: April 2020

Recent advances have enabled GPUs to be used as general-purpose parallel processors on commodity hardware for little cost. However, the ability to program these devices has not kept up with their performance. The programming model for GPUs has a number of restrictions that make it difficult to program. For example, software running on the GPU cannot perform dynamic memory allocation, requiring the programmer to pre-allocate all memory the GPU might use. To achieve good performance, GPU programmers must also be aware of how data is moved between host and GPU memory and between the different levels of the GPU memory hierarchy.
We describe Firepile, a library for GPU programming in Scala. The library enables a subset of Scala to be executed on the GPU. Code trees can be created from run-time function values, which can then be analyzed and transformed to generate GPU code. A key property of this mechanism is that it is modular: unlike with other meta-programming constructs, the use of code trees need not be exposed in the library interface. Code trees are general and can be used by library writers in other application domains. Our experiments show Firepile users can achieve performance comparable to C code targeted to the GPU with shorter, simpler, and easier-to-understand code.
Leading-edge ada verification technologies
Authors: Kanig Johannes 
Published: April 2020

We give a hands-on introduction to the tools GNATtest and GNATprove, both developed at AdaCore in the Hi-Lite research project. They allow to do verification of Ada 2012 contracts through testing and formal verification, and also allow a combination of the results of both tools.
The tutorial will contain a very short introduction to Ada 2012, and attendees will write a small example on which they can play with GNATtest to develop test cases, and GNATprove to do some formal verification.
Tutorial overview
Authors: Nilsen Kelvin 
Published: April 2020

In spite of the high-level abstraction benefits of automatic tracing garbage collection, current prevailing sentiment within the safety certification community is that a simpler memory model is required for the most rigorous levels of software safety certification. Thus, the draft JSR-302 specification for safety critical Java relies on scope-based memory allocation rather than tracing garbage collection. The scoped memory model for JSR-302 is a simplification of the RTSJ model. JSR-302 enforces a strict hierarchy of scopes and distinguishes private scopes, which can be seen only by one thread, from mission scopes, which can be accessed by all the threads that comprise a mission, including threads running within inner-nested sub-missions. The hierarchical memory structure allows implementations to guarantee the absence of memory fragmentation for scope management, unlike the Real-Time Specification for Java from which the JSR-302 specification was derived.
In the absence of block structure, it is more difficult in Java to safely manage references to stack-allocated objects than in Ada. While the simplified hierarchical management of scoped memory that is part of JSR-302 addresses memory fragmentation concerns, it does not guarantee the absence of dangling pointers. As with the Real-Time Specification for Java, JSR-302 requires a run-time check to enforce that no reference assignment creates a relationship whereby an outer-nested object is allowed to point to an inner-nested object. This rule assures the absence of dangling pointers, but it introduces a different problem: every assignment to a reference field must be accompanied by a run-time check to validate the appropriate scope nesting relationship. This run-time check will throw a run-time exception if the assignment is deemed inappropriate.
The safety certification evidence for a given safety-critical Java program must therefore include an argument for every reference assignment that it will not cause the program to abort with a run-time exception. Furthermore, the certification evidence must prove that sufficient memory is available to reliably execute each safety-critical task in the system.
This tutorial provides an overview of dynamic memory management in Safety Critical Java and describes two annotation systems that have been designed to support static (compile-time) enforcement of memory safety properties. The first annotation system is described in an appendix to the draft JSR-302 standard. This relatively simple annotation system, which is not considered normative, serves to demonstrate that memory safety can be statically proven without requiring extensive annotations throughout existing library code. The second annotation system is the system implemented in Perc Pico. This annotation system, which is much richer than the draft JSR-302 annotation, has been in experimental use for over five years. During that time, tens of thousands of lines of experimental application code have been developed, with the experience motivating a variety of refinements to the original design.
An EDSL approach to high performance Haskell programming
Authors: Ankner Johan , Svenningsson Josef David 
Published: April 2020

This paper argues for a new methodology for writing high performance Haskell programs by using Embedded Domain Specific Languages.
We exemplify the methodology by describing a complete library, meta-repa, which is a reimplementation of parts of the repa library. The paper describes the implementation of meta-repa and contrasts it with the standard approach to writing high performance libraries. We conclude that even though the embedded language approach has an initial cost of defining the language and some syntactic overhead it gives a more tailored programming model, stronger performance guarantees, better control over optimizations, simpler implementation of fusion and inlining and allows for moving type level programming down to value level programming in some cases. We also provide benchmarks showing that meta-repa is as fast, or faster, than repa.
Furthermore, meta-repa also includes push arrays and we demonstrate their usefulness for writing certain high performance kernels such as FFT.
CakeML
Authors: Kumar Ramana , Myreen Magnus O. , Norrish Michael , Owens Scott 
Published: April 2020

We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.
Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover.
From parametricity to conservation laws, via Noether's theorem
Authors: Atkey Robert 
Published: April 2020

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds' theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields "free" theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy is by Noether's theorem a consequence of a system's invariance under time-shifting.
In this paper, we link Reynolds' relational parametricity with Noether's theorem for deriving conserved quantities. We propose an extension of System F$\omega$ with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of our extension of F$\omega$, that relational parametricity is enough to satisfy the hypotheses of Noether's theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.
A trusted mechanised JavaScript specification
Authors: Bodin Martin , Chargueraud Arthur , Filaretti Daniele , Gardner Philippa , Maffeis Sergio , Naudziuniene Daiva , Schmitt Alan , Smith Gareth 
Published: April 2020

JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
We present JSCert, a formalisation of the current ECMA standard in the Coq proof assistant, and JSRef, a reference interpreter for JavaScript extracted from Coq to OCaml. We give a Coq proof that JSRef is correct with respect to JSCert and assess JSRef using test262, the ECMA conformance test suite. Our methodology ensures that JSCert is a comparatively accurate formulation of the English standard, which will only improve as time goes on. We have demonstrated that modern techniques of mechanised specification can handle the complexity of JavaScript.
Profiling for laziness
Authors: Chang Stephen , Felleisen Matthias 
Published: April 2020

While many programmers appreciate the benefits of lazy programming at an abstract level, determining which parts of a concrete program to evaluate lazily poses a significant challenge for most of them. Over the past thirty years, experts have published numerous papers on the problem, but developing this level of expertise requires a significant amount of experience.
We present a profiling-based technique that captures and automates this expertise for the insertion of laziness annotations into strict programs. To make this idea precise, we show how to equip a formal semantics with a metric that measures waste in an evaluation. Then we explain how to implement this metric as a dynamic profiling tool that suggests where to insert laziness into a program. Finally, we present evidence that our profiler's suggestions either match or improve on an expert's use of laziness in a range of real-world applications.
Gradual typing embedded securely in JavaScript
Authors: Swamy Nikhil , Fournet Cedric , Rastogi Aseem , Bhargavan Karthikeyan , Chen Juan , Strub Pierre-Yves , Bierman Gavin 
Published: April 2020

JavaScript's flexible semantics makes writing correct code hard and writing secure code extremely difficult. To address the former problem, various forms of gradual typing have been proposed, such as Closure and TypeScript. However, supporting all common programming idioms is not easy; for example, TypeScript deliberately gives up type soundness for programming convenience. In this paper, we propose a gradual type system and implementation techniques that provide important safety and security guarantees.
We present TS# , a gradual type system and source-to-source compiler for JavaScript. In contrast to prior gradual type systems, TS# features full runtime reflection over three kinds of types: (1) simple types for higher-order functions, recursive datatypes and dictionary-based extensible records; (2) the type any, for dynamically type-safe TS# expressions; and (3) the type un, for untrusted, potentially malicious JavaScript contexts in which TS# is embedded. After type-checking, the compiler instruments the program with various checks to ensure the type safety of TS# despite its interactions with arbitrary JavaScript contexts, which are free to use eval, stack walks, prototype customizations, and other offensive features. The proof of our main theorem employs a form of type-preserving compilation, wherein we prove all the runtime invariants of the translation of TS# to JavaScript by showing that translated programs are well-typed in JS# , a previously proposed dependently typed language for proving functional correctness of JavaScript programs.
We describe a prototype compiler, a secure runtime, and sample applications for TS#. Our examples illustrate how web security patterns that developers currently program in JavaScript (with much difficulty and still with dubious results) can instead be programmed naturally in TS#, retaining a flavor of idiomatic JavaScript, while providing strong safety guarantees by virtue of typing.
All about the with statement in JavaScript
Authors: Park Changhee , Lee Hongki , Ryu Sukyoung 
Published: April 2020

The with statement in JavaScript makes static analysis of JavaScript applications difficult by introducing a new scope at run time and thus invalidating lexical scoping. Therefore, many static approaches to JavaScript program analysis and the strict mode of ECMAScript 5 simply disallow the with statement. To justify exclusion of the with statement, we should better understand the actual usage patterns of the with statement.
In this paper, we present the usage patterns of the with statement in real-world JavaScript applications currently used in the 898 most popular web sites. We investigate whether we can rewrite the with statements in each pattern to other statements not using the with statement. We show that we can rewrite all the static occurrences of the with statement that do not have any dynamic code generating functions. Even though the rewriting process is not applicable to any dynamically generated with statements, our results are still promising. Because all the static approaches that disallow the with statement also disallow dynamic code generation, such static approaches can allow the with statement using our rewriting process. We formally present our rewriting strategy, provide its implementation, and show its faithfulness using extensive testing. We believe that removing with statements will simplify JavaScript program analysis designs without considering dynamic scope introduction while imposing fewer syntactic restrictions.
Differential Equation Invariance Axiomatization
Authors: Platzer André , Tan Yong Kiam 
Published: April 2020

This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the proof-theoretical counterpart of dark matter. They create a new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis.
An extended axiomatization with existence and uniqueness axioms is complete for all local progress properties, and, with a real induction axiom, is complete for all semianalytic invariants. This parsimonious axiomatization serves as the logical foundation for reasoning about invariants of differential equations. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case.