6 citations · 20 across the 17 of their papers we have counts for
18 papers
Taming Scope Extrusion in Gradual Imperative Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek +4
Metaprogramming enables the generation of performant code, while gradual typing facilitates the smooth migration from untyped scripts to robust statically typed programs. However,…
Gradual Metaprogramming
Tianyu Chen, Darshal Shetty, Jeremy G. Siek +4
Data engineers increasingly use domain-specific languages (DSLs) to generate the code for data pipelines. Such DSLs are often embedded in Python. Unfortunately, there are challenge…
Quest Complete: the Holy Grail of Gradual Security
Tianyu Chen, Jeremy G. Siek
Languages with gradual information-flow control combine static and dynamic techniques to prevent security leaks. Gradual languages should satisfy the gradual guarantee: programs th…
Mechanized Noninterference for Gradual Security
Tianyu Chen, Jeremy G. Siek
This paper presents the first machine-checked proof of noninterference for a language with gradual information-flow control, thereby establishing a rock solid foundation for secure…
Parameterized Cast Calculi and Reusable Meta-theory for Gradually Typed Lambda Calculi
Jeremy G. Siek
The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek and Taha (2006) and its underlying cast calculus. For example, Wadle…
Transitivity of Subtyping for Intersection Types
Jeremy G. Siek
The subtyping rules for intersection types traditionally employ a transitivity rule (Barendregt et al. 1983), which means that subtyping does not satisfy the subformula property, m…