29 citations · 30 across the 9 of their papers we have counts for
12 papers · 1 filter
Abstract Compilation as Abstraction of Operator Semantics, applied to Cost Analysis
Louis Rustenholz, Alessio Mansutti, Pedro López-García +3
Least fixpoints are fundamental to program semantics, but they abstract away the recursive structure that generated them. We introduce operator semantics: a semantic intermediate r…
Circuit Width Estimation via Effect Typing and Linear Dependency (Long Version)
Andrea Colledan, Ugo Dal Lago
Circuit description languages are a class of quantum programming languages in which programs are classical and produce a description of a quantum computation, in the form of a quan…
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri +1
Non-interference is a popular way to enforce confidentiality of sensitive data. However, declassification of sensitive information is often needed in realistic applications but bre…
REST: Integrating Term Rewriting with Program Verification (Extended Version)
Zachary Grannan, Niki Vazou, Eva Darulova +1
We introduce REST, a novel term rewriting technique for theorem proving that uses online termination checking and can be integrated with existing program verifiers. REST enables fl…
Refinement Types: A Tutorial
Ranjit Jhala, Niki Vazou
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable…
Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou +2
Many researchers have explored ways to bring static typing to dynamic languages. However, to date, such systems are not precise enough when types depend on values, which often aris…