Memory Safety and Race Freedom in Concurrent Programming Languages with Linear Capabilities. - Niki Vazou; Michalis A. Papakyriakou; Nikolaos Papaspyrou (FedCSIS, 2011)

Abstract Refinement Types. - Niki Vazou; Patrick Maxim Rondon; Ranjit Jhala (ESOP, 2013)

LiquidHaskell: experience with refinement types in the real world. - Niki Vazou; Eric L. Seidel; Ranjit Jhala (Haskell, 2014)

Refinement types for Haskell. - Niki Vazou; Eric L. Seidel; Ranjit Jhala; Dimitrios Vytiniotis; Simon L. Peyton Jones (ICFP, 2014)

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. - Niki Vazou; Eric L. Seidel; Ranjit Jhala (CoRR, 2014)

Type Targeted Testing. - Eric L. Seidel; Niki Vazou; Ranjit Jhala (ESOP, 2015)

Bounded refinement types. - Niki Vazou; Alexander Bakst; Ranjit Jhala (ICFP, 2015)

From Monads to Effects and Back. - Niki Vazou; Daan Leijen (PADL, 2016)

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT). - Niki Vazou; Ranjit Jhala (CoRR, 2016)

Verified Parallel String Matching in Haskell. - Niki Vazou; Jeff Polakow (CoRR, 2016)

Liquid Haskell: Haskell as a Theorem Prover. - Niki Vazou (2016)

A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq. - Niki Vazou; Leonidas Lampropoulos; Jeff Polakow (Haskell, 2017)

Deriving Law-Abiding Instances. - Ryan G. Scott; Vikraman Choudhury; Ryan Newton; Niki Vazou; Ranjit Jhala (CoRR, 2017)

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). - Niki Vazou; Joachim Breitner; Rose Kunkel; David Van Horn; Graham Hutton (Haskell@ICFP, 2018)

Refinement Types for Ruby. - Milod Kazerounian; Niki Vazou; Austin Bourgerie; Jeffrey S. Foster; Emina Torlak (VMCAI, 2018)

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). - Niki Vazou; Joachim Breitner; Will Kunkel; David Van Horn; Graham Hutton (CoRR, 2018)

Refinement reflection: complete verification with SMT. - Niki Vazou; Anish Tondwalkar; Vikraman Choudhury; Ryan G. Scott; Ryan R. Newton; Philip Wadler; Ranjit Jhala (Proc. ACM Program. Lang., 2018)

Gradual liquid type inference. - Niki Vazou; Éric Tanter; David Van Horn (Proc. ACM Program. Lang., 2018)

PLAS 2019: ACM SIGSAC Workshop on Programming Languages and Analysis for Security. - Piotr Mardziel; Niki Vazou (CCS, 2019)

Type-level computations for Ruby libraries. - Milod Kazerounian; Sankha Narayan Guria; Niki Vazou; Jeffrey S. Foster; David Van Horn (PLDI, 2019)

LWeb: information flow security for multi-tier web applications. - James Parker; Niki Vazou; Michael Hicks 001 (Proc. ACM Program. Lang., 2019)

LIO*: Low Level Information Flow Control in F. - Jean-Joseph Marty; Lucas Franceschino; Jean-Pierre Talpin; Niki Vazou (CoRR, 2020)

Liquidate your assets: reasoning about resource usage in liquid Haskell. - Martin A. T. Handley; Niki Vazou; Graham Hutton (Proc. ACM Program. Lang., 2020)

Verifying replicated data types with typeclass refinements in Liquid Haskell. - Yiyun Liu; James Parker; Patrick Redmond; Lindsey Kuper; Michael Hicks 001; Niki Vazou (Proc. ACM Program. Lang., 2020)

STORM: Refinement Types for Secure Web Applications. - Nico Lehmann; Rose Kunkel; Jordan Brown; Jean Yang 001; Niki Vazou; Nadia Polikarpova; Deian Stefan; Ranjit Jhala (OSDI, 2021)

Functional Extensionality for Refinement Types. - Niki Vazou; Michael Greenberg 002 (CoRR, 2021)

Refinement Types: A Tutorial. - Ranjit Jhala; Niki Vazou (Found. Trends Program. Lang., 2021)

REST: Integrating Term Rewriting with Program Verification. - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (ECOOP, 2022)

Liquid proof macros. - Henry Blanchette; Niki Vazou; Leonidas Lampropoulos (Haskell, 2022)

Coinduction inductively: mechanizing coinductive proofs in Liquid Haskell. - Lykourgos Mastorou; Nikolaos Papaspyrou; Niki Vazou (Haskell, 2022)

How to safely use extensionality in Liquid Haskell. - Niki Vazou; Michael Greenberg 002 (Haskell, 2022)

Verified Causal Broadcast with Liquid Haskell. - Patrick Redmond; Gan Shen; Niki Vazou; Lindsey Kuper (IFL, 2022)

ANOSY: approximated knowledge synthesis with refinement types for declassification. - Sankha Narayan Guria; Niki Vazou; Marco Guarnieri; James Parker (PLDI, 2022)

REST: Integrating Term Rewriting with Program Verification (Extended Version). - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (CoRR, 2022)

Flux: Liquid Types for Rust. - Nico Lehmann; Adam T. Geller; Gilles Barthe; Niki Vazou; Ranjit Jhala (CoRR, 2022)

Mechanizing Refinement Types (extended). - Michael Borkowski; Niki Vazou; Ranjit Jhala (CoRR, 2022)

REST: Integrating Term Rewriting with Program Verification (Artifact). - Zachary Grannan; Niki Vazou; Eva Darulova; Alexander J. Summers (Dagstuhl Artifacts Ser., 2022)

Safe couplings: coupled refinement types. - Elizaveta Vasilenko; Niki Vazou; Gilles Barthe (Proc. ACM Program. Lang., 2022)

Flux: Liquid Types for Rust. - Nico Lehmann; Adam T. Geller; Niki Vazou; Ranjit Jhala (Proc. ACM Program. Lang., 2023)

OBRA: Oracle-Based, Relational, Algorithmic Type Verification. - Elizaveta Vasilenko; Niki Vazou; Gilles Barthe (APLAS, 2024)

Mechanizing Refinement Types. - Michael Borkowski; Niki Vazou; Ranjit Jhala (Proc. ACM Program. Lang., 2024)