bluuebunny/crossref_metadata_2025 huggingface dataset:
Data-driven lemma synthesis for interactive proofs
Authors: Sivaraman Aishwarya , Sanchez-Stern Alex , Chen Bretton , Lerner Sorin , Millstein Todd
Published: October 2022

Interactive proofs of theorems often require auxiliary helper lemmas to prove the desired theorem. Existing approaches for automatically synthesizing helper lemmas fall into two broad categories. Some approaches are goal-directed, producing lemmas specifically to help a user make progress from a given proof state, but they have limited expressiveness in terms of the lemmas that can be produced. Other approaches are highly expressive, able to generate arbitrary lemmas from a given grammar, but they are completely undirected and hence not amenable to interactive usage.

In this paper, we develop an approach to lemma synthesis that is both goal-directed and expressive.
The key novelty is a technique for reducing lemma synthesis to a data-driven program synthesis problem, whereby examples for synthesis are generated from the current proof state. We also describe a technique to systematically introduce new variables for lemma synthesis, as well as techniques for filtering and ranking candidate lemmas for presentation to the user. We implement these ideas in a tool called lfind, which can be run as a Coq tactic. In an evaluation on four benchmark suites, lfind produces useful lemmas in 68% of the cases where a human prover used a lemma to make progress. In these cases lfind synthesizes a lemma that either enables a fully automated proof of the original goal or that matches the human-provided lemma.
Synthesis-powered optimization of smart contracts via data type refactoring
Authors: Chen Yanju , Wang Yuepeng , Goyal Maruth , Dong James , Feng Yu , Dillig Işil
Published: October 2022

Since executing a smart contract on the Ethereum blockchain costs money (measured in
gas
), smart contract developers spend significant effort in reducing gas usage. In this paper, we propose a new technique for reducing the gas usage of smart contracts by changing the underlying data layout. Given a smart contract
P
and a type-level transformation, our method automatically synthesizes a new contract
P
′ that is functionally equivalent to
P
. Our approach provides a convenient DSL for expressing data type refactorings and employs program synthesis to generate the new version of the contract. We have implemented our approach in a tool called Solidare and demonstrate its capabilities on real-world smart contracts from Etherscan and GasStation. In particular, we show that our approach is effective at automating the desired data layout transformation and that it is useful for reducing gas usage of smart contracts that use rich data structures.
Specification-guided component-based synthesis from effectful libraries
Authors: Mishra Ashish , Jagannathan Suresh
Published: October 2022

Component-based synthesis seeks to build programs using the APIs provided by a set of libraries. Oftentimes, these APIs have effects, which make it challenging to reason about the correctness of potential synthesis candidates. This is because changes to global state made by effectful library procedures affect how they may be composed together, yielding an intractably large search space that can confound typical enumerative synthesis techniques. If the nature of these effects are exposed as part of their specification, however, deductive synthesis approaches can be used to help guide the search for components. In this paper, we present a new specification-guided synthesis procedure that uses Hoare-style pre- and post-conditions to express fine-grained effects of potential library component candidates to drive a bi-directional synthesis search strategy. The procedure alternates between a forward search process that seeks to build larger terms given an existing context but which is otherwise unaware of the actual goal, alongside a backward search mechanism that seeks terms consistent with the desired goal but which is otherwise unaware of the context from which these terms must be synthesized. To further improve efficiency and scalability, we integrate a conflict-driven learning procedure into the synthesis algorithm that provides a semantic characterization of previously encountered unsuccessful search paths that is used to prune the space of possible candidates as synthesis proceeds. We have implemented our ideas in a tool called and demonstrate its effectiveness on a number of challenging synthesis problems defined over OCaml libraries equipped with effectful specifications.
SigVM: enabling event-driven execution for truly decentralized smart contracts
Authors: Zhao Zihan , Beillahi Sidi Mohamed , Song Ryan , Cai Yuxi , Veneris Andreas , Long Fan
Published: October 2022

This paper presents SigVM, the first blockchain virtual machine that extends EVM to support an event-driven execution model, enabling developers to build truly decentralized smart contracts. Contracts in SigVM can emit signal events, on which other contracts can listen. Once an event is triggered, corresponding handler functions are automatically executed as signal transactions. We build an end-to-end blockchain platform SigChain and a contract language compiler SigSolid to realize the potential of SigVM. Experimental results show that our benchmark applications can be reimplemented with SigVM in a truly decentralized way, eliminating the dependency on centralized and unreliable mechanisms like off-chain relay servers. The development effort of reimplementing these contracts with SigVM is small, i.e., we modified on average 3.17% of the contract code. The runtime and the gas overhead of SigVM on these contracts is negligible.
Solo: a lightweight static analysis for differential privacy
Authors: Abuah Chiké , Darais David , Near Joseph P.
Published: October 2022

