bluuebunny/crossref_metadata_2025_split huggingface dataset:
Characteristic slip distribution and earthquake recurrence along the eastern Altyn Tagh fault revealed by high-resolution topographic data
Authors: Kang Wenjun , Xu Xiwei , Oskin Michael E. , Yu Guihua , Luo Jiahong , Chen Guihua , Luo Hao , Sun Xinzhe , Wu Xiyan 
Published: December 2019

AbstractThe seismic cycle model is roughly constrained by limited offset data sets from the eastern Altyn Tagh fault with a low slip rate. The recent availability of high-resolution topographic data from the eastern Altyn Tagh fault provides an opportunity to obtain distinctly improved quantitative, dense measurements of fault offsets. In this paper, we used airborne light detection and ranging data and unmanned aircraft vehicle photogrammetry to evaluate fault offsets. To better constrain the large earthquake recurrence model, we acquired dense data sets of fault displacements using the LaDiCaoz_v2.1 software. A total of 321 offset measurements below 30 m highlight two new observations: (1) surface-slip of the most recent earthquake and multiple events exhibit both short-wavelength (m-scale) and long-wavelength (km-scale) variability; and (2) synthesis of offset frequency analysis and coefficient of variation indicate regular slip events with ∼6 m slip increment on fault segments to the west of the Shulehe triple junction. The distribution of offsets and paleoseismological data reveal that the eastern Altyn Tagh fault exhibits characteristic slip behavior, with the characteristic slip of ∼6 m and a recurrence period ranging from 1170 to 3790 years. Paleoearthquake recurrence intervals and slip increments yield mean horizontal slip-rate estimates of 2.1–2.6 mm/yr for fault segments to the west of the Shulehe triple junction. Assuming a 10 km rupture depth and a 30 GPa shear modulus, we estimated a characteristic slip event moment magnitude (Mw) of ∼7.6. Finally, we discuss the interaction mechanism between Altyn Tagh fault (strike fault) and the NW-trending thrust faults (reverse faults) that caused the sudden decrease of sinistral slip rate at the Shulehe and Subei triple junctions; our results support the eastward “lateral slip extrusion” model.
Einstein–Cartan–Dirac gravity with U(1) symmetry breaking
Authors: Cabral Francisco , Lobo Francisco S. N. , Rubiera-Garcia Diego 
Published: December 2019

AbstractEinstein–Cartan theory is an extension of the standard formulation of General Relativity where torsion (the antisymmetric part of the affine connection) is non-vanishing. Just as the space-time metric is sourced by the stress-energy tensor of the matter fields, torsion is sourced via the spin density tensor, whose physical effects become relevant at very high spin densities. In this work we introduce an extension of the Einstein–Cartan–Dirac theory with an electromagnetic (Maxwell) contribution minimally coupled to torsion. This contribution breaks the U(1) gauge symmetry, which is suggested by the possibility of a torsion-induced phase transition in the early Universe, yielding new physics in extreme (spin) density regimes. We obtain the generalized gravitational, electromagnetic and fermionic field equations for this theory, estimate the strength of the corrections, and discuss the corresponding phenomenology. In particular, we briefly address some astrophysical considerations regarding the relevance of the effects which might take place inside ultra-dense neutron stars with strong magnetic fields (magnetars).
The structure of clusters formed by Stockmayer supracolloidal magnetic polymers
Authors: Novak Ekaterina V. , Pyanzina Elena S. , Sánchez Pedro A. , Kantorovich Sofia S. 
Published: December 2019

Abstract.
Unlike Stockmayer fluids, that prove to undergo gas-liquid transition on cooling, the system of dipolar hard or soft spheres without any additional central attraction so far has not been shown to have a critical point. Instead, in the latter, one observes diverse self-assembly scenarios. Crosslinking dipolar soft spheres into supracolloidal magnetic polymer-like structures (SMPs) changes the self-assembly behaviour. Moreover, aggregation in systems of SMPs strongly depends on the constituent topology. For Y- and X-shaped SMPs, under the same conditions in which dipolar hard spheres would form chains, the formation of very large loose gel-like clusters was observed (E. Novak et al., J. Mol. Liq. 271, 631 (2018)). In this work, using molecular dynamics simulations, we investigate the self-assembly in suspensions of four topologically different SMPs --chains, rings, X and Y-- whose monomers interact via Stockmayer potential. As expected, compact drop-like clusters are formed by SMPs in all cases if the central isotropic attraction is introduced, however, their shape and internal structure turn out to depend on the SMPs topology.

