bluuebunny/crossref_metadata_2025_split huggingface dataset:
Orthologic with Axioms
Authors: Guilloud Simon , Kunčak Viktor 
Published: January 2024

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polynomial-time equivalence checking that is sound with respect to Boolean algebra semantics. We generalize ortholattice reasoning and obtain an algorithm for proving a larger class of classically valid formulas.
As the key result, we analyze a proof system for orthologic augmented with axioms. An important feature of the system is that it limits the number of formulas in a sequent to at most two, which makes the extension with axioms non-trivial. We show a generalized form of cut elimination for this system, which implies a sub-formula property. From there we derive a cubic-time algorithm for provability from axioms, or equivalently, for validity in finitely presented ortholattices. We further show that propositional resolution of width 5 proves all formulas provable in orthologic with axioms. We show that orthologic system subsumes resolution of width 2 and arbitrarily wide unit resolution and is complete for reasoning about generalizations of propositional Horn clauses.
Moving beyond ground axioms, we introduce effectively propositional orthologic (by analogy with EPR for classical logic), presenting its semantics as well as a sound and complete proof system. Our proof system implies the decidability of effectively propositional orthologic, as well as its fixed-parameter tractability for a bounded maximal number of variables in each axiom. As a special case, we obtain a generalization of Datalog with negation and disjunction.
Fusing Direct Manipulations into Functional Programs
Authors: Zhang Xing , Xie Ruifeng , Guo Guanchen , He Xiao , Zan Tao , Hu Zhenjiang 
Published: January 2024

Bidirectional live programming systems (BLP) enable developers to modify a program by directly manipulating the program output, so that the updated program can produce the manipulated output. One state-of-the-art approach to BLP systems is operation-based, which captures the developer's intention of program modifications by taking how the developer manipulates the output into account. The program modifications are usually hard coded for each direct manipulation in these BLP systems, which are difficult to extend. Moreover, to reflect the manipulations to the source program, these BLP systems trace the modified output to appropriate code fragments and perform corresponding code transformations. Accordingly, they require direct manipulation users be aware of the source code and how it is changed, making "direct" manipulation (on output) be "indirect".
In this paper, we resolve this problem by presenting a novel operation-based framework for bidirectional live programming, which can automatically fuse direct manipulations into the source code, thus supporting code-insensitive direct manipulations. Firstly, we design a simple but expressive delta language DM capable of expressing common direct manipulations for output values. Secondly, we present a fusion algorithm that propagates direct manipulations into the source functional programs and applies them to the constants whenever possible; otherwise, the algorithm embeds manipulations into the "proper positions" of programs. We prove the correctness of the fusion algorithm that the updated program executes to get the manipulated output. To demonstrate the expressiveness of DM and the effectiveness of our fusion algorithm, we have implemented FuseDM, a prototype SVG editor that supports GUI-based operations for direct manipulation, and successfully designed 14 benchmark examples starting from blank code using FuseDM.
Polyregular Functions on Unordered Trees of Bounded Height
Authors: Bojańczyk Mikołaj , Klin Bartek 
Published: January 2024

We consider injective first-order interpretations that input and output trees of bounded height. The corresponding functions have polynomial output size, since a first-order interpretation can use a
k
-tuple of input nodes to represent a single output node. We prove that the equivalence problem for such functions is decidable, i.e. ‍given two such interpretations, one can decide whether, for every input tree, the two output trees are isomorphic.

We also give a calculus of typed functions and combinators which derives exactly injective first-order interpretations for unordered trees of bounded height. The calculus is based on a type system, where the type constructors are products, coproducts and a monad of multisets. Thanks to our results about tree-to-tree interpretations, the equivalence problem is decidable for this calculus.
As an application, we show that the equivalence problem is decidable for first-order interpretations between classes of graphs that have bounded tree-depth. In all cases studied in this paper, first-order logic and MSO have the same expressive power, and hence all results apply also to MSO interpretations.
Validation of Modern JSON Schema: Formalization and Complexity
Authors: Attouche Lyes , Baazizi Mohamed-Amine , Colazzo Dario , Ghelli Giorgio , Sartiani Carlo , Scherzinger Stefanie 
Published: January 2024