Existing approaches for statically enforcing differential privacy in higher order languages use either linear or relational refinement types. A barrier to adoption for these approaches is the lack of support for expressing these “fancy types” in mainstream programming languages. For example, no mainstream language supports relational refinement types, and although Rust and modern versions of Haskell both employ some linear typing techniques, they are inadequate for embedding enforcement of differential privacy, which requires “full” linear types. We propose a new type system that enforces differential privacy, avoids the use of linear and relational refinement types, and can be easily embedded in richly typed programming languages like Haskell. We demonstrate such an embedding in Haskell, demonstrate its expressiveness on case studies, and prove soundness of our type-based enforcement of differential privacy.
A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model
Authors: Blaudeau Clément , Liu Fengyun
Published: October 2022

An object under initialization does not fulfill its class specification yet and can be unsafe to
use as it may have uninitialized fields. It can sometimes be useful to call methods on such a
partially initialized object in order to compute a complex initial value, or to let the object
escape its constructor in order to create mutually recursive objects. However, inadvertent usage
of uninitialized fields can lead to run-time crashes. Those subtle programming errors are not
statically detected by most modern compilers.

While many other features of object-oriented programming languages have been thoroughly studied
over the years, object initialization lacks a simple, systematic, and principled
treatment. Building on the insights of previous work, we identify a set of four core principles
for safe initialization: monotonicity, authority, stackability, and scopability. We capture the
essence of the principles with a minimal calculus, Celsius, and show that the principles give rise
to a practical initialization system that strikes a balance between expressiveness and
simplicity. The meta-theory of the system is entirely mechanized using the Coq proof assistant. We
believe that our approach based on well-identified core principles sheds new light on the
underlying mechanisms ensuring safety and could serve as a basis for language design when faced
with similar challenges.
A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency
Authors: Frumin Dan , D’Osualdo Emanuele , van den Heuvel Bas , Pérez Jorge A.
Published: October 2022

The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O’Hearn and Pym’s Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new π-calculus with sessions, called πBI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of πBI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine λ-calculus; and a non-interference result for access of resources.
Oracle-free repair synthesis for floating-point programs
Authors: Zou Daming , Gu Yuchen , Shi Yuanfeng , Wang MingZhe , Xiong Yingfei , Su Zhendong
Published: October 2022

The floating-point representation provides widely-used data types (such as “float” and “double”) for modern numerical software. Numerical errors are inherent due to floating-point’s approximate nature, and pose an important, well-known challenge. It is nontrivial to fix/repair numerical code to reduce numerical errors — it requires eithernumerical expertise(for manual fixing) or high-precisionoracles(for automatic repair); both are difficult requirements. To tackle this challenge, this paper introduces aprincipled dynamic approachthat isfully automatedandoracle-freefor effectively repairing floating-point errors. The key of our approach is the novel notion ofmicro-structurethat characterizes structural patterns of floating-point errors. We leverage micro-structures’ statistical information on floating-point errors to effectively guide repair synthesis and validation. Compared with existing state-of-the-art repair approaches, our work is fully automatic and has the distinctive benefit of not relying on the difficult to obtain high-precision oracles. Evaluation results on 36 commonly-used numerical programs show that our approach is highly efficient and effective: (1) it is able to synthesize repairs instantaneously, and (2) versus the original programs, the repaired programs have orders of magnitude smaller floating-point errors, while having faster runtime performance.
Optimal heap limits for reducing browser memory use
Authors: Kirisame Marisa , Shenoy Pranav , Panchekha Pavel
Published: October 2022

Garbage-collected language runtimes carefully tune heap limits to reduce garbage collection time and memory usage. However, there's a trade-off: a lower heap limit reduces memory use but increases garbage collection time. Classic methods for setting heap limits include manually tuned heap limits and multiple-of-live-size rules of thumb, but it is not clear when one rule is better than another or how to compare them.

