An official website of the United States government
We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create entirely new DSLs whose dependent type ``power'' is tailored to a specific domain. Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs. This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.
more »
« less
This content will become publicly available on March 11, 2026
A steam-mediated isothermal amplification and flocculation-based detection platform for electricity-free point of care diagnostics
SteamFloc-LAMP is a molecular diagnostic platform that operates without electricity. It utilizes steam from boiling water for DNA amplification and flocculation for rapid pathogen detection, making it suitable for low-resource settings.
more »
« less
- PAR ID:
- 10582769
- Publisher / Repository:
- Analyst
- Date Published:
- Journal Name:
- The Analyst
- Volume:
- 150
- Issue:
- 6
- ISSN:
- 0003-2654
- Page Range / eLocation ID:
- 1187 to 1194
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
From the general inverse theory of periodic Jacobi matrices, it is known that a periodic Jacobi matrix of minimal period p≥2 may have at most p−2 closed spectral gaps. We discuss the maximal number of closed gaps for one-dimensional periodic discrete Schrödinger operators of period p. We prove nontrivial upper and lower bounds on this quantity for large p and compute it exactly for p≤6. Among our results, we show that a discrete Schrödinger operator of period four or five may have at most a single closed gap, and we characterize exactly which potentials may exhibit a closed gap. For period six, we show that at most two gaps may close. In all cases in which the maximal number of closed gaps is computed, it is seen to be strictly smaller than p−2, the bound guaranteed by the inverse theory. We also discuss similar results for purely off-diagonal Jacobi matrices.more » « less
-
In this paper, we consider weak solutions of the Euler–Lagrange equation to a variational energy functional modeling the geometrically nonlinear Cosserat micropolar elasticity of continua in dimension three, which is a system coupling between the Poisson equation and the equation of $$p$$-harmonic maps (#2\le p\le 3$$). We show that if a weak solution is stationary, then its singular set is discrete for $2<3$ and has zero one-dimensional Hausdorff measure for $p=2$. If, in addition, it is a stable-stationary weak solution, then it is regular everywhere when $$p\in [2, 32/15]$$.more » « less
-
Abstract IntroductionWe rely on coastal resources for food, water, and energy. However, over 75% of U.S. coastlines are eroding. Concurrently, the U.S. recycles less glass than other developed countries, landfilling hundreds of millions of tons every year. Recycled glass sand has many potential benefits over natural sand for combatting land loss; for example, it can be produced with controlled particle size to better resist erosion, making it an excellent—and underutilized—material for environmental restoration. ObjectivesThis research compares the physical and chemical properties of recycled glass sand to natural sands (beach and dredge) from the U.S. Gulf Coast to assess environmental safety. MethodsParticle size distribution, angularity, particle and bulk density, compaction, and permeability were evaluated using standard methods. Elemental composition and leaching were analyzed using x‐ray fluorescence and toxicity characteristic leaching procedure (TCLP), respectively. ResultsRecycled glass sand is not “sharp,” although it is less well‐rounded than natural sand. Porosity, compaction, and water permeability depend on particle size, and glass sand can be size‐separated to match or complement natural sand. Recycled glass sand is mostly silica. Additional elements used in glass processing are present at acceptable levels, and no leaching of harmful elements is detectable by TCLP. Thermally decomposable residues (e.g. label and adhesive) reliably comprised less than 1% of the material. ConclusionsThe characteristics of recycled glass sand make it a good resource for environmental restoration.more » « less
-
This review discusses the effectiveness of visual and haptic cues for second language (L2) lexical tone acquisition, with a special focus on observation and production of hand gestures. It explains how these cues can facilitate initial acquisition of L2 lexical tones via multimodal depictions of pitch. In doing so, it provides recommendations for incorporation of multimodal cues into L2 lexical tone pedagogy.more » « less