JSON Schema is the de-facto standard schema language for JSON data. The language went through many minor revisions, but the most recent versions of the language, starting from Draft 2019-09, added two novel features, dynamic references and annotation-dependent validation, that change the evaluation model. Modern JSON Schema is the name used to indicate all versions from Draft 2019-09, which are characterized by these new features, while Classical JSON Schema is used to indicate the previous versions.
These new “modern” features make the schema language quite difficult to understand and have generated many discussions about the correct interpretation of their official specifications; for this reason, we undertook the task of their formalization. During this process, we also analyzed the complexity of data validation in Modern JSON Schema, with the idea of confirming the polynomial complexity of Classical JSON Schema validation, and we were surprised to discover a completely different truth: data validation, which is expected to be an extremely efficient process, acquires, with Modern JSON Schema features, a PSPACE complexity.
In this paper, we give the first formal description of Modern JSON Schema, which we have discussed with the community of JSON Schema tool developers, and which we consider a central contribution of this work. We then prove that its data validation problem is PSPACE-complete. We prove that the origin of the problem lies in the Draft 2020-12 version of dynamic references, and not in annotation-dependent validation. We study the schema and data complexities, showing that the problem is PSPACE-complete with respect to the schema size even with a fixed instance but is in P when the schema is fixed and only the instance size is allowed to vary. Finally, we run experiments that show that there are families of schemas where the difference in asymptotic complexity between dynamic and static references is extremely visible, even with small schemas.
Disentanglement with Futures, State, and Interaction
Authors: Arora Jatin , Muller Stefan K. , Acar Umut A. 
Published: January 2024

Recent work has proposed a memory property for parallel programs,
called disentanglement, and showed that it is pervasive in a variety
of programs, written in different languages, ranging from C/C++ to
Parallel ML, and showed that it can be exploited to improve
the performance of parallel functional programs.
All existing work on disentanglement, however, considers the
"fork/join" model for parallelism and does not apply to "futures",
the more powerful approach to parallelism.
This is not surprising:
fork/join parallel programs exhibit a reasonably strict dependency
structure (e.g., series-parallel DAGs), which disentanglement exploits.
In contrast, with futures, parallel computations become first-class
values of the language, and thus can be created, and passed between
functions calls or stored in memory, just like other ordinary values,
resulting in complex dependency structures, especially in the
presence of mutable state.
For example, parallel programs with futures can have deadlocks, which
is impossible with fork-join parallelism.
In this paper, we are interested in the theoretical question of
whether disentanglement may be extended beyond fork/join parallelism,
and specifically to futures.
We consider a functional language with futures, Input/Output (I/O),
and mutable state (references) and show that a broad range of programs
written in this language are disentangled.
We start by formalizing disentanglement for futures and proving that
purely functional programs written in this language are disentangled.
We then generalize this result in three directions.
First, we consider state (effects) and prove that stateful programs
are disentangled if they are race free.
Second, we show that race freedom is sufficient but not a necessary
condition and non-deterministic programs, e.g. those that use atomic
read-modify-operations and some non-deterministic combinators, may
also be disentangled.
Third, we prove that disentangled task-parallel programs written with
futures are free of deadlocks, which arise due to interactions between
state and the rich dependencies that can be expressed with futures.
Taken together, these results show that disentanglement generalizes to
parallel programs with futures and, thus, the benefits of disentanglement
may go well beyond fork-join parallelism.
Solving Infinite-State Games via Acceleration
Authors: Heim Philippe , Dimitrova Rayna 
Published: January 2024

Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games.
We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation.
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
Authors: Ackerman Nate , Freer Cameron E. , Kaddar Younesse , Karwowski Jacek , Moss Sean , Roy Daniel , Staton Sam , Yang Hongseok 
Published: January 2024

We study semantic models of probabilistic programming languages over graphs, and establish a connection to graphons from graph theory and combinatorics. We show that every well-behaved equational theory for our graph probabilistic programming language corresponds to a graphon, and conversely, every graphon arises in this way.
We provide three constructions for showing that every graphon arises from an equational theory. The first is an abstract construction, using Markov categories and monoidal indeterminates. The second and third are more concrete. The second is in terms of traditional measure theoretic probability, which covers 'black-and-white' graphons. The third is in terms of probability monads on the nominal sets of Gabbay and Pitts. Specifically, we use a variation of nominal sets induced by the theory of graphs, which covers Erdős-Rényi graphons. In this way, we build new models of graph probabilistic programming from graphons.
Total Type Error Localization and Recovery with Holes
Authors: Zhao Eric , Maroof Raef , Dukkipati Anand , Blinn Andrew , Pan Zhiyi , Omar Cyrus 
Published: January 2024

Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states.
The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e. the system identifies unfillable holes using a system of traced provenances, rather than localized in an ad hoc manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.
Explicit Effects and Effect Constraints in ReML
Authors: Elsman Martin 
Published: January 2024

