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