4 citations · 10 across the 6 of their papers we have counts for
6 papers · 1 filter
Eiger: Auditable, executable, flexible legal regulations
Alexander Bernauer, Richard A. Eisenberg
Despite recent advances in communication and automation, regulations are still written in natural-language prose, subject to ambiguity, inconsistency, and incompleteness. How can w…
Seeking Stability by being Lazy and Shallow
Gert-Jan Bottu, Richard A. Eisenberg
Designing a language feature often requires a choice between several, similarly expressive possibilities. Given that user studies are generally impractical, we propose using stabil…
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…
Kind Inference for Datatypes: Technical Supplement
Ningning Xie, Richard A. Eisenberg, Bruno C. d. S. Oliveira
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the c…
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…
Constrained Type Families
J. Garrett Morris, Richard Eisenberg
We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either req…