More Like this

1. Error Localization for Sequential Effect Systems

   https://doi.org/10.1007/978-3-031-44245-2_16  

   Gordon, Colin S.; Yun, Chaewon (October 2023, Static Analysis Symposium 2023)

   Hermenegildo, M.V. (Ed.)

   We describe a new concrete approach to giving predictable error locations for sequential (flow-sensitive) effect systems. Prior implementations of sequential effect systems rely on either computing a bottom-up effect and comparing it to a declaration (e.g., method annotation) or leaning on constraint-based type inference. These approaches do not necessarily report program locations that precisely indicate where a program may “go wrong” at runtime. Instead of relying on constraint solving, we draw on the notion of a residual from literature on ordered algebraic structures. Applying these to effect quantales (a large class of sequential effect systems) yields an implementation approach which accepts exactly the same program as an original effect quantale, but for effect-incorrect programs is guaranteed to fail type-checking with predictable error locations tied to evaluation order. We have implemented this idea in a generic effect system implementation framework for Java, and report on experiences applying effect systems from the literature and novel effect systems to Java programs. We find that the reported error locations with our technique are significantly closer to the program points that lead to failed effect checks. 

   more » « less
2. Layered and object-based game semantics

   https://doi.org/10.1145/3498703  

   Oliveira Vale, Arthur; Melliès, Paul-André; Shao, Zhong; Koenig, Jérémie; Stefanesco, Léo (January 2022, Proceedings of the ACM on Programming Languages)

   Large-scale software verification relies critically on the use of compositional languages, semantic models, specifications, and verification techniques. Recent work on certified abstraction layers synthesizes game semantics, the refinement calculus, and algebraic effects to enable the composition of heterogeneous components into larger certified systems. However, in existing models of certified abstraction layers, compositionality is restricted by the lack of encapsulation of state. In this paper, we present a novel game model for certified abstraction layers where the semantics of layer interfaces and implementations are defined solely based on their observable behaviors. Our key idea is to leverage Reddy's pioneer work on modeling the semantics of imperative languages not as functions on global states but as objects with their observable behaviors. We show that a layer interface can be modeled as an object type (i.e., a layer signature) plus an object strategy. A layer implementation is then essentially a regular map, in the sense of Reddy, from an object with the underlay signature to that with the overlay signature. A layer implementation is certified when its composition with the underlay object strategy implements the overlay object strategy. We also describe an extension that allows for non-determinism in layer interfaces. After formulating layer implementations as regular maps between object spaces, we move to concurrency and design a notion of concurrent object space, where sequential traces may be identified modulo permutation of independent operations. We show how to express protected shared object concurrency, and a ticket lock implementation, in a simple model based on regular maps between concurrent object spaces. 

   more » « less
3. The simplicial coalgebra of chains determines homotopy types rationally and one prime at a time

   https://doi.org/10.1090/tran/8579  

   Rivera, Manuel; Wierstra, Felix; Zeinalian, Mahmoud (January 2022, Transactions of the American Mathematical Society)

   We prove that the simplicial cocommutative coalgebra of singular chains on a connected topological space determines the homotopy type rationally and one prime at a time, without imposing any restriction on the fundamental group. In particular, the fundamental group and the homology groups with coefficients in arbitrary local systems of vector spaces are completely determined by the natural algebraic structure of the chains. The algebraic structure is presented as the class of the simplicial cocommutative coalgebra of chains under a notion of weak equivalence induced by a functor from coalgebras to algebras coined by Adams as the cobar construction. The fundamental group is determined by a quadratic equation on the zeroth homology of the cobar construction of the normalized chains which involves Steenrod’s chain homotopies for cocommutativity of the coproduct. The homology groups with local coefficients are modeled by an algebraic analog of the universal cover which is invariant under our notion of weak equivalence. We conjecture that the integral homotopy type is also determined by the simplicial coalgebra of integral chains, which we prove when the universal cover is of finite type. 

   more » « less
4. Equivariant Witt complexes and twisted topological Hochschild homology

   https://doi.org/10.1016/j.topol.2025.109444  

   Bohmann, Anna Marie; Gerhardt, Teena; Krulewski, Cameron; Petersen, Sarah; Yang, Lucy (May 2025, Topology and its Applications)

   The topological Hochschild homology of a ring (or ring spectrum) R is an S1-spectrum, and the fixed points of THH(R) for subgroups C_n of S1 have been widely studied due to their use in algebraic K-theory computations. Hesselholt and Madsen proved that the fixed points of topological Hochschild homology are closely related to Witt vectors. Further, they defined the notion of a Witt complex, and showed that it captures the algebraic structure of the homotopy groups of the fixed points of THH. Recent work defines a theory of twisted topological Hochschild homology for equivariant rings (or ring spectra) that builds upon Hill, Hopkins and Ravenel's work on equivariant norms. In this paper, we study the algebraic structure of the equivariant homotopy groups of twisted THH. In particular, drawing on the definition of equivariant Witt vectors by Blumberg, Gerhardt, Hill and Lawson, we define an equivariant Witt complex and prove that the equivariant homotopy of twisted THH has this structure. Our definition of equivariant Witt complexes contributes to a growing body of research in the subject of equivariant algebra. 

   more » « less
5. Concomitant Entanglement and Control Criticality Driven by Collective Measurements

   https://doi.org/10.1103/PRXQuantum.6.010351  

   Iadecola, Thomas; Wilson, Justin H; Pixley, JH (March 2025, PRX Quantum)

   Adaptive quantum circuits—where a quantum many-body state is controlled using measurements and conditional unitary operations—are a powerful paradigm for state preparation and quantum error-correction tasks. They can support two types of nonequilibrium quantum phase transitions: measurement-induced transitions between volume- and area-law-entangled steady states and control-induced transitions where the system falls into an absorbing state or, more generally, an orbit visiting several absorbing states. Within this context, nonlocal conditional operations can alter the critical properties of the two transitions and the topology of the phase diagram. Here, we consider the scenario where the measurements are , in order to engineer efficient control onto dynamical trajectories. Motivated by Rydberg-atom arrays, we consider a locally constrained model with global sublattice magnetization measurements and local correction operations to steer the system’s dynamics onto a many-body orbit with finite recurrence time. The model has a well-defined classical limit, which we leverage to aid our analysis of the control transition. As a function of the density of local correction operations, we find control and entanglement transitions with continuously varying critical exponents. For sufficiently high densities of local correction operations, we find that both transitions acquire a dynamical critical exponent $z<1$, reminiscent of criticality in long-range power-law interacting systems. At low correction densities, we find that the criticality reverts to a short-range nature with $z\gtrsim 1$. In the long-range regime, the control and entanglement transitions are indistinguishable to within the resolution of our finite-size numerics, while in the short-range regime we find evidence that the transitions become distinct. We conjecture that the effective long-range criticality mediated by collective measurements is essential in driving the two transitions together. Published by the American Physical Society2025 

   more » « less