Graphical abstract
Microstructure and mechanical properties of high strength TMCP steel hybrid disk laser-MAG welded joint
Authors: Lei Zheng , Zhu Zongtao , Yang Xiaoyi , Jiang Yishuai , Chen Hui 
Published: December 2019

Hybrid laser-arc welding (HLAW) was carried out on high strength thermo-mechanical controlled process (TMCP) steel of 14 mm thickness using single-pass welding (SPW) and multi-pass welding (MPW) processes. Well-formed weld joints with good performance were successfully obtained. The results showed that the microstructure of weld was pre-eutectoid ferrite, acicular ferrite and some granular bainite. There were mainly lath bainite, granular bainite and acicular ferrite in the heat-affected zone. The grain sizes of SPW were thicker than MPW, and the bainite content of MPW was higher than SPW. The average hardness value of the fusion zone was lower than that of the Heat affected zone, but higher than that of the base material. The weld was divided into upper arc domain zone (ADZ) and lower laser domain zone (LDZ). The ADZ was harder than the LDZ. The average absorbed energy of SPW and MPW in the fusion zone at −40[Formula: see text]C was 125.5 and 92 J/cm2, respectively. The influences of microstructure on impact toughness were summarized by analyzing the hardness distribution and microstructure of the welded joint. The brittle transition temperatures of the two processes obtained by the energy criterion and the morphology criterion were close to each other.
Design of DQPSK Demodulator for Implantable Biomedical Devices
Authors: Garg Vaibhav , Kandpal Kavindra 
Published: December 2019

Implantable biomedical devices (IBDs) play a vital role in today’s healthcare industry. Such applications demand high data rate, low power and small-sized demodulators. This work presents a simple small-sized low-power architecture for differential quadrature phase shift keying (DQPSK) demodulator for these devices. The proposed circuitry is designed in UMC 90-nm CMOS technology and occupies a layout area of 0.015[Formula: see text]mm2. It is operated at 1-V supply voltage with a power consumption of 405[Formula: see text][Formula: see text]W. The carrier frequency is 10[Formula: see text]MHz and the obtained data rate is 20[Formula: see text]Mbps. Hence it exhibits a high data-rate-to-carrier-frequency (DRCF) ratio of 200% making it ideal for IBDs.
Dependent type systems as macros
Authors: Chang Stephen , Ballantyne Michael , Turner Milo , Bowman William J. 
Published: December 2019

We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages.
With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions.
Or they may create entirely new DSLs whose dependent type ``power'' is tailored to a specific domain.
Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs.
This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.
Complexity and information in invariant inference
Authors: Feldman Yotam M. Y. , Immerman Neil , Sagiv Mooly , Shoham Sharon 
Published: December 2019

This paper addresses the complexity of SAT-based invariant inference, a prominent approach to safety verification. We consider the problem of inferring an inductive invariant of polynomial length given a transition system and a safety property. We analyze the complexity of this problem in a black-box model, called the Hoare-query model, which is general enough to capture algorithms such as IC3/PDR and its variants. An algorithm in this model learns about the system's reachable states by querying the validity of Hoare triples.
We show that in general an algorithm in the Hoare-query model requires an exponential number of queries. Our lower bound is information-theoretic and applies even to computationally unrestricted algorithms, showing that no choice of generalization from the partial information obtained in a polynomial number of Hoare queries can lead to an efficient invariant inference procedure in this class.
We then show, for the first time, that by utilizing rich Hoare queries, as done in PDR, inference can be exponentially more efficient than approaches such as ICE learning, which only utilize inductiveness checks of candidates. We do so by constructing a class of transition systems for which a simple version of PDR with a single frame infers invariants in a polynomial number of queries, whereas every algorithm using only inductiveness checks and counterexamples requires an exponential number of queries.
Our results also shed light on connections and differences with the classical theory of exact concept learning with queries, and imply that learning from counterexamples to induction is harder than classical exact learning from labeled examples. This demonstrates that the convergence rate of Counterexample-Guided Inductive Synthesis depends on the form of counterexamples.
The weak call-by-value λ-calculus is reasonable for both time and space
Authors: Forster Yannick , Kunze Fabian , Roth Marc 
Published: December 2019

