Searcharxiv⌕ Search

arXiv subjects

William J. Bowman

Publications and source records attributed to William J. Bowman.

13 recordsLinked to original sources

Human Perception-Inspired Grain Segmentation Refinement Using Conditional Random Fields

Automated detection of grain boundaries (GBs) in electron microscope images of polycrystalline materials could help accelerate the nanoscale characterization of myriad engineering materials and novel materials under scientific research. Accurate segmentation of interconnected line networks, such as GBs in polycrystalline material microstructures, poses a significant challenge due to the fragmented masks produced by conventional computer vision (CV) algorithms, including convolutional neural networks. These algorithms struggle with thin masks, often necessitating post-processing for effective contour closure and continuity. Previous approaches in this domain have typically relied on custom post-processing techniques that are problem-specific and heavily dependent on the quality of the mask obtained from a CV algorithm. Addressing this issue, this paper introduces a fast, high-fidelity post-processing technique that is universally applicable to segmentation masks of interconnected line networks. Leveraging domain knowledge about grain boundary connectivity, this method employs conditional random fields and perceptual grouping rules to refine segmentation masks of any image with a discernible grain structure. This approach significantly enhances segmentation mask accuracy by correctly reconstructing fragmented GBs in electron microscopy images of a polycrystalline oxide. The refinement improves the statistical representation of the microstructure, reflected by a 51 % improvement in a grain alignment metric that provides a more physically meaningful assessment of complex microstructures than conventional metrics. This method enables rapid and accurate characterization, facilitating an unprecedented level of data analysis and improving the understanding of GB networks, making it suitable for a range of disciplines where precise segmentation of interconnected line networks is essential.

cond-mat.mtrl-sci↗

Macro-embedding Compiler Intermediate Languages in Racket

We present the design and implementation of a macro-embedding of a family of compiler intermediate languages, from a Scheme-like language to x86-64, into Racket. This embedding is used as part of a testing framework for a compilers course to derive interpreters for all the intermediate languages. The embedding implements features including safe, functional abstractions as well as unsafe assembly features, and the interactions between the two at various intermediate stages. This paper aims to demonstrate language-oriented techniques and abstractions for implementing (1) a large family of languages and (2) interoperability between low- and high-level languages. The primary strength of this approach is the high degree of code reuse and interoperability compared to implementing each interpreter separately. The design emphasizes modularity and compositionality of an open set of language features by local macro expansion into a single host language, rather than implementing a language pre-defined by a closed set of features. This enables reuse from both the host language (Racket) and between intermediate languages, and enables interoperability between high- and low-level features, simplifying development of the intermediate language semantics. It also facilitates extending or redefining individual language features in intermediate languages, and exposing multiple interfaces to the embedded languages.

cs.PL↗

Compilation as Multi-Language Semantics

Modeling interoperability between programs in different languages is a key problem when modeling verified and secure compilation, which has been successfully addressed using multi-language semantics. Unfortunately, existing models of compilation using multi-language semantics define two variants of each compiler pass: a syntactic translation on open terms to model compilation, and a run-time translation of closed terms at multi-language boundaries to model interoperability. In this talk, I discuss work-in-progress approach to uniformly model a compiler entirely as a reduction system on open term in a multi-language semantics, rather than as a syntactic translation. This simultaneously defines the compiler and the interoperability semantics, reducing duplication. It also provides interesting semantic insights. Normalization of the cross-language redexes performs ahead-of-time (AOT) compilation. Evaluation in the multi-language models just-in-time (JIT) compilation. Confluence of multi-language reduction implies compiler correctness, and part of the secure compilation proof (full abstraction), enabling focus on the difficult part of the proof. Subject reduction of the multi-language reduction implies type-preservation of the compiler.

cs.PL↗

Extended Abstract: Towards a Performance Comparison of Syntax and Type-Directed NbE

A key part of any dependent type-checker is the method for checking whether two types are equal. A common claim is that syntax-directed equality is more performant, although type-directed equality is more expressive. However, this claim is difficult to make precise, since implementations choose only one or the other approach, making a direct comparison impossible. We present some work-in-progress developing a realistic platform for direct, apples-to-apples, comparison of the two approaches, quantifying how much slower type-directed equality checking is, and analyzing why and how it can be improved.

cs.PL↗

Dependent-Type-Preserving Memory Allocation

Dependently typed programming languages such as Coq, Agda, Idris, and F*, allow programmers to write detailed specifications of their programs and prove their programs meet these specifications. However, these specifications can be violated during compilation since they are erased after type checking. External programs linked with the compiled program can violate the specifications of the original program and change the behavior of the compiled program -- even when compiled with a verified compiler. For example, since Coq does not allow explicitly allocating memory, a programmer might link their Coq program with a C program that can allocate memory. Even if the Coq program is compiled with a verified compiler, the external C program can still violate the memory-safe specification of the Coq program by providing an uninitialized pointer to memory. This error could be ruled out by type checking in a language expressive enough to indicate whether memory is initialized versus uninitialized. Linking with a program with an uninitialized pointer could be considered ill-typed, and our linking process could prevent linking with ill-typed programs. To facilitate type checking during linking, we can use type-preserving compilation, which preserves the types through the compilation process. In this ongoing work, we develop a typed intermediate language that supports dependent memory allocation, as well as a dependent-type-preserving compiler pass for memory allocation.

cs.PL↗

Fast and Extensible Hybrid Embeddings with Micros

