4 citations · 7 across the 3 of their papers we have counts for
4 papers · 1 filter
Bounded First-Class Universe Levels in Dependent Type Theory
Jonathan Chan, Stephanie Weirich
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…
Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
Li-yao Xia, Laura Israel, Maite Kramarz +4
Lazy evaluation is a powerful tool that enables better compositionality and potentially better performance in functional programming, but it is challenging to analyze its computati…
Effects and Coeffects in Call-By-Push-Value (Extended Version)
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal +2
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 investiga…
Making Logical Relations More Relatable (Proof Pearl)
Emmanuel Suárez Acevedo, Stephanie Weirich
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 p…