We address this problem with a new framework where heap limits are set for multiple heaps at once. Our key insight is that every heap limit rule induces a particular allocation of memory across multiple processes, and this allocation can be sub-optimal. We use our framework to derive an optimal "square-root" heap limit rule, which minimizes total memory usage for any amount of total garbage collection time. Paradoxically, the square-root heap limit rule achieves this coordination without communication: it allocates memory optimally across multiple heaps without requiring any communication between those heaps.

To demonstrate that this heap limit rule is effective, we prototype it for V8, the JavaScript runtime used in Google Chrome, Microsoft Edge, and other browsers, as well as in server-side frameworks like node.js and Deno. On real-world web pages, our prototype achieves reductions of approximately 16.0% of memory usage while keeping garbage collection time constant. On memory-intensive benchmarks, reductions of up to 30.0% of garbage collection time are possible with no change in total memory usage.
Scalable verification of GNN-based job schedulers
Authors: Wu Haoze , Barrett Clark , Sharif Mahmood , Narodytska Nina , Singh Gagandeep
Published: October 2022

Recently, Graph Neural Networks (GNNs) have been applied for scheduling jobs over clusters, achieving better performance than hand-crafted heuristics. Despite their impressive performance, concerns remain over whether these GNN-based job schedulers meet users’ expectations about other important properties, such as strategy-proofness, sharing incentive, and stability. In this work, we consider formal verification of GNN-based job schedulers. We address several domain-specific challenges such as networks that are deeper and specifications that are richer than those encountered when verifying image and NLP classifiers. We develop vegas, the first general framework for verifying both single-step and multi-step properties of these schedulers based on carefully designed algorithms that combine abstractions, refinements, solvers, and proof transfer. Our experimental results show that vegas achieves significant speed-up when verifying important properties of a state-of-the-art GNN-based scheduler compared to previous methods.
Fractional resources in unbounded separation logic
Authors: Dardinier Thibault , Müller Peter , Summers Alexander J.
Published: October 2022

Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction.

Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions.

In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.
A study of inline assembly in solidity smart contracts
Authors: Chaliasos Stefanos , Gervais Arthur , Livshits Benjamin
Published: October 2022

The Solidity programming language is the most widely used language for smart contract development. Improving smart contracts’ correctness, security, and performance has been the driving force for research in vulnerability detection, program analysis, and compiler techniques for Solidity. Similar to system-level languages such as C, Solidity enables the embedding of low-level code in programs, in the form of inline assembly code. Developers use inline assembly for low-level optimizations, extending the Solidity language through libraries, and using blockchain-specific opcodes only available through inline assembly. Nevertheless, inline assembly fragments are not well understood by an average developer and can introduce security threats as well as affect the optimizations that can be applied to programs by the compiler; it also significantly limits the effectiveness of source code static analyzers that operate on the Solidity level. A better understanding of how inline assembly is used in practice could in turn increase the performance, security, and support for inline assembly in Solidity.
This paper presents a large-scale quantitative study of the use of inline assembly in 6.8M smart contracts deployed on the Ethereum blockchain. We find that 23% of the analyzed smart contracts contain inline assembly code, and that the use of inline assembly has become more widespread over time. We further performed a manual qualitative analysis for identifying usage patterns of inline assembly in Solidity smart contracts. Our findings are intended to help practitioners understand when they should use inline assembly and guide developers of Solidity tools in prioritizing which parts of inline assembly to implement first. Finally, the insights of this study could be used to enhance the Solidity language, improve the Solidity compiler, and to open up new research directions by driving future researchers to build appropriate methods and techniques for replacing inline assembly in Solidity programs when there is no real necessity to use it.
Generic go to go: dictionary-passing, monomorphisation, and hybrid
Authors: Ellis Stephen , Zhu Shuofei , Yoshida Nobuko , Song Linhai
Published: October 2022

Go is a popular statically-typed industrial programming language. To aid the type safe reuse of code, the
recent Go release (Go 1.18) published early 2022 includes bounded parametric polymorphism via generic types.
Go 1.18 implements generic types using a combination of monomorphisation and call-graph based
dictionary-passing called hybrid. This hybrid approach can be viewed as an optimised form of monomorphisation that
statically generates specialised methods and types based on possible instantiations. A monolithic dictionary
supplements information lost during monomorphisation, and is structured according to the program’s call
graph. Unfortunately, the hybrid approach still suffers from code bloat, poor compilation speed, and limited
code coverage.

