4 papers
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…