2015/11/04 by Ronald Garcia, Garcia, Ronald, Éric Tanter +1
Computer Science · #Advanced Malware Detection Techniques #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1511.01399
openalex publication_date 2015/11/04 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Abstracting Gradual Typing (AGT) is an approach to systematically deriving gradual counterparts to static type disciplines. The approach consists of defining the semantics of gradual types by interpreting them as sets of static types, and then defining an optimal abstraction back to gradual types. These operations are used to lift the static discipline to the gradual setting. The runtime semantics of the gradual language then arises as reductions on gradual typing derivations. To demonstrate the flexibility of AGT, we gradualize λSEC, the prototypical security-typed language, with respect to only security labels rather than entire types, yielding a type system that ranges gradually from simply-typed to securely-typed. We establish noninterference for the gradual language, called λ_\widetildeSEC, using Zdancewic's logical relation proof method. Whereas prior work presents gradual security cast languages, which require explicit security casts, this work yields the first gradual security source language, which requires no explicit casts.