In this paper we propose and formalise a new non-specialising call-site based dictionary-passing translation.
Our call-site based translation creates individual dictionaries for each type parameter, with dictionary
construction occurring in place of instantiation, overcoming the limitations of hybrid. We prove it correct using
a novel and general bisimulation up to technique. To better understand how different generics translation
approaches work in practice, we benchmark five translators, Go 1.18, two existing monomorphisation
translators, our dictionary-passing translator, and an erasure translator. Our findings reveal several suggestions for
improvements for Go 1.18— specifically how to overcome the expressiveness limitations of generic Go and
improve compile time and compiled code size performance of Go 1.18.
Katara: synthesizing CRDTs with verified lifting
Authors: Laddad Shadaj , Power Conor , Milano Mae , Cheung Alvin , Hellerstein Joseph M.
Published: October 2022

Conflict-free replicated data types (CRDTs) are a promising tool for designing scalable, coordination-free distributed systems. However, constructing correct CRDTs is difficult, posing a challenge for even seasoned developers. As a result, CRDT development is still largely the domain of academics, with new designs often awaiting peer review and a manual proof of correctness. In this paper, we present Katara, a program synthesis-based system that takes sequential data type implementations and automatically synthesizes verified CRDT designs from them. Key to this process is a new formal definition of CRDT correctness that combines a reference sequential type with a lightweight ordering constraint that resolves conflicts between non-commutative operations. Our process follows the tradition of work in verified lifting, including an encoding of correctness into SMT logic using synthesized inductive invariants and hand-crafted grammars for the CRDT state and runtime. Katara is able to automatically synthesize CRDTs for a wide variety of scenarios, from reproducing classic CRDTs to synthesizing novel designs based on specifications in existing literature. Crucially, our synthesized CRDTs are fully, automatically verified, eliminating entire classes of common errors and reducing the process of producing a new CRDT from a painstaking paper proof of correctness to a lightweight specification.
Compilation of dynamic sparse tensor algebra
Authors: Chou Stephen , Amarasinghe Saman
Published: October 2022

Many applications, from social network graph analytics to control flow analysis, compute on sparse data that evolves over the course of program execution.
Such data can be represented as dynamic sparse tensors and efficiently stored in formats (data layouts) that utilize pointer-based data structures like block linked lists, binary search trees, B-trees, and C-trees among others.
These specialized formats support fast in-place modification and are thus better suited than traditional, array-based data structures like CSR for storing dynamic sparse tensors.
However, different dynamic sparse tensor formats have distinct benefits and drawbacks, and performing different computations on tensors that are stored in different formats can require vastly dissimilar code that are not straightforward to correctly implement and optimize.

This paper shows how a compiler can generate efficient code to compute tensor algebra operations on dynamic sparse tensors that may be stored in a wide range of disparate formats.
We propose a language for precisely specifying recursive, pointer-based data structures, and we show how this language can express many different dynamic data structures, including all the ones named above as well as many more.
We then describe how, given high-level specifications of such dynamic data structures, a compiler can emit code to efficiently access and compute on dynamic sparse tensors that are stored in the aforementioned data structures.

We evaluate our technique and find it generates efficient dynamic sparse tensor algebra kernels that have performance comparable to, if not better than, state-of-the-art libraries and frameworks such as PAM, Aspen, STINGER, and Terrace.
At the same time, our technique supports a wider range of tensor algebra operations---such as those that simultaneously compute with static and dynamic sparse tensors---than Aspen, STINGER, and Terrace, while also achieving significantly better performance than PAM for those same operations.
A case for DOT: theoretical foundations for objects with pattern matching and GADT-style reasoning
Authors: Boruch-Gruszecki Aleksander , Waśko Radosław , Xu Yichen , Parreaux Lionel
Published: October 2022

Many programming languages in the OO tradition now support pattern matching in some form. Historical examples include Scala and Ceylon, with the more recent additions of Java, Kotlin, TypeScript, and Flow. But pattern matching on generic class hierarchies currently results in puzzling type errors in most of these languages. Yet this combination of features occurs naturally in many scenarios, such as when manipulating typed ASTs. To support it properly, compilers needs to implement a form of subtyping reconstruction: the ability to reconstruct subtyping information uncovered at runtime during pattern matching. We introduce cDOT, a new calculus in the family of Dependent Object Types (DOT) intended to serve as a formal foundation for subtyping reconstruction. Being descended from pDOT, itself a formal foundation for Scala, cDOT can be used to encode advanced object-oriented features such as generic inheritance, type constructor variance, F-bounded polymorphism, and first-class recursive modules. We demonstrate that subtyping reconstruction subsumes GADTs by encoding λ