An important aspect of building robust systems that execute on dedicated hardware and perhaps in constrained environments is to control and manage the effects performed by program code.We present ReML, a higher-order statically-typed functional language, which allows programmers to be explicit about the effects performed by program code and in particular effects related to memory management. Allowing programmers to be explicit about effects, the regions in which values reside, and the constraints under which code execute, makes programs robust to changes in the program source code and to compiler updates, including compiler optimisations.ReML is integrated with a polymorphic inference system that builds on top of region-inference, as it is implemented in the MLKit, a Standard ML compiler that uses region-based memory management as its primary memory management scheme.
A Novel Cross-Domain Recommendation with Evolution Learning
Authors: Chen Yi-Cheng , Lee Wang-Chien 
Published: January 2024

In this “info-plosion” era, recommendation systems (or recommenders) play a significant role in finding interesting items in the surge of online digital activities and e-commerce. Several techniques have been widely applied for recommendation systems, but the cold-start and sparsity problems remain a major challenge. The cold-start problem occurs when generating recommendations for new users and items without sufficient information. Sparsity refers to the problem of having a large amount of users and items but with few transactions or interactions. In this article, a novel cross-domain recommendation model, Cross-Domain Evolution Learning Recommendation (abbreviated as CD-ELR), is developed to communicate the information from different domains in order to tackle the cold-start and sparsity issues by integrating matrix factorization and recurrent neural network. We introduce an evolutionary concept to describe the preference variation of users over time. Furthermore, several optimization methods are developed for combining the domain features for precision recommendation. Experimental results show that CD-ELR outperforms existing state-of-the-art recommendation baselines. Finally, we conduct experiments on several real-world datasets to demonstrate the practicability of the proposed CD-ELR.
Lung Cancer in Ever- and Never-Smokers: Findings from Multi-Population GWAS Studies
Authors: Li Yafang , Xiao Xiangjun , Li Jianrong , Han Younghun , Cheng Chao , Fernandes Gail F. , Slewitzke Shannon E. , Rosenberg Susan M. , Zhu Meng , Byun Jinyoung , Bossé Yohan , McKay James D. , Albanes Demetrios , Lam Stephen , Tardon Adonina , Chen Chu , Bojesen Stig E. , Landi Maria T. , Johansson Mattias , Risch Angela , Bickeböller Heike , Wichmann H-Erich , Christiani David C. , Rennert Gad , Arnold Susanne M. , Goodman Gary E. , Field John K. , Davies Michael P.A. , Shete Sanjay , Marchand Loïc Le , Liu Geoffrey , Hung Rayjean J. , Andrew Angeline S. , Kiemeney Lambertus A. , Sun Ryan , Zienolddiny Shanbeh , Grankvist Kjell , Johansson Mikael , Caporaso Neil E. , Cox Angela , Hong Yun-Chul , Lazarus Philip , Schabath Matthew B. , Aldrich Melinda C. , Schwartz Ann G. , Gorlov Ivan , Purrington Kristen S. , Yang Ping , Liu Yanhong , Bailey-Wilson Joan E. , Pinney Susan M. , Mandal Diptasri , Willey James C. , Gaba Colette , Brennan Paul , Xia Jun , Shen Hongbing , Amos Christopher I. 
Published: January 2024

Abstract

Background:
Clinical, molecular, and genetic epidemiology studies displayed remarkable differences between ever- and never-smoking lung cancer.

Methods:
We conducted a stratified multi-population (European, East Asian, and African descent) association study on 44,823 ever-smokers and 20,074 never-smokers to identify novel variants that were missed in the non-stratified analysis. Functional analysis including expression quantitative trait loci (eQTL) colocalization and DNA damage assays, and annotation studies were conducted to evaluate the functional roles of the variants. We further evaluated the impact of smoking quantity on lung cancer risk for the variants associated with ever-smoking lung cancer.

Results:
Five novel independent loci, GABRA4, intergenic region 12q24.33, LRRC4C, LINC01088, and LCNL1 were identified with the association at two or three populations (P &lt; 5 × 10−8). Further functional analysis provided multiple lines of evidence suggesting the variants affect lung cancer risk through excessive DNA damage (GABRA4) or cis-regulation of gene expression (LCNL1). The risk of variants from 12 independent regions, including the well-known CHRNA5, associated with ever-smoking lung cancer was evaluated for never-smokers, light-smokers (packyear ≤ 20), and moderate-to-heavy-smokers (packyear &gt; 20). Different risk patterns were observed for the variants among the different groups by smoking behavior.

