bluuebunny/crossref_metadata_2025_split huggingface dataset:
Relative bioavailability of a pediatric dispersible tablet and adult film‐coated tablet of macitentan in healthy volunteers
Authors: Sidharta Patricia N. , Štěpánová Radka , Globig Susanne , Ulč Ivan , Csonka Dénes 
Published: April 2020

AbstractTo compare the pharmacokinetic (PK) properties of the pediatric dispersible tablet formulation of macitentan and the adult film‐coated tablet formulation of macitentan in healthy subjects. A randomized, open‐label, single‐dose, two‐sequence, two‐period, crossover, Phase 1 study was conducted in 12 healthy adults. Subjects were randomized to one of the two possible treatment sequences A/B or B/A on Day 1 under fasted conditions. Treatment A was a single 10 mg dose of macitentan (film‐coated adult formulation) and Treatment B was a single 10 mg dose of macitentan, consisting of two 5 mg dispersible tablets (pediatric formulation). PK sampling over 216 hours was conducted, and PK parameters were derived using non‐compartmental methods. For macitentan, geometric means ratio of peak plasma concentrations (Cmax), plasma concentration‐time curve from zero to the time of the last quantifiable concentration (AUC0‐t), and plasma concentration‐time curve from zero to infinity (AUC0‐∞) were 1.140, 0.974, and 0.974, respectively. The corresponding 90% confidence intervals fell entirely within the referenced range of 0.8000 to 1.2500, which is used for evaluation of bioequivalence. These results indicate no significant differences between the pediatric dispersible tablet and the adult film‐coated tablet. Both formulations were well tolerated. The pediatric dispersible tablet is biocomparable to the adult film‐coated tablet formulation.
Intranasal epinephrine in dogs: Pharmacokinetic and heart rate effects
Authors: Dretchen Kenneth L. , Mesa Zack , Robben Matthew , Slade Desmond , Hill Scott , Croutch Claire , Kappeler Kyle , Mesa Michael 
Published: April 2020

AbstractEpinephrine is the standard of care for the treatment of severe allergy and anaphylaxis. Epinephrine is most often administered through the intramuscular (IM) route via autoinjector. The current study aimed to evaluate an alternative method of epinephrine treatment through intranasal (IN) delivery in dogs. The pharmacokinetic (PK) parameters of maximum plasma concentration (Cmax), time to reach maximum plasma concentration (Tmax), and area under the plasma concentration‐time curve from 0 to 90 minutes (AUC0–90) were observed after IN epinephrine (2, 3, 4, 5, 10, and 20 mg) and IM epinephrine via autoinjector (0.15 and 0.3 mg) for 90 minutes. Heart rate effects were measured after IN (2 and 5 mg) and IM (0.15 and 0.3 mg) epinephrine administration. IN epinephrine (5 mg) demonstrated significantly greater plasma epinephrine concentration at 1 minute as compared with IM epinephrine (0.3 mg) (1.68 ± 0.65 ng/mL vs 0.21 ± 0.08 ng/mL, P = .03). There were no significant differences in Cmax, Tmax, and AUC0–90 between 2‐mg IN and 0.15‐mg IM epinephrine or between 5‐mg IN and 0.3‐mg IM epinephrine. IN epinephrine reduced heart rate increases, as compared to IM epinephrine. IN and IM epinephrine were both well‐tolerated. Overall, IN epinephrine demonstrated advantages over IM epinephrine, including the rapid increase in plasma epinephrine and lack of increased heart rate over time.
Mechanism, kinetics, and environmental assessment of OH‐initiated transformation of CTDE in the atmosphere
Authors: Yang Yu‐Qi , Zhang Wei , Deng Ming‐Shuai , Pan Xiu‐Mei , Bai Feng‐Yang , Tan Lei 
Published: April 2020