2,
G
µ

, a classical constraint-based GADT calculus, into cDOT.
Taming transitive redundancy for context-free language reachability
Authors: Lei Yuxiang , Sui Yulei , Ding Shuo , Zhang Qirun
Published: October 2022

Given an edge-labeled graph, context-free language reachability (CFL-reachability) computes reachable node pairs by deriving new edges and adding them to the graph. The redundancy that limits the scalability of CFL-reachability manifests as redundant derivations, i.e., identical edges can be derived multiple times due to the many paths between two reachable nodes. We observe that most redundancy arises from the derivations involving transitive relations of reachable node pairs. Unfortunately, existing techniques for reducing redundancy in transitive-closure-based problems are either ineffective or inapplicable to identifying and eliminating redundant derivations during on-the-fly CFL-reachability solving.

This paper proposes a scalable yet precision-preserving approach to all-pairs CFL-reachability analysis by taming its transitive redundancy. Our key insight is that transitive relations are intrinsically ordered, and utilizing the order for edge derivation can avoid most redundancy. To address the challenges in determining the derivation order from the dynamically changed graph during CFL-reachability solving, we introduce a hybrid graph representation by combining spanning trees and adjacency lists, together with a dynamic construction algorithm. Based on this representation, we propose a fast and effective partially ordered algorithm POCR to boost the performance of CFL-reachability analysis by reducing its transitive redundancy during on-the-fly solving. Our experiments on context-sensitive value-flow analysis and field-sensitive alias analysis for C/C++ demonstrate the promising performance of POCR. On average, POCR eliminates 98.50% and 97.26% redundant derivations respectively for the value-flow and alias analysis, achieving speedups of 21.48× and 19.57× over the standard CFL-reachability algorithm. We also compare POCR with two recent open-source tools, Graspan (a CFL-reachability solver) and Soufflé (a Datalog engine). The results demonstrate that POCR is over 3.67× faster than Graspan and Soufflé on average for both value-flow analysis and alias analysis.
Symbolic execution for randomized programs
Authors: Susag Zachary , Lahiri Sumit , Hsu Justin , Roy Subhajit
Published: October 2022

We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of
probabilistic symbolic variables
, which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the KLEE symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds’ algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against Psi, an exact probabilistic symbolic inference engine, and Storm, a probabilistic model checker, and show that our method significantly outperforms both tools.
Veracity: declarative multicore programming with commutativity
Authors: Chen Adam , Fathololumi Parisa , Koskinen Eric , Pincus Jared
Published: October 2022

There is an ongoing effort to provide programming abstractions that ease the burden of exploiting multicore hardware. Many programming abstractions (
e.g.
, concurrent objects, transactional memory, etc.) simplify matters, but still involve intricate engineering. We argue that some difficulty of multicore programming can be meliorated through a declarative programming style in which programmers directly express the independence of fragments of sequential programs.

In our proposed paradigm, programmers write programs in a familiar, sequential manner, with the added ability to explicitly express the conditions under which code fragments sequentially commute. Putting such commutativity conditions into source code offers a new entry point for a compiler to exploit the known connection between commutativity and parallelism. We give a semantics for the programmer’s sequential perspective and, under a correctness condition, find that a compiler-transformed parallel execution is equivalent to the sequential semantics. Serializability/linearizability are not the right fit for this condition, so we introduce scoped serializability and show how it can be enforced with lock synthesis techniques.

We next describe a technique for automatically verifying and synthesizing commute conditions via a new reduction from our commute blocks to logical specifications, upon which symbolic commutativity reasoning can be performed. We implemented our work in a new language called Veracity, implemented in Multicore OCaml. We show that commutativity conditions can be automatically generated across a variety of new benchmark programs, confirm the expectation that concurrency speedups can be seen as the computation increases, and apply our work to a small in-memory filesystem and an adaptation of a crowdfund blockchain smart contract.
Model-guided synthesis of inductive lemmas for FOL with least fixpoints
Authors: Murali Adithya , Peña Lucas , Blanchard Eion , Löding Christof , Madhusudan P.
Published: October 2022

Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.
Intrinsically-typed definitional interpreters à la carte
Authors: van der Rest Cas , Poulsen Casper Bach , Rouvoet Arjen , Visser Eelco , Mosses Peter
Published: October 2022

Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components:
language fragments
. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
High-level effect handlers in C++
Authors: Ghica Dan , Lindley Sam , Bravo Marcos Maroñas , Piróg Maciej
Published: October 2022

Effect handlers allow the programmer to implement computational effects, such as custom error handling, various forms of lightweight concurrency, and dynamic binding, inside the programming language. We introduce cpp-effects, a C++ library for effect handlers with a typed high-level, object-oriented interface. We demonstrate that effect handlers can be successfully applied in imperative systems programming languages with manual memory management. Through a collection of examples, we explore how to program effectively with effect handlers in C++, discuss the intricacies and challenges of the implementation, and show that despite its limitations, cpp-effects performance is competitive and in some cases even outperforms state-of-the-art approaches such as C++20 coroutines and the libmprompt library for multiprompt delimited control.
An Overview of Ada 202x
Authors: Cousins Jeff
Published: October 2022

Let us begin with why do we need another revision, when Ada has been used to successfully deliver so many projects around the world, indeed across the solar system?
First steps towards an IEEE 802.1AS clock for EDF scheduling in distributed real-time systems
Authors: Pérez Tijero Héctor , García Prieto Diego , Gutiérrez J. Javier
Published: October 2022

The EDF (Earliest Deadline First) scheduling policy can take advantage of the existence of a synchronization clock mechanism to reach higher utilizations in distributed real-time systems, as indicated by theoretical research. In this work, we give the first steps to enable the usage of EDF and a global clock in a distributed system. To this end, our proposal relies on Linux to provide the global clock and on a Real-Time Operating System (RTOS) to provide the global EDF policy. The objective is the evaluation of global EDF to verify to what extent the theoretical results are met.
LncRNA CARMN inhibits cervical cancer cell growth via the miR-92a-3p/BTG2/Wnt/β-catenin axis
Authors: Wang Lijun , Zhao Hu , Fang Ying , Yuan Bo , Guo Yilin , Wang Wuliang
Published: October 2022

Long noncoding RNA (lncRNA) cardiac mesoderm enhancer-associated noncoding RNA ( CARMN) is a newly discovered tumor-suppressor lncRNA in cancers. However, its role in cervical cancer (CC) remains elusive. This study was conducted to analyze the molecular mechanism of CARMN in CC cell growth and provide a novel theoretical basis for CC treatment. RT-qPCR and clinical analysis revealed that CARMN and B-cell translocation gene 2 ( BTG2) were downregulated, whereas miR-92a-3p was upregulated in CC tissues and cells and their expressions were correlated with clinicopathological characteristics and prognosis. MTT assay, flow cytometry, and Transwell assays revealed that CARMN overexpression reduced proliferation, migration, and invasion and increased apoptosis rate in CC cells. Mechanically, CARMN repressed miR-92a-3p to promote BTG2 transcription. Functional rescue assays revealed that miR-92a-3p overexpression or BTG2 downregulation reversed the inhibitory role of CARMN overexpression in CC cell growth. Western blot analysis elicited that Wnt3a and β-catenin were elevated in CC cells and CARMN blocked the Wnt/β-catenin signaling pathway via the miR-92a-3p/BTG2 axis. Overall, our findings demonstrated that CARMN repressed miR-92a-3p to upregulate BTG2 transcription and then blocked the Wnt/β-catenin signaling pathway, thereby suppressing CC cell growth.
Pyrroloquinoline Quinone Administration Alleviates Allergic Airway Inflammation in Mice by Regulating the JAK-STAT Signaling Pathway
Authors: Min Zhihui , Zhou Jiebai , Mao Ruolin , Cui Bo , Cheng Yunfeng , Chen Zhihong
Published: October 2022

