18 citations · 35 across the 7 of their papers we have counts for
7 papers · 1 filter
Propositional Equality for Gradual Dependently Typed Programming
Joseph Eremondi, Ronald Garcia, Éric Tanter
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have b…
Approximate Normalization and Eager Equality Checking for Gradual Inductive Families
Joseph Eremondi, Ronald Garcia, Éric Tanter
Harnessing the power of dependently typed languages can be difficult. Programmers must manually construct proofs to produce well-typed programs, which is not an easy task. In parti…
Abstracting Gradual Typing Moving Forward: Precise and Space-Efficient (Technical Report)
Felipe Bañados Schwerter, Alison M. Clark, Khurram A. Jafery +1
Abstracting Gradual Typing (AGT) is a systematic approach to designing gradually-typed languages. Languages developed using AGT automatically satisfy the formal semantic criteria f…
Approximate Normalization for Gradual Dependent Types
Joseph Eremondi, Éric Tanter, Ronald Garcia
Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) de…
Deriving a Simple Gradual Security Language
Ronald Garcia, Éric Tanter
Abstracting Gradual Typing (AGT) is an approach to systematically deriving gradual counterparts to static type disciplines. The approach consists of defining the semantics of gradu…
Monotonic References for Gradual Typing
Jeremy G. Siek, Michael M. Vitousek
We describe an alternative approach to handling mutable references (aka. pointers) within a gradually typed language that has different efficiency characteristics than the prior ap…
Lazy Evaluation and Delimited Control
Ronald Garcia, Andrew Lumsdaine, Amr Sabry
The call-by-need lambda calculus provides an equational framework for reasoning syntactically about lazy evaluation. This paper examines its operational characteristics. By a serie…