31 citations · 38 across the 8 of their papers we have counts for
9 papers · 1 filter
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…
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…
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…