The current asthma therapies are inadequate for many patients with severe asthma. Pyrroloquinoline quinone (PQQ) is a naturally-occurring redox cofactor and nutrient that can exert a multitude of physiological effects, including anti-inflammatory and antioxidative effects. We sought to explore the effects of PQQ on allergic airway inflammation and reveal the underlying mechanisms. In vitro, the effects of PQQ on the secretion of epithelial-derived cytokines by house dust mite- (HDM-) incubated 16-HBE cells and on the differentiation potential of CD4+ T cells were investigated. In vivo, PQQ was administered to mice with ovalbumin- (OVA-) induced asthma, and lung pathology and inflammatory cell infiltration were assessed. The changes in T cell subsets and signal transducers and activators of transcription (STATs) were evaluated by flow cytometry. Pretreatment with PQQ significantly decreased HDM-stimulated thymic stromal lymphopoietin (TSLP) production in a dose-dependent manner in 16-HBE cells and inhibited Th2 cell differentiation in vitro. Treatment with PQQ significantly reduced bronchoalveolar lavage fluid (BALF) inflammatory cell counts in the OVA-induced mouse model. PQQ administration also changed the secretion of IFN-γ and IL-4 as well as the percentages of Th1, Th2, Th17, and Treg cells in the peripheral blood and lung tissues, along with inhibition the phosphorylation of STAT1, STAT3, and STAT6 while promoting that of STAT4 in allergic airway inflammation model mice. PQQ can alleviate allergic airway inflammation in mice by improving the immune microenvironment and regulating the JAK-STAT signaling pathway. Our findings suggest that PQQ has great potential as a novel therapeutic agent for inflammatory diseases, including asthma.
Comparison of Characteristics of Breast Cancer Detected through Different Imaging Modalities in a Large Cohort of Hong Kong Chinese Women: Implication of Imaging Choice on Upcoming Local Screening Program
Authors: Chan Yik Shuen , Hung Wai Ka , Yuen Lok Wa , Chan Ho Yan Yolanda , Chu Chiu Wing Winnie , Cheung Polly Suk Yee
Published: October 2022

