26,098 papers · page 98 of 1,305
Algebraic theories with dependency between sorts form the structural core of Martin-L\"of type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (co…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programming languages instead …
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods th…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pth…
Abstract elided by the publisher.
Abstract elided by the publisher.
Abstract Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operatio…
Abstract We present for the first time a supermartingale certificate for $$\omega $$ ω -regular specifications. We leverage the Robbins & Siegmund convergence theorem to characterize supermartingale certificates for the almost-sure acceptance of Streett conditions on general stoc…
Abstract We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the proble…