Conclusions:
We identified novel variants associated with lung cancer in only ever- or never-smoking groups that were missed by prior main-effect association studies.

Impact:
Our study highlights the genetic heterogeneity between ever- and never-smoking lung cancer and provides etiologic insights into the complicated genetic architecture of this deadly cancer.
Molecular and Pathologic Characterization of YAP1-Expressing Small Cell Lung Cancer Cell Lines Leads to Reclassification as SMARCA4-Deficient Malignancies
Authors: Ng Jin , Cai Ling , Girard Luc , Prall Owen W.J. , Rajan Neeha , Khoo Christine , Batrouney Ahida , Byrne David J. , Boyd Danielle K. , Kersbergen Ariena J. , Christie Michael , Minna John D. , Burr Marian L. , Sutherland Kate D. 
Published: January 2024

Abstract

Purpose:
The classification of small cell lung cancer (SCLC) into distinct molecular subtypes defined by ASCL1, NEUROD1, POU2F3, or YAP1 (SCLC-A, -N, -P, or -Y) expression, paves the way for a personalized treatment approach. However, the existence of a distinct YAP1-expressing SCLC subtype remains controversial.

Experimental Design:
To better understand YAP1-expressing SCLC, the mutational landscape of human SCLC cell lines was interrogated to identify pathogenic alterations unique to SCLC-Y. Xenograft tumors, generated from cell lines representing the four SCLC molecular subtypes, were evaluated by a panel of pathologists who routinely diagnose thoracic malignancies. Diagnoses were complemented by transcriptomic analysis of primary tumors and human cell line datasets. Protein expression profiles were validated in patient tumor tissue.

Results:
Unexpectedly, pathogenic mutations in SMARCA4 were identified in six of eight SCLC-Y cell lines and correlated with reduced SMARCA4 mRNA and protein expression. Pathologist evaluations revealed that SMARCA4-deficient SCLC-Y tumors exhibited features consistent with thoracic SMARCA4-deficient undifferentiated tumors (SMARCA4-UT). Similarly, the transcriptional profile SMARCA4-mutant SCLC-Y lines more closely resembled primary SMARCA4-UT, or SMARCA4-deficient non–small cell carcinoma, than SCLC. Furthermore, SMARCA4-UT patient samples were associated with a YAP1 transcriptional signature and exhibited strong YAP1 protein expression. Together, we found little evidence to support a diagnosis of SCLC for any of the YAP1-expressing cell lines originally used to define the SCLC-Y subtype.

Conclusions:
SMARCA4-mutant SCLC-Y cell lines exhibit characteristics consistent with SMARCA4-deficient malignancies rather than SCLC. Our findings suggest that, unlike ASCL1, NEUROD1, and POU2F3, YAP1 is not a subtype defining transcription factor in SCLC.
See related commentary by Rekhtman, p. 1708
La funzione anti-dialogica. Condizioni di incongruenza negli scambi di battute della poesia italiana del Novecento
Authors: Martini Giulia 
Published: January 2024

A análise das trocas presentes nos livros de poesia italiana do século XX mostrou um recurso horizontal ao expediente do dialogismo em chave disfuncional e pragmaticamente patológica, entre comunicações gagas, interrompidas, conflitantes ou sem sentido; o diálogo, em outras palavras, não se manifesta como uma adesão íntima a uma comunicação consonantal e recíproca, mas se refere ao mau funcionamento da própria comunicação. Do Canti di Castelvecchio (1903) de Giovanni Pascoli à Composita solvantur (1994) de Franco Fortini, os episódios líricos que contêm interações verbais parecem originar-se e remeter a uma 'função antidialógica': proliferam as conversas patológicas, as falhas posicionais, as interações conflituosas, as falhas pragmáticas; os falantes tendem a interagir de forma disfuncional e deslógica, abundam mal-entendidos, silêncios e reticências, falta cooperação, como se os atores fossem construídos para não se comunicar. A presente contribuição visa, assim, a enquadrar a função antidialógica que acabamos de esboçar através da comparação entre algumas amostras textuais e os principais módulos de incongruência pragmática, introduzidos primeiro a partir de uma classificação dos atos de fala, depois através do aprofundamento de um poema paradigmático.