Background. We compared the clinico-radio-pathological characteristics of breast cancer detected through mammogram (MMG) and ultrasound (USG) and discuss the implication of the choice of imaging as the future direction of our recently launched local screening program. Methods. Retrospective study of 14613 Hong Kong Chinese female patients with histologically confirmed breast cancer registered in the Hong Kong Breast Cancer Registry between January 2006 and February 2020. Patients were classified into four groups based on the mode of breast cancer detection (detectable by both mammogram and ultrasound (MMG+/USG+), mammogram only (MMG+/USG−), ultrasound only (MMG−/USG+), or not detectable by either (MMG−/USG−). Characteristics of breast cancer detected were compared, including patient demographics, breast density on MMG, mode of presentation, tumour size, histological type, and staging. Types of mammographic abnormalities were also evaluated for MMG+ subgroups. Results. 85% of the cancers were detectable by MMG, while USG detected an additional 9%. MMG+/USG+ cancers were larger, more advanced in stage, often of symptomatic presentation, and commonly manifested as mammographic mass. MMG+/USG− cancers were more likely of asymptomatic presentation, manifested as microcalcifications, and of earlier stage and to be ductal carcinoma in situ. MMG−/USG+ cancers were more likely seen in young patients and those with denser breasts and more likely of symptomatic presentation. MMG−/USG− cancers were often smaller and found in denser breasts. Conclusion. Mammogram has a good detection rate of cancers in our local population. It has superiority in detecting early cancers by detecting microcalcifications. Our current study agrees that ultrasound is one of the key adjunct tools of breast cancer detection.
Perihelion Precessions of Inner Planets in Einstein’s Theory and Predicted Values for the Cosmological Constant
Authors: Salas S Alvaro H. , Castillo H Jairo E , Martınez H Lorenzo J.
Published: October 2022

In this paper, we obtain the approximate value of 42.9815 arcsec/century for Mercury’s perihelion precession by solving both numerically and analytically the nonlinear ordinary differential equation derived from the geodesic equation in Einstein’s Theory of Relativity. We also compare our result with known results, and we illustrate graphically the way Mercury’s perihelion moves. The results we obtained are applicable to any body that moves around the Sun. We give predictions about the value of the Cosmological Constant. Simple algebraic formulas allow to estimate perihelion shifts with high accuracy.
Swarming Computational Procedures for the Coronavirus‐Based Mathematical SEIR‐NDC Model
Authors: Suantai Suthep , Sabir Zulqurnain , Raja Muhammad Asif Zahoor , Cholamjiak Watcharaporn
Published: October 2022

The motive of the current work is related to solving the coronavirus‐based mathematical system of susceptible (S), exposed (E), infected (I), recovered (R), overall population (N), civic observation (D), and cumulative performance (C), called as SEIR‐NDC. The numerical solutions of the SEIR‐NDC model are presented by using the computational framework of artificial neural networks (ANNs) together with the swarming optimization procedures aided with the sequential quadratic programming. The swarming procedure based on the particle swarm optimization (PSO) works as a global search, while the sequential quadratic programming (SQP) is used as a local search algorithm. A merit function is constructed by using the nonlinear dynamics of the SEIR‐NDC mathematical system based on its 7 classes, and the optimization of the merit function is performed through the PSOSQP. The numerical expressions of system are accessible with the ANNs using the PSOSQP optimization with 30 variables. The correctness of the stochastic computing scheme performances is verified by using the comparison of the obtained performances of the mathematical SEIR‐NDC system and the reference Runge–Kutta scheme. Furthermore, the graphical illustrations of the performance indices, absolute error, and convergence curves are derived to validate the robustness of the proposed ANN‐PSOSQP approach for the mathematical SEIR‐NDC system.
An Optimization Model for the Student-to-Project Supervisor Assignment Problem-The Case of an Engineering Department
Authors: Ramotsisi Johnson , Kgomotso Mompoloki , Seboni Lone
Published: October 2022

Purpose. Empirical studies on the topic of assigning university project students to supervisors are currently underexplored. Such studies are critical to success of both the students and the university. Whilst extant research on this topic has contributed to an understanding of student assignments, what appears to be missing is application of a comprehensive framework to inform formulation and validation of a robust solution approach that takes account of both student and supervisor preferences, to optimize a real-life student-to-project supervisor assignment problem. Methodology. Questionnaire and interview surveys with project coordinators, project supervisors, head of department and students were conducted to identify factors surrounding the student-to-project supervisor assignment, through a case study approach in a university department offering engineering degree programs. This study not only develops a framework to understand an effective student-to-project supervisor assignment decision but also applies it in practice, through a case study in a University department offering engineering degree programs. An integer linear programming model was developed and implemented in an optimization software to optimize the student-to-project supervisor assignment, using data from the case study. Findings. Using OpenSolver, validated model results show improvements in matching both students and project supervisors’ preferences, whilst complying with supervisors’ workloads. These results also reveal an improvement in minimizing the project coordinator’s time in doing the assignment by introducing a standardized approach that concurrently considers all variables in a consistent manner. Originality. The contribution lies in: (1) development of a robust framework for student-to-supervisor assignments, (2) explicit consideration of contextual factors that recognize different assignment scenarios, (3) identification of feedback loops to recognize not only the need for continuous improvement in student-to-supervisor assignments but also links to performance in final year projects, (4) unique insights to guide project coordinators in relation to an efficient, effective, comprehensive, and standardized approach to the student-to-project supervisor assignment, and (5) a deeper understanding of a comprehensive range of factors that play a role in student-to-project supervisor assignments in higher education institutions.
Treatment Delays and Chance of Reperfusion Therapy in Patients with Acute Stroke: A Danish Nationwide Study
Authors: Mainz Jeppe , Andersen Grethe , Valentin Jan Brink , Gude Martin Faurholdt , Johnsen Søren Paaske
Published: October 2022

Introduction: We aimed to determine the treatment delay for ischemic stroke patients in Denmark. Methods: A nationwide register-based study on acute ischemic stroke patients admitted through emergency medical services. Treatment delay comprised patient, prehospital, and in-hospital delay. Analyses were stratified according to length of prehospital delay (<3 vs. ≥3 h). Results: A total of 5,356 ischemic stroke episodes were included. The median onset-to-door time was 187 min, and 2,405 (43%) arrived at the stroke unit within 3 h. Overall, the median patient delay was 115 min. For early arrival (n = 2,280), patient delay was 27 min compared to 437 min for late arrivals (n = 2,448). Median prehospital delay varied by 9 min between early- and late-arriving patients. Approximately 48% of the early-arriving patients compared to 9% of the late-arriving patients received i.v. thrombolysis. For thrombectomy, the numbers were 10% and 3%, respectively. This corresponded to an unadjusted relative risk (RR) of 0.18 (95% CI: 0.16–0.21) and adjusted (age, sex, cohabitation status, and stroke severity) RR of 0.20 (95% CI: 0.18–0.23) for i.v. thrombolysis when comparing patients arriving later than 3 h with patients arriving earlier. For thrombectomy, the unadjusted and adjusted RRs were 0.30 (95% CI: 0.23–0.39) and 0.40 (95% CI: 0.31–0.52), respectively. Conclusions: Patient delay remains the most important barrier for use of reperfusion therapy among acute ischemic stroke patients calling 1-1-2, whereas system delay seems independent of patient delay.