We study the weak call-by-value λ-calculus as a model for computational complexity theory and establish the natural measures for time and space — the number of beta-reduction steps and the size of the largest term in a computation — as reasonable measures with respect to the invariance thesis of Slot and van Emde Boas from 1984. More precisely, we show that, using those measures, Turing machines and the weak call-by-value λ-calculus can simulate each other within a polynomial overhead in time and a constant factor overhead in space for all computations terminating in (encodings of) ”true” or ”false”. The simulation yields that standard complexity classes like
P
,
NP
,
PSPACE
, or
EXP
can be defined solely in terms of the λ-calculus, but does not cover sublinear time or space.

Note that our measures still have the well-known size explosion property, where the space measure of a computation can be exponentially bigger than its time measure. However, our result implies that this exponential gap disappears once complexity classes are considered instead of concrete computations.
We consider this result a first step towards a solution for the long-standing open problem of whether the natural measures for time and space of the λ-calculus are reasonable. Our proof for the weak call-by-value λ-calculus is the first proof of reasonability (including both time and space) for a functional language based on natural measures and enables the formal verification of complexity-theoretic proofs concerning complexity classes, both on paper and in proof assistants.

The proof idea relies on a hybrid of two simulation strategies of reductions in the weak call-by-value λ-calculus by Turing machines, both of which are insufficient if taken alone. The first strategy is the most naive one in the sense that a reduction sequence is simulated precisely as given by the reduction rules; in particular, all substitutions are executed immediately. This simulation runs within a constant overhead in space, but the overhead in time might be exponential. The second strategy is heap-based and relies on structure sharing, similar to existing compilers of eager functional languages. This strategy only has a polynomial overhead in time, but the space consumption might require an additional factor of log
n
, which is essentially due to the size of the pointers required for this strategy. Our main contribution is the construction and verification of a space-aware interleaving of the two strategies, which is shown to yield both a constant overhead in space
and
a polynomial overhead in time.
Decomposition diversity with symmetric data and codata
Authors: Binder David , Jabs Julian , Skupin Ingo , Ostermann Klaus 
Published: December 2019

The expression problem describes a fundamental trade-off in program design: Should a program's primary decomposition be determined by the way its domain objects are constructed ("functional" decomposition), or by the way they are destructed ("object-oriented" decomposition)? We argue that programming languages should not force one of these decompositions on the programmer; rather, a programming language should support both ways of decomposing a program in a symmetric way, with an easy translation between these decompositions. However, current programming languages are usually not symmetric and hence make it unnecessarily hard to switch the decomposition.
We propose a language that is symmetric in this regard and allows a fully automatic translation between "functional" and "object-oriented" decomposition. We present a language with algebraic data types and pattern matching for "functional" decomposition and codata types and copattern matching for "object-oriented" decomposition, together with a bijective translation that turns a data type into a codata type ("destructorization") or vice versa ("constructorization"). We present the first symmetric programming language with support for local (co)pattern matching, which includes local anonymous function or object definitions, that allows an automatic translation as described above. We also present the first mechanical formalization of such a language and prove i) that the type system is sound, that the translations between data and codata types are ii) type-preserving, iii) behavior-preserving and iv) inverses of each other. We also extract a mechanically verified implementation from our formalization and have implemented an IDE with direct support for these translations.
PλωNK: functional probabilistic NetKAT
Authors: Vandenbroucke Alexander , Schrijvers Tom 
Published: December 2019

