54 citations · 141 across the 20 of their papers we have counts for
24 papers
Lava: Foundations for Liquid Haskell via Translation to Rocq
Colin Rothgang, Loïc Peyrot, Yannick Forster +2
Liquid Haskell is an extension of the Glasgow Haskell compiler (GHC) that adds support for refinement types: types restricted by logical predicates. Specifications are automaticall…
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…
Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners
Louis Rustenholz, Manuel V. Hermenegildo, Pedro Lopez-Garcia +3
We present the theory underpinning a complexity analysis tool (under development) that aims at automating tedious parts of the analysis of complex algorithms originating from the f…
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…
Mechanizing Refinement Types (extended)
Michael Borkowski, Niki Vazou, Ranjit Jhala
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verifica…
Flux: Liquid Types for Rust
Nico Lehmann, Adam Geller, Niki Vazou +1
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manip…
Verified Causal Broadcast with Liquid Haskell
Patrick Redmond, Gan Shen, Niki Vazou +1
Protocols to ensure that messages are delivered in causal order are a ubiquitous building block of distributed systems. For instance, distributed data storage systems can use causa…
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…
How to Safely Use Extensionality in Liquid Haskell
Niki Vazou, Michael Greenberg
Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs t…
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…
LIO*: Low Level Information Flow Control in F*
Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin +1
We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired…
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…
LWeb: Information Flow Security for Multi-tier Web Applications
James Parker, Niki Vazou, Michael Hicks
This paper presents LWeb, a framework for enforcing label-based, information flow policies in database-using web applications. In a nutshell, LWeb marries the LIO Haskell IFC enfor…
Gradual Liquid Type Inference
Niki Vazou, Éric Tanter, David Van Horn
Liquid typing provides a decidable refinement inference mechanism that is convenient but subject to two major issues: (1) inference is global and requires top-level annotations, ma…
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell)
Niki Vazou, Joachim Breitner, Will Kunkel +2
Equational reasoning is one of the key features of pure functional languages such as Haskell. To date, however, such reasoning always took place externally to Haskell, either manua…
Refinement Types for Ruby
Milod Kazerounian, Niki Vazou, Austin Bourgerie +2
Refinement types are a popular way to specify and reason about key program properties. In this paper, we introduce RTR, a new system that adds refinement types to Ruby. RTR is buil…
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury +4
We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the fu…
Deriving Law-Abiding Instances
Ryan Scott, Vikraman Choudhury, Ryan Newton +2
Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. Bu…
Verified Parallel String Matching in Haskell
Niki Vazou, Jeff Polakow
In this paper, we prove correctness of parallelizing a string matcher using Haskell as a theorem prover. We use refinement types to specify correctness properties, Haskell terms to…
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT)
Niki Vazou, Ranjit Jhala
Refinement Reflection turns your favorite programming language into a proof assistant by reflecting the code implementing a user-defined function into the function's (output) refin…
Bounded Refinement Types
Niki Vazou, Alexander Bakst, Ranjit Jhala
We present a notion of bounded quantification for refinement types and show how it expands the expressiveness of refinement typing by using it to develop typed combinators for: (1)…
Type Targeted Testing
Eric L. Seidel, Niki Vazou, Ranjit Jhala
We present a new technique called type targeted testing, which translates precise refinement types into comprehensive test-suites. The key insight behind our approach is that throu…
From Safety To Termination And Back: SMT-Based Verification For Lazy Languages
Niki Vazou, Eric L. Seidel, Ranjit Jhala
SMT-based verifiers have long been an effective means of ensuring safety properties of programs. While these techniques are well understood, we show that they implicitly require ea…