AbstractThe transformation mechanism and kinetics of 2‐chloro‐1,1,2‐trifluoroethyl‐difluoromethyl‐ether (CTDE, CHF2OCF2CHFCl) triggered by OH radicals are studied by density‐functional theory methods and canonical variational transition state theory. The computational rate constant including small‐curvature tunneling correction is found to be in commendable agreement with the experimental data. Two hydrogen abstraction channels to form the alkyl radicals of C·F2OCF2CHFCl and CHF2OCF2C·FCl are observed, and the formation of CHF2OCF2C·FCl is found to be more favorable than C·F2OCF2CHFCl kinetically and thermodynamically. Subsequent evolution of CHF2OCF2C·FCl in the presence of NO and O2 indicates that the organic nitrate (CHF2OCF2CONO2FCl) is the stable product. The dechlorinate of alkoxy radical (CHF2OCF2C(O·)FCl) is the most favorable degradation channel, and the estimated ozone depletion potential for CTDE relative to chlorofluorocarbon‐11 is 0.0204, which could lead to ozone depletion as a consequence. The computed atmospheric lifetime for CTDE is found to be 3.69 years by considering the combined contributions from OH radicals and Cl atoms. The total radiative forcing and global warming potential of CTDE are, respectively, 0.547 W m−2 ppbv and 628.58 (100 years) at 298 K, suggesting that the contribution of CTDE to the greenhouse effect is moderate.
Longitudinal lung involvement of systemic lupus erythematosus‐related vasculitis and alveolar proteinosis‐like reaction
Authors: Suzuki Takahito , Enomoto Noriyuki , Horiike Yasuoki , Asada Kazuhiro , Shirai Toshihiro , Suda Takafumi 
Published: April 2020

AbstractA 44‐year‐old woman with no symptoms was referred to our hospital for thorough examination of consolidation opacity on her left lung, which was growing for four years. She was diagnosed with systemic lupus erythematosus (SLE) at the age of 35 years and had been treated with prednisolone 10 mg/day. Physical examination and bronchoscopy revealed no abnormality including microbiological tests. She underwent surgical resection of the lung lesion. Lung biopsy specimens showed aggregation of lymphocytes with germinal centres and collagen deposition. Vasculitis and pulmonary alveolar proteinosis (PAP)‐like reaction were also found. We diagnosed this lung opacity as an SLE‐related lung lesion with vasculitis and PAP‐like reaction. Lung involvement of SLE is scarce and long‐term lung vasculitis and PAP‐like reaction are extremely rare in patients with SLE. Clinicians should be aware of such SLE‐related lung consolidation opacity that comprises lung vasculitis and PAP‐like reaction.
A Meta‐Analysis on the Effects of Text Structure Instruction on Reading Comprehension in the Upper Elementary Grades
Authors: Bogaerds-Hazenberg Suzanne T.M. , Evers-Vermeul Jacqueline , van den Bergh Huub 
Published: April 2020

AbstractIn this meta‐analysis, the authors synthesize results from 44 (quasi‐)experimental studies on informational and narrative text structure interventions involving students in grades 4–6 in regular school settings. Findings show that text structure instruction had positive immediate effects on students’ reading comprehension but that effect sizes varied largely across outcome measures: questions (Hedges’g = 0.25), summarization (g = 0.57), recall (g = 0.37), and knowledge about text structure (g = 0.38). However, students who received text structure instruction no longer outperformed control groups at delayed posttests. Content‐related features, such as a focus on paragraph‐level structure, active construction of graphic organizers, and teaching rule‐based summarization techniques, moderated the effectiveness of text structure instruction, but these effects also varied across outcome measures. Instructional features moderated delayed effects: Interventions with opportunities for individual student practice resulted in higher delayed effects for comprehension questions. The authors argue that text structure instruction deserves a place in the primary school curriculum so the positive effects on reading will be maintained.
Reliance on science: Worldwide front‐page patent citations to scientific articles
Authors: Marx Matt , Fuegi Aaron 
Published: April 2020

AbstractResearch summaryTo what extent do firms rely on basic science in their R&D efforts? Several scholars have sought to answer this and related questions, but progress has been impeded by the difficulty of matching unstructured references in patents to published papers. We introduce an open‐access dataset of references from the front pages of patents granted worldwide to scientific papers published since 1800. Each patent‐paper linkage is assigned a confidence score, which is characterized in a random sample by false negatives versus false positives. All matches are available for download at http://relianceonscience.org. We outline several avenues for strategy research enabled by these new data.Managerial summaryTo what extent do firms rely on basic science in their R&D efforts? Several scholars have sought to answer this and related questions, but progress has been impeded by the difficulty of matching unstructured references in patents to published papers. We introduce an open‐access dataset of references from the front pages of patents granted worldwide to scientific papers published since 1800. Each patent‐paper linkage is assigned a confidence score, and we check a random sample of these confidence scores by hand in order to estimate both coverage (i.e., of the matches we should have found, what percentage did we find) and accuracy (i.e., of the matches we found, what percentage are correct). We outline several avenues for strategy research enabled by these new data.
Preparation of open‐tubular CEC column bonded with 6‐O‐monotosyl‐deoxy‐β‐cyclodextrin and its application in the enantioseparation of several related benzimidazoles
Authors: Fan Shitong , Guan Jin , Yan Feng , Zhang Dongxiang , Shi Shuang , Wang Silin 
Published: April 2020