Macro embedding is a popular approach to defining extensible shallow embeddings of object languages in Scheme like host languages. While macro embedding has even been shown to enable implementing extensible typed languages in systems like Racket, it comes at a cost: compile-time performance. In this paper, we revisit micros - syntax to intermediate representation (IR) transformers, rather than source syntax to source syntax transformers (macros). Micro embedding enables stopping at an IR, producing a deep embedding and enabling high performance compile-time functions over an efficient IR, before shallowly embedding the IR back into source syntax. Combining micros with several design patterns to enable the IR and functions over it to be extensible, we achieve extensible hybrid embedding of statically typed languages with significantly improved compile-time compared to macro-embedding approaches. We describe our design patterns and propose new abstractions packaging these patterns.

cs.PL↗

One Weird Trick to Untie Landin's Knot

In this work, we explore Landin's Knot, which is understood as a pattern for encoding general recursion, including non-termination, that is possible after adding higher-order references to an otherwise terminating language. We observe that this isn't always true -- higher-order references, by themselves, don't lead to non-termination. The key insight is that Landin's Knot relies not primarily on references storing functions, but on unrestricted quantification over a function's environment. We show this through a closure converted language, in which the function's environment is made explicit and hides the type of the environment through impredicative quantification. Once references are added, this impredicative quantification can be exploited to encode recursion. We conjecture that by restricting the quantification over the environment, higher-order references can be safely added to terminating languages, without resorting to more complex type systems such as linearity, and without restricting references from storing functions.

cs.PL↗

Type Universes as Allocation Effects

In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidding a type from quantifying over all types. Instead, the types of types (universes) form a hierarchy, and a type can only quantify over types in other universes (with some exceptions), restricting cyclic reasoning in proofs. We present a perspective where universes also describe \emph{where} values are allocated in the heap, and the choice of universe algebra imposes a structure on the heap overall. The resulting type system provides a simple declarative system for reasoning about and restricting memory allocation, without reasoning about reads or writes. We present a theoretical framework for equipping a type system with higher-order references restricted by a universe hierarchy, and conjecture that many existing universe algebras give rise to interesting systems for reasoning about allocation. We present 3 instantiations of this approach to enable reasoning about allocation in the simply typed $λ$-calculus: (1) the standard ramified universe hierarchy, which we prove guarantees termination of the language extended with higher-order references by restricting cycles in the heap; (2) an extension with an \emph{impredicative} base universe, which we conjecture enables full-ground references (with terminating computation but cyclic ground data structures); (3) an extension with \emph{universe polymorphism}, which divides the heap into fine-grained regions.

cs.PL↗

Compositionally Complex Perovskite Oxides as a New Class of Li-Ion Solid Electrolytes

Compositionally complex ceramics (CCCs), including high-entropy ceramics (HECs) as a subclass, offer new opportunities of materials discovery beyond the traditional methodology of searching new stoichiometric compounds. Herein, we establish new strategies of tailoring CCCs via a seamless combination of (1) non-equimolar compositional designs and (2) controlling microstructures and interfaces. Using oxide solid electrolytes for all-solid-state batteries as an exemplar, we validate these new strategies via discovering a new class of compositionally complex perovskite oxides (CCPOs) to show the possibility of improving ionic conductivities beyond the limit of conventional doping. As an example (amongst the 28 CCPOs examined), we demonstrate that the ionic conductivity can be improved by >60% in (Li0.375Sr0.4375)(Ta0.375Nb0.375Zr0.125Hf0.125)O3-δ, in comparison with the state-of-art (Li0.375Sr0.4375)(Ta0.75Zr0.25)O3-δ (LSTZ) baseline, via maintaining comparable electrochemical stability. Furthermore, the ionic conductivity can be improved by another >70% via grain boundary (GB) engineering, achieving >270% of the LSTZ baseline. This work suggests transformative new strategies for designing and tailoring HECs and CCCs, thereby opening a new window for discovering materials for energy storage and many other applications.

cond-mat.mtrl-sci↗

Is Sized Typing for Coq Practical?

Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven't they been adapted to Coq? In this paper, we venture to answer this question with CIC$\widehat{*}$, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq's kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is wildly impractical in terms of performance.

cs.PL↗

Emergence of near-boundary segregation zones in face-centered cubic multi-principal element alloys

Grain boundaries have been shown to dramatically influence the behavior of relatively simple materials such as monatomic metals and binary alloys. The increased chemical complexity associated with multi-principal element alloys is hypothesized to lead to new grain boundary phenomena. To explore the relationship between grain boundary structure and chemistry in these materials, hybrid molecular dynamics/Monte Carlo simulations of a faceted Σ11 <110> tilt boundary, chosen to sample both high- and low-energy boundary configurations, are performed in face-centered cubic CrFeCoNiCu and CrFeCoNi equiatomic alloys. Unexpected enrichment of Fe is discovered in the face-centered cubic regions adjacent to the interface and found to be correlated with a structurally-distinct region of reduced atomic volume. Comparison with the boundary of the same type in monatomic Cu demonstrates that altered near-boundary regions exist in simpler systems as well, with the chemical complexity of the multi-principal element alloys highlighting its existence and importance.

cond-mat.mtrl-sci↗

Dependent Type Systems as Macros

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.

cs.PL↗

Typed Closure Conversion for the Calculus of Constructions

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but compilation interferes with the type-system rules for reasoning about run-time terms. We develop a type-preserving closure-conversion translation from the Calculus of Constructions (CC) with strong dependent pairs ($Σ$ types)---a subset of the core language of Coq---to a type-safe, dependently typed compiler intermediate language named CC-CC. The central challenge in this work is how to translate the source type-system rules for reasoning about functions into target type-system rules for reasoning about closures. To justify these rules, we prove soundness of CC-CC by giving a model in CC. In addition to type preservation, we prove correctness of separate compilation.

cs.PL↗