This work presents PλωNK, a functional probabilistic network programming language that extends Probabilistic NetKAT (PNK). Like PNK, it enables probabilistic modelling of network behaviour, by providing probabilistic choice and infinite iteration (to simulate looping network packets). Yet, unlike PNK, it also offers abstraction and higher-order functions to make programming much more convenient.
The formalisation of PλωNK is challenging for two reasons: Firstly, network programming induces multiple side effects (in particular, parallelism and probabilistic choice) which need to be carefully controlled in a functional setting. Our system uses an explicit syntax for thunks and sequencing which makes the interplay of these effects explicit. Secondly, measure theory, the standard domain for formalisations of (continuous) probablistic languages, does not admit higher-order functions. We address this by leveraging ω-Quasi Borel Spaces (ωQBSes), a recent advancement in the domain theory of probabilistic programming languages.
We believe that our work is not only useful for bringing abstraction to PNK, but that—as part of our contribution—we have developed the meta-theory for a probabilistic language that combines advanced features like higher-order functions, iteration and parallelism, which may inform similar meta-theoretic efforts.
Mechanized semantics and verified compilation for a dataflow synchronous language with reset
Authors: Bourke Timothy , Brun Lélio , Pouzet Marc 
Published: December 2019

Specifications based on block diagrams and state machines are used to design control software, especially in the certified development of safety-critical applications. Tools like SCADE Suite and Simulink/Stateflow are equipped with compilers that translate such specifications into executable code. They provide programming languages for composing functions over streams as typified by Dataflow Synchronous Languages like Lustre.
Recent work builds on CompCert to specify and verify a compiler for the core of Lustre in the Coq Interactive Theorem Prover. It formally links the stream-based semantics of the source language to the sequential memory manipulations of generated assembly code. We extend this work to treat a primitive for resetting subsystems. Our contributions include new semantic rules that are suitable for mechanized reasoning, a novel intermediate language for generating optimized code, and proofs of correctness for the associated compilation passes.
Graduality and parametricity: together again for the first time
Authors: New Max S. , Jamner Dustin , Ahmed Amal 
Published: December 2019

Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work.
We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.
Augmented example-based synthesis using relational perturbation properties
Authors: An Shengwei , Singh Rishabh , Misailovic Sasa , Samanta Roopsha 
Published: December 2019

Example-based specifications for program synthesis are inherently ambiguous and may cause synthesizers to generate programs that do not exhibit intended behavior on unseen inputs. Existing synthesis techniques attempt to address this problem by either placing a domain-specific syntactic bias on the hypothesis space or heavily relying on user feedback to help resolve ambiguity.
We present a new framework to address the ambiguity/generalizability problem in example-based synthesis. The key feature of our framework is that it places a semantic bias on the hypothesis space using "relational perturbation properties" that relate the perturbation/change in a program output to the perturbation/change in a program input. An example of such a property is permutation invariance: the program output does not change when the elements of the program input (array) are permuted. The framework is portable across multiple domains and synthesizers and is based on two core steps: (1) automatically augment the set of user-provided examples by "applying" relational perturbation properties and (2) use a generic example-based synthesizer to generate a program consistent with the augmented set of examples. Our framework can be instantiated with three different user interfaces, with varying degrees of user engagement to help infer relevant relational perturbation properties. This includes an interface in which the user only provides examples and our framework automatically infers relevant properties. We implement our framework in a tool SKETCHAX specialized to the SKETCH synthesizer and demonstrate that SKETCHAX is effective in significantly boosting the performance of SKETCH for all three user interfaces.
SyTeCi: automating contextual equivalence for higher-order programs with references
Authors: Jaber Guilhem 
Published: December 2019

We propose a framework to study contextual equivalence of programs written in a call-by-value functional language with local integer references. It reduces the problem of contextual equivalence to the problem of non-reachability in a transition system of memory configurations. This reduction is complete for recursion-free programs.
Restricting to programs that do not allocate references inside the body of functions, we encode this non-reachability problem as a set of constrained Horn clause that can then be checked for satisfiability automatically. Restricting furthermore to a language with finite data-types, we also get a new decidability result for contextual equivalence at any type.
Build your own SQL-on-Hadoop Query Engine
Authors: Scherzinger Stefanie 
Published: December 2019

This is a report on a course taught at OTH Regensburg in the summer term of 2018. The students in this course built their own SQL-on-Hadoop engine as a term project in just 8 weeks. miniHive is written in Python and compiles SQL queries into MapReduce workflows. These are then executed on Hadoop. miniHive performs generic query optimizations (selection and projection pushdown, or cost-based join reordering), as well as Map- Reduce-specific optimizations.
The course was taught in English, using a flipped classroom model. The course material was mainly compiled from third-party teaching videos. This report describes the course setup, the miniHive milestones, and gives a short review of the most successful student projects.