AbstractA new chiral open‐tubular capillary electrochromatography column was prepared with 6‐O‐monotosyl‐deoxy‐β‐cyclodextrin as staionary phase by covalent immobilization on inner wall of a fused‐silica capillary. Preparation procedure of the open‐tubular column was investigated and resulting surface morphology was determined using scanning electron microscopy. Moreover, the enantiomeric separation performance of open‐tubular capillary electrochromatography column was evaluated by using several related benzimidazoles as model analytes, including pantoprazole, tenatoprazole, omeprazole, and lansoprazole. The primary factors affecting its separation efficiency, such as type, concentration, and pH of buffer, applied voltage were optimized. In the optimum conditions, the enantiomers of four analytes revealed high resolutions of 5.75–8.83. The relative standard deviation values for the migrated times and resolutions of the model analyte representing intraday, interday, and column‐to‐column were less than 1.8 and 1.3%, respectively. The chiral open‐tubular capillary electrochromatography column still had satisfactory separation performance after continuous use for 72 h or intermittent use for 3 months.
Trace-Relating Compiler Correctness and Secure Compilation
Authors: Abate Carmine , Blanco Roberto , Ciobâcă Ștefan , Durier Adrien , Garg Deepak , Hrițcu Cătălin , Patrignani Marco , Tanter Éric , Thibault Jérémy 
Published: April 2020

AbstractCompiler correctness is, in its simplest form, defined as the inclusion of the set of traces of the compiled program into the set of traces of the original program, which is equivalent to the preservation of all trace properties. Here traces collect, for instance, the externally observable events of each execution. This definition requires, however, the set of traces of the source and target languages to be exactly the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show in order to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side-channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many secure compilation definitions, which characterize the protection of a compiled program against linked adversarial code.
Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session Types
Authors: Jongmans Sung-Shik , Yoshida Nobuko 
Published: April 2020

AbstractA key open problem with multiparty session types (MPST) concerns their expressiveness: current MPST have inflexible choice, no existential quantification over participants, and limited parallel composition. This precludes many real protocols to be represented by MPST. To overcome these bottlenecks of MPST, we explore a new technique using weak bisimilarity between global types and endpoint types, which guarantees deadlock-freedom and absence of protocol violations. Based on a process algebraic framework, we present well-formed conditions for global types that guarantee weak bisimilarity between a global type and its endpoint types and prove their check is decidable. Our main practical result, obtained through benchmarks, is that our well-formedness conditions can be checked orders of magnitude faster than directly checking weak bisimilarity using a state-of-the-art model checker.
Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems
Authors: Krogh-Jespersen Morten , Timany Amin , Ohlenbusch Marit Edna , Gregersen Simon Oddershede , Birkedal Lars 
Published: April 2020

AbstractBuilding network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present , a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that is well-suited for both horizontal and vertical modular reasoning.
Semantic Foundations for Deterministic Dataflow and Stream Processing
Authors: Mamouras Konstantinos 
Published: April 2020

AbstractWe propose a denotational semantic framework for deterministic dataflow and stream processing that encompasses a variety of existing streaming models. Our proposal is based on the idea that data streams, stream transformations, and stream-processing programs should be classified using types. The type of a data stream is captured formally by a monoid, an algebraic structure with a distinguished binary operation and a unit. The elements of a monoid model the finite fragments of a stream, the binary operation represents the concatenation of stream fragments, and the unit is the empty fragment. Stream transformations are modeled using monotone functions on streams, which we call stream transductions. These functions can be implemented using abstract machines with a potentially infinite state space, which we call stream transducers. This abstract typed framework of stream transductions and transducers can be used to (1) verify the correctness of streaming computations, that is, that an implementation adheres to the desired behavior, (2) prove the soundness of optimizing transformations, e.g. for parallelization and distribution, and (3) inform the design of programming models and query languages for stream processing. In particular, we show that several useful combinators can be supported by the full class of stream transductions and transducers: serial composition, parallel composition, and feedback composition.
RustHorn: CHC-Based Verification for Rust Programs
Authors: Matsushita Yusuke , Tsukada Takeshi , Kobayashi Naoki 
Published: April 2020

