31 citations · 74 across the 15 of their papers we have counts for
15 papers
Definitional Inversion, Without Normalisation
Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu +3
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 a…
Stratified Type Theory
Jonathan Chan, Stephanie Weirich
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 func…
Program Adverbs and Tlön Embeddings
Yao Li, Stephanie Weirich
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…
Implementing Dependent Types in pi-forall
Stephanie Weirich
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 lectur…
A Dependent Dependency Calculus (Extended Version)
Pritam Choudhury, Harley Eades, Stephanie Weirich
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 the…
ICFP 2020 Post-Conference Report
Stephanie Weirich, Benjamin Pierce
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. I…
Reasoning about the garden of forking paths
Yao Li, Li-yao Xia, Stephanie Weirich
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 e…
A graded dependent type system with a usage-aware semantics (extended version)
Pritam Choudhury, Harley Eades, Richard A. Eisenberg +1
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type sy…
Embracing a mechanized formalization gap
Antal Spector-Zabusky, Joachim Breitner, Yao Li +1
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…
A Role for Dependent Types in Haskell (Extended version)
Stephanie Weirich, Pritam Choudhury, Antoine Voizard +1
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…
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code
Joachim Breitner, Antal Spector-Zabusky, Yao Li +3
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 libr…
Total Haskell is Reasonable Coq
Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah +1
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 p…
Irrelevance, Heterogeneous Equality, and Call-by-value Dependent Type Systems
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn +7
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studi…
Step-Indexed Normalization for a Language with General Recursion
Chris Casinghino, Vilhelm Sjöberg, Stephanie Weirich
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 normal…
Termination Casts: A Flexible Approach to Termination with General Recursion
Aaron Stump, Vilhelm Sjöberg, Stephanie Weirich
This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambd…