arXiv subjects

Stephanie Weirich

Publications and source records attributed to Stephanie Weirich.

At least 19 recordsLinked to original sources

arXiv2026

Definitional Inversion, Without Normalisation

We contribute a new proof technique, based on domain theory, to prove key meta-theoretic properties of dependent type systems: definitional inversion properties, i.e. injectivity and no-confusion of type constructors. This proof technique is independent of normalisation, and indeed applies even for the "type-in-type" rule of Martin-L\"of's original type theory. Our proof is the first to establish injectivity of type constructors for such a system in the presence of $\eta$ laws. More generally, the technique is motivated by, and intended for, the metatheory of systems such as Idris, Lean, or dependent Haskell, whose underlying type theory is known to be non-normalising, as well as projects such as MetaRocq or Lean4Lean, where G\"odel's second incompleteness theorem means we cannot show normalisation of the object logic in itself. We showcase the method on a small type theory, then explain how it extends to more ambitious extensions.

cs.LO↗

arXiv2026

Typing Strictness (Extended Version)

Strictness analysis is critical to efficient implementation of languages with non-strict evaluation, mitigating much of the performance overhead of laziness. However, reasoning about strictness at the source level can be challenging and unintuitive. We propose a new definition of strictness that refines the traditional one by describing variable usage more precisely. We lay type-theoretic foundations for this definition in both call-by-name and call-by-push-value settings, drawing inspiration from the literature on type systems tracking effects and coeffects. We prove via a logical relation that the strictness attributes computed by our type systems accurately describe the use of variables at runtime, and we offer a strictness-annotation-preserving translation from the call-by-name system to the call-by-push-value one. All our results are mechanized in Rocq.

cs.PL↗

arXiv2025

Rebound: Efficient, Expressive, and Well-Scoped Binding

We introduce the Rebound library that supports well-scoped term representations in Haskell and automates the definition of substitution, alpha-equivalence, and other operations that work with binding structures. The key idea of our design is the use of first-class environments that map variables to expressions in some new scope. By statically tracking scopes, users of this library gain confidence that they have correctly maintained the subtle invariants that stem from using de Bruijn indices. Behind the scenes, Rebound uses environments to optimize the application of substitutions, while providing explicit access to these data structures when desired. We demonstrate that this library is expressive by using it to implement a wide range of language features with sophisticated uses of binding and several different operations that use this abstract syntax. Our examples include pi-forall, a tutorial implementation of a type checker for a dependently-typed programming language. Finally, we benchmark Rebound to understand its performance characteristics and find that it produces faster code than competing libraries.

cs.PL↗

arXiv2025

Bounded First-Class Universe Levels in Dependent Type Theory

In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from introducing logical inconsistency in the presence of type-in-type. The simplest mechanism is a hierarchy of universes indexed by a sequence of levels, typically the naturals. To improve reusability of definitions, they can be made level polymorphic, abstracting over level variables and adding a notion of level expressions. For even more expressive power, level expressions can be made first-class as terms themselves, and level polymorphism is subsumed by dependent functions quantifying over levels. Furthermore, bounded level polymorphism provides more expressivity by being able to explicitly state constraints on level variables. While semantics for first-class levels with constraints are known, syntax and typing rules have not been explicitly written down. Yet pinning down a well-behaved syntax is not trivial; there exist prior type theories with bounded level polymorphism that fail to satisfy subject reduction. In this work, we design an explicit syntax for a type theory with bounded first-class levels, parametrized over arbitrary well-founded sets of levels. We prove the metatheoretic properties of subject reduction, type safety, consistency, and canonicity, entirely mechanized from syntax to semantics in Lean.

cs.PL↗

arXiv2024

Effects and Coeffects in Call-By-Push-Value (Extended Version)

Effect and coeffect tracking integrate many types of compile-time analysis, such as cost, liveness, or dataflow, directly into a language's type system. In this paper, we investigate the addition of effect and coeffect tracking to the type system of call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and for its ability to cleanly express both call-by-name and call-by-value computations. Our main result is effect-and-coeffect soundness, which asserts that the type system accurately bounds the effects that the program may trigger during execution and accurately tracks the demands that the program may make on its environment. This result holds for two different dynamic semantics: a generic one that can be adapted for different coeffects and one that is adapted for reasoning about resource usage. In particular, the second semantics discards the evaluation of unused values and pure computations while ensuring that effectful computations are always evaluated, even if their results are not required. Our results have been mechanized using the Coq proof assistant.

cs.PL↗

arXiv2024

Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs

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.

cs.PL↗

arXiv2024

Stratified Type Theory

A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type rule. In this work, we argue that a universe hierarchy is not the only option for a type theory with a type universe. Taking inspiration from Leivant's Stratified System F, we introduce Stratified Type Theory (StraTT), where rather than stratifying universes by levels, we stratify typing judgements and restrict the domain of dependent functions to strictly lower levels. Even with type-in-type, this restriction suffices to enforce consistency. In StraTT, we consider a number of extensions beyond just stratified dependent functions. First, the subsystem subStraTT employs McBride's crude-but-effective stratification (also known as displacement) as a simple form of level polymorphism where global definitions with concrete levels can be displaced uniformly to any higher level. Second, to recover some expressivity lost due to the restriction on dependent function domains, the full StraTT includes a separate nondependent function type with a "floating" domain whose level matches that of the overall function type. Finally, we have implemented a prototype type checker for StraTT extended with datatypes and inference for level and displacement annotations, along with a small core library. We have proven subStraTT to be consistent and StraTT to be type safe, but consistency of the full StraTT remains an open problem, largely due to the interaction between floating functions and cumulativity of judgements. Nevertheless, we believe StraTT to be consistent, and as evidence have verified the failure of some well-known type-theoretic paradoxes using our implementation.