AbstractReduction to the satisfiablility problem for constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. The current CHC-based methods for pointer-manipulating programs, however, are not very scalable. This paper proposes a novel translation of pointer-manipulating Rust programs into CHCs, which clears away pointers and heaps by leveraging ownership. We formalize the translation for a simplified core of Rust and prove its correctness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.
A First-Order Logic with Frames
Authors: Murali Adithya , Peña Lucas , Löding Christof , Madhusudan P. 
Published: April 2020

AbstractWe propose a novel logic, called Frame Logic (FL), that extends first-order logic (with recursive definitions) using a construct $$\textit{Sp}(\cdot )$$

Sp
(
·
)

that captures the implicit supports of formulas— the precise subset of the universe upon which their meaning depends. Using such supports, we formulate proof rules that facilitate frame reasoning elegantly when the underlying model undergoes change. We show that the logic is expressive by capturing several data-structures and also exhibit a translation from a precise fragment of separation logic to frame logic. Finally, we design a program logic based on frame logic for reasoning with programs that dynamically update heaps that facilitates local specifications and frame reasoning. This program logic consists of both localized proof rules as well as rules that derive the weakest tightest preconditions in FL.
Solving Program Sketches with Large Integer Values
Authors: Pan Rong , Hu Qinheping , Singh Rishabh , D’Antoni Loris 
Published: April 2020

AbstractProgram sketching is a program synthesis paradigm in which the programmer provides a partial program with holes and assertions. The goal of the synthesizer is to automatically find integer values for the holes so that the resulting program satisfies the assertions. The most popular sketching tool, Sketch, can efficiently solve complex program sketches, but uses an integer encoding that often performs poorly if the sketched program manipulates large integer values. In this paper, we propose a new solving technique that allows Sketch to handle large integer values while retaining its integer encoding. Our technique uses a result from number theory, the Chinese Remainder Theorem, to rewrite program sketches to only track the remainders of certain variable values with respect to several prime numbers. We prove that our transformation is sound and the encoding of the resulting programs are exponentially more succinct than existing Sketch encodings. We evaluate our technique on a variety of benchmarks manipulating large integer values. Our technique provides speedups against both existing Sketch solvers and can solve benchmarks that existing Sketch solvers cannot handle.
Higher-Ranked Annotation Polymorphic Dependency Analysis
Authors: Thorand Fabian , Hage Jurriaan 
Published: April 2020

AbstractThe precision of a static analysis can be improved by increasing the context-sensitivity of the analysis. In a type-based formulation of static analysis for functional languages this can be achieved by, e.g., introducing let-polyvariance or subtyping. In this paper we go one step further by defining a higher-ranked polyvariant type system so that even properties of lambda-bound identifiers can be generalized over. We do this for dependency analysis, a generic analysis that can be instantiated to a range of different analyses that in this way all can profit.We prove that our analysis is sound with respect to a call-by-name semantics and that it satisfies a so-called noninterference property. We provide a type reconstruction algorithm that we have proven to be terminating, and sound and complete with respect to its declarative specification. Our principled description can serve as a blueprint for making other analyses higher-ranked.
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
Authors: Toman John , Siqi Ren , Suenaga Kohei , Igarashi Atsushi , Kobayashi Naoki 
Published: April 2020

AbstractWe present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.
Higher-Order Spreadsheets with Spilled Arrays
Authors: Williams Jack , Joharizadeh Nima , Gordon Andrew D. , Sarkar Advait 
Published: April 2020

AbstractWe develop a theory for two recently-proposed spreadsheet mechanisms: gridlets allow for abstraction and reuse in spreadsheets, and build on spilled arrays, where an array value spills out of one cell into nearby cells. We present the first formal calculus of spreadsheets with spilled arrays. Since spilled arrays may collide, the semantics of spilling is an iterative process to determine which arrays spill successfully and which do not. Our first theorem is that this process converges deterministically. To model gridlets, we propose the grid calculus, a higher-order extension of our calculus of spilled arrays with primitives to treat spreadsheets as values. We define a semantics of gridlets as formulas in the grid calculus. Our second theorem shows the correctness of a remarkably direct encoding of the Abadi and Cardelli object calculus into the grid calculus. This result is the first rigorous analogy between spreadsheets and objects; it substantiates the intuition that gridlets are an object-oriented counterpart to functional programming extensions to spreadsheets, such as sheet-defined functions.
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
Authors: Costea Andreea , Zhu Amy , Polikarpova Nadia , Sergey Ilya 
Published: April 2020

AbstractIn program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user’s intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows.We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)–(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.