An official website of the United States government
We present an enumerative program synthesis framework calledcomponent-based refactoringthat can refactor “direct” style code that does not use library components into equivalent “combinator” style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code calledequivalence by canonicalizationthat does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such asmapandfilterin the staticallytyped functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool calledCobblerand evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.
more »
« less
This content will become publicly available on June 10, 2026
Functional Meaning for Parallel Streaming
Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by introducing a partial order structure on shared state that describes how the state evolves over time.Monotoneprograms that respect the order are deterministic. Datalog-inspired languages incorporate this idea of monotonicity in a first-class way but they are not general-purpose. We would like parallel and distributed languages to be as natural to use as any functional language, without sacrificing expressivity, and with a formal basis of study as appealing as the lambda calculus. This paper presents λ∨, a core language for deterministic parallelism that embodies the ideas above. In λ∨, values may increase over time according to astreaming orderand all computations are monotone with respect to that order. The streaming order coincides with the approximation order found in Scott semantics and so unifies the foundations of functional programming with the foundations of deterministic distributed computation. The resulting lambda calculus has a computationally adequate model rooted in domain theory. It integrates the compositionality and power of abstraction characteristic of functional programming with the declarative nature of Datalog.
more »
« less
- Award ID(s):
- 2247088
- PAR ID:
- 10621645
- Publisher / Repository:
- Association for Computing Machinery
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 9
- Issue:
- PLDI
- ISSN:
- 2475-1421
- Page Range / eLocation ID:
- 1220 to 1244
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Ultraviolet and visible integrated photonics enable applications in quantum information, sensing, and spectroscopy, among others. Few materials support low-loss photonics into the UV, and the relatively low refractive index of known depositable materials limits the achievable functionality. Here, we present a high-index integrated photonics platform based on HfO2and Al2O3composites deposited via atomic layer deposition (ALD) with low loss in the visible and near UV. We show that Al2O3incorporation dramatically decreases bulk loss compared to pure HfO2, consistent with inhibited crystallization due to the admixture of Al2O3. Composites exhibit refractive indexnfollowing the average of that of HfO2and Al2O3, weighted by the HfO2fractional compositionx. Atλ = 375 nm, composites withx = 0.67 exhibitn = 2.01, preserving most of HfO2’s significantly higher index, and 3.8(7) dB/cm material loss. We further present fully etched and cladded waveguides, grating couplers, and ring resonators, realizing a single-mode waveguide loss of 0.25(2) dB/cm inferred from resonators of 2.6 million intrinsic quality factor atλ = 729 nm, 2.6(2) dB/cm atλ = 405 nm, and 7.7(6) dB/cm atλ = 375 nm. We measure the composite’s thermo-optic coefficient (TOC) to be 2.44(3) × 10−5RIU/°C nearλ = 397 nm. This work establishes (HfO2)x(Al2O3)1−xcomposites as a platform amenable to integration for low-loss, high-index photonics spanning the UV to NIR.more » « less
-
Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states. The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e., the system identifies unfillable holes using a system of traced provenances, rather than localized in anad hocmanner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.more » « less
-
ABSTRACT ObjectiveNeighborhood perceptions are associated with physical and mental health outcomes; however, the biological associates of this relationship remain to be fully understood. Here, we evaluate the relationship between neighborhood perceptions and amygdala activity and connectivity with salience network (i.e., insula, anterior cingulate, thalamus) nodes. MethodsForty-eight older adults (mean age = 68 [7] years, 52% female, 47% non-Hispanic Black, 2% Hispanic) without dementia or depression completed the Perceptions of Neighborhood Environment Scale. Lower scores indicated less favorable perceptions of aesthetic quality, walking environment, availability of healthy food, safety, violence (i.e., more perceived violence), social cohesion, and participation in activities with neighbors. Participants separately underwent resting-state functional magnetic resonance imaging. ResultsLess favorable perceived safety (β= −0.33,pFDR= .04) and participation in activities with neighbors (β= −0.35,pFDR= .02) were associated with higher left amygdala activity, independent of covariates including psychosocial factors. Less favorable safety perceptions were also associated with enhanced left amygdala functional connectivity with the bilateral insular cortices and the left anterior insula (β= −0.34,pFDR= .04). Less favorable perceived social cohesion was associated with enhanced left amygdala functional connectivity with the right thalamus (β =−0.42,pFDR= .04), and less favorable perceptions about healthy food availability were associated with enhanced left amygdala functional connectivity with the bilateral anterior insula (right:β= −0.39,pFDR= .04; left:β= −0.42,pFDR= .02) and anterior cingulate gyrus (β= −0.37,pFDR= .04). ConclusionsTaken together, our findings document relationships between select neighborhood perceptions and amygdala activity as well as connectivity with salience network nodes; if confirmed, targeted community-level interventions and existing community strengths may promote brain-behavior relationships.more » « less
-
Parallel programs are frequently modeled asdependencyorcostgraphs, which can be used to detect various bugs, or simply to visualize the parallel structure of the code. However, such graphs reflect just one particular execution and are typically constructed in apost-hocmanner.Graph types, which were introduced recently to mitigate this problem, can be assigned statically to a program by a type system and compactly represent the family of all graphs that could result from the program. Unfortunately, prior work is restricted in its treatment offutures, an increasingly common and especially dynamic form of parallelism. In short, each instance of a future must be statically paired with a vertex name. Previously, this led to the restriction that futures could not be placed in collections or be used to construct data structures. Doing so is not a niche exercise: such structures form the basis of numerous algorithms that use forms of pipelining to achieve performance not attainable without futures. All but the most limited of these examples are out of reach of prior graph type systems. In this paper, we propose a graph type system that allows for almost arbitrary combinations of futures and recursive data types. We do so by indexing datatypes with a type-levelvertex structure, a codata structure that supplies unique vertex names to the futures in a data structure. We prove the soundness of the system in a parallel core calculus annotated with vertex structures and associated operations. Although the calculus is annotated, this is merely for convenience in defining the type system. We prove that it is possible to annotate arbitrary recursive types with vertex structures, and show using a prototype inference engine that these annotations can be inferred from OCaml-like source code for several complex parallel algorithms.more » « less