cs.PL↗

arXiv2023

Making Logical Relations More Relatable (Proof Pearl)

Mechanical proofs by logical relations often involve tedious reasoning about substitution. In this paper, we show that this is not necessarily the case, by developing, in Agda, a proof that all simply typed lambda calculus expressions evaluate to values. A formalization of the proof is remarkably short (~40 lines of code), making for an excellent introduction to the technique of proofs by logical relations not only on paper but also in a mechanized setting. We then show that this process extends to more sophisticated reasoning by also proving the totality of normalization by evaluation. Although these proofs are not new, we believe presenting them will empower both new and experienced programming language theorists in their use of logical relations.

cs.PL↗

arXiv2023

Implementing Dependent Types in pi-forall

These lecture notes describe the design of a minimal dependently-typed language called "pi-forall" and walk through the implementation of its type checker. They are based on lectures given at the Oregon Programming Languages Summer School during July 2023.

cs.PL↗

arXiv2022

Program Adverbs and Tlön Embeddings

Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpreted events, while admitting a rich equational theory of equivalence. But monads are not the only way to structure effectful computation, why should we limit ourselves? In this paper, inspired by applicative functors, selective functors, and other structures, we define a collection of data structures and theories, which we call program adverbs, that capture a variety of computational patterns. Program adverbs are themselves composable, allowing them to be used to specify the semantics of languages with multiple computation patterns. We use program adverbs as the basis for a new class of semantic embeddings called Tlön embeddings. Compared with embeddings based on free monads, Tlön embeddings allow more flexibility in computational modeling of effects, while retaining more information about the program's syntactic structure.

cs.PL↗

arXiv2022

A Dependent Dependency Calculus (Extended Version)

Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language design: its results can help users and compilers enforce security constraints, eliminate dead code, among other applications. In this work, we present a Dependent Dependency Calculus (DDC), which extends this general idea to the setting of a dependently-typed language. We use this calculus to track both run-time and compile-time irrelevance, enabling faster type-checking and program execution.

cs.PL↗

arXiv2021

Reasoning about the garden of forking paths

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.

cs.PL↗

arXiv2021

ICFP 2020 Post-Conference Report

This document describes the ICFP 2020 virtual conference, including the planning process and the criteria that informed its design, plus feedback from the post-conference survey. It is intended to provide a record of the event and give advice to future organizers of virtual conferences.

cs.DL↗

arXiv2019

Embracing a mechanized formalization gap

If a code base is so big and complicated that complete mechanical verification is intractable, can we still apply and benefit from verification methods? We show that by allowing a deliberate mechanized formalization gap we can shrink and simplify the model until it is manageable, while still retaining a meaningful, declaratively documented connection to the original, unmodified source code. Concretely, we translate core parts of the Haskell compiler GHC into Coq, using hs-to-coq, and verify invariants related to the use of term variables.

cs.PL↗

arXiv2019

A Role for Dependent Types in Haskell (Extended version)

Modern Haskell supports zero-cost coercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism of roles to prohibit invalid coercions. In this work, we show how to integrate roles with dependent type systems and prove, using the Coq proof assistant, that the resulting system is sound. We have designed this work as a foundation for the addition of dependent types to the Glasgow Haskell Compiler, but we also expect that it will be of use to designers of other dependently-typed languages who might want to adopt Haskell's safe coercions feature.

cs.PL↗

arXiv2018

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code

Good tools can bring mechanical verification to programs written in mainstream functional languages. We use hs-to-coq to translate significant portions of Haskell's containers library into Coq, and verify it against specifications that we derive from a variety of sources including type class laws, the library's test suite, and interfaces from Coq's standard library. Our work shows that it is feasible to verify mature, widely-used, highly optimized, and unmodified Haskell code. We also learn more about the theory of weight-balanced trees, extend hs-to-coq to handle partiality, and -- since we found no bugs -- attest to the superb quality of well-tested functional code.

cs.PL↗

arXiv2017

Total Haskell is Reasonable Coq

We would like to use the Coq proof assistant to mechanically verify properties of Haskell programs. To that end, we present a tool, named hs-to-coq, that translates total Haskell programs into Coq programs via a shallow embedding. We apply our tool in three case studies -- a lawful Monad instance, "Hutton's razor", and an existing data structure library -- and prove their correctness. These examples show that this approach is viable: both that hs-to-coq applies to existing Haskell code, and that the output it produces is amenable to verification.

cs.PL↗

arXiv2012

Step-Indexed Normalization for a Language with General Recursion

The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments-a_logical_fragment where every term normalizes and which is consistent when interpreted as a logic, and a_programmatic_fragment with general recursion and other convenient but unsound features. In this paper, we present a small example language in this style. Our design allows the programmer to explicitly mention and pass information between the two fragments. We show that this feature substantially complicates the metatheory and present a new technique, combining the traditional Girard-Tait method with step-indexed logical relations, which we use to show normalization for the logical fragment.

cs.PL↗