Search for: All records

Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computation cost. Existing works either require manually annotating sharing, or rely on separation logic to reason about heaps of mutable cells. In this paper, we propose a bidirectional demand semantics that allows for extrinsic reasoning about the computation cost of lazy programs without relying on special program logics. To show the effectiveness of our approach, we apply the demand semantics to a variety of case studies including insertion sort, selection sort, Okasaki's banker's queue, and the implicit queue. We formally prove that the banker's queue and the implicit queue are both amortized and persistent using the Rocq Prover (formerly known as Coq). We also propose the reverse physicist's method, a novel variant of the classical physicist's method, which enables mechanized, modular and compositional reasoning about amortization and persistence with the demand semantics. 

Abstract Cured-in-place pipe (CIPP) technology is increasingly being utilized to repair aging and damaged pipes, however, there are concerns associated with the public health hazards of emissions. CIPP installation involves the manufacture of a new plastic composite pipe at the worksite and includes multiple variable components including resin material, curing methods, and operational conditions. We hypothesize styrene-based composite manufacturing emissions (CMEs) will induce greater pulmonary inflammatory responses and oxidative stress, as well as neurological toxicity compared with nonstyrene CMEs. Further, these CME-toxicological responses will be sex- and time-dependent. To test the hypothesis, representative CMEs were generated using a laboratory curing chamber and characterized using thermal desorption-gas chromatography-mass spectrometry and photoionization detector. Styrene was released during staying, isothermal curing, and cooling phases of the process and peaked during the cooling phase. Male and female C57BL6/J mice were utilized to examine alterations in pulmonary responses and neurotoxicity 1 day and 7 days following exposure to air (controls), nonstyrene-CMEs, or styrene-CMEs. Serum styrene metabolites were increased in mice exposed to styrene-CMEs. Metabolic and lipid profiling revealed alterations related to CIPP emissions that were resin-, time-, and sex-dependent. Exposure to styrene-CMEs resulted in an influx of lymphocytes in both sexes. Expression of inflammatory and oxidative stress markers, including Tnfα, Vcam1, Ccl2, Cxcl2, Il6, Cxcl1, Tgfβ1, Tgmt2, and Hmox1, displayed alterations following exposure to emissions. These changes in pulmonary and neurological markers of toxicity were dependent on resin type, sex, and time. Overall, this study demonstrates resin-specific differences in representative CMEs and alterations in toxicity endpoints, which can potentially inform safer utilization of composite manufacturing processes. 

Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation makes it hard to analyze a program's computational cost, either informally or formally. In this work, we present a novel and simple framework for formally reasoning about lazy computation costs based on a recent model of lazy evaluation: clairvoyant call-by-value. The key feature of our framework is its simplicity, as expressed by our definition of the clairvoyance monad. This monad is both simple to define (around 20 lines of Coq) and simple to reason about. We show that this monad can be effectively used to mechanically reason about the computational cost of lazy functional programs written in Coq. 

Abstract In Earth’s low atmosphere, hurricanes are destructive due to their great size, strong spiral winds with shears, and intense rain/precipitation. However, disturbances resembling hurricanes have not been detected in Earth’s upper atmosphere. Here, we report a long-lasting space hurricane in the polar ionosphere and magnetosphere during low solar and otherwise low geomagnetic activity. This hurricane shows strong circular horizontal plasma flow with shears, a nearly zero-flow center, and a coincident cyclone-shaped aurora caused by strong electron precipitation associated with intense upward magnetic field-aligned currents. Near the center, precipitating electrons were substantially accelerated to ~10 keV. The hurricane imparted large energy and momentum deposition into the ionosphere despite otherwise extremely quiet conditions. The observations and simulations reveal that the space hurricane is generated by steady high-latitude lobe magnetic reconnection and current continuity during a several hour period of northward interplanetary magnetic field and very low solar wind density and speed. 

Transactional objects combine the performance of classical concurrent objects with the high-level programmability of transactional memory. However, verifying the correctness of transactional objects is tricky, requiring reasoning simultaneously about classical concurrent objects, which guarantee the atomicity of individual methods—the property known as linearizability—and about software-transactional-memory libraries, which guarantee the atomicity of user-defined sequences of method calls—or serializability. We present a formal-verification framework called C4, built up from the familiar notion of linearizability and its compositional properties, that allows proof of both kinds of libraries, along with composition of theorems from both styles to prove correctness of applications or further libraries. We apply the framework in a significant case study, verifying a transactional set object built out of both classical and transactional components following the technique oftransactional predication; the proof is modular, reasoning separately about the transactional and nontransactional parts of the implementation. Central to our approach is the use of syntactic transformers oninteraction trees—i.e., transactional libraries that transform client code to enforce particular synchronization disciplines. Our framework and case studies are mechanized in Coq.