2024
OBRA: Oracle-Based, Relational, Algorithmic Type Verification by Elizaveta Vasilenko, Niki Vazou, and Gilles Barthe. APLAS 2024 [.pdf]
Modular Implementation and Formalization of Dynamic Policies Work In Progress by Antonio Zegarelli, Niki Vazou, and Marco Guarnieri. FCS 2024 [.pdf]
Mechanizing Refinement Types by Michael Borokowski, Niki Vazou, and Ranjit Jhala. POPL 2024 [.pdf]
2023
Flux: Liquid types for rust by Nico Lehmann, Adam T Geller, Niki Vazou, Ranjit Jhala. PLDI 2023 [.pdf, doi]
Towards a Translation from Liquid Haskell to Coq by Lykourgos Mastorou, Niki Vazou, and Michael Greenberg. TYPES 2023 [.pdf
On the Practicality and Soundness of Refinement Types by Niki Vazou. LFMTP 2023 [.pdf
2022
Verified Causal Broadcast with Liquid Haskell by Patrick Redmond, Gan Shen, Niki Vazou, and Lindsey Kuper. IFL 2022 [.pdf, doi]
Safe Couplings: Coupled Refinement Types by Lisa Vasilenko, Niki Vazou, and Gilles Barthe. ICFP 2022 [.pdf, artifact]
Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell by Lykourgos Mastorou, Nikolaos Papaspyrou, and Niki Vazou. Haskell 2022. [.pdf, artifact]
How to Safely Use Extensionality in Liquid Haskell by Niki Vazou and Michael Greenberg. Haskell 2022. [.pdf, artifact]
Liquid Proof Macros by Henry Blanchette, Niki Vazou, and Leonidas Lampropoulos. Haskell 2022. [.pdf, artifact]
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification by Sankha Guria, Niki Vazou, Marco Guarnieri, and James Parker. PLDI 2022. [.pdf, artifact]
REST: Integrating Term Rewriting with Program Verification by Zachary Grannan, Niki Vazou, Eva Darulova, and Alexander J. Summers. ECOOP 2022. [.pdf, artifact]
2021
STORM: Refinement Types for Secure Web Applications by Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, and Ranjit Jhala. OSDI 2021. [.pdf]
Refinement Types: A Tutorial by Ranjit Jhala and Niki Vazou. Foundations and Trends® in Programming Languages . [.pdf]
2020
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell by Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou. OOPSLA 2020. [.pdf]
Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell by Martin Handley, Niki Vazou, and Graham Hutton. POPL 2020. [.pdf]
2019
LWeb: Information Flow Security for Multi-Tier Web Applications by James Parker, Niki Vazou, and Michael Hicks. POPL 2019. [.pdf]
Type-level computations for Ruby libraries by Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S Foster, and David Van Horn. PLDI 2019. [.pdf]
2018
Refinement Reflection: Complete Verification with SMT by Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan Scott, Ryan Newton, Philip Wadler, and Ranjit Jhala. POPL 2018. [.pdf, slides, video]
Gradual Liquid Type Inference by Niki Vazou, Éric Tanter and David Van Horn. OOPSLA 2018. [.pdf, slides] Best Paper Award
Theorem Proving for All by Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton. Haskell 2018. [.pdf, .html, slides]
Refinement Types for Ruby by Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeff Foster, and Emina Torlak. VMCAI, 2018. VMCAI 2018. [.pdf]
2017
- A Tale of Two Provers by Niki Vazou, Leonidas Lampropoulos, and Jeff Polakow. Haskell 2017. [.pdf, .slides]
2016
- From Monads to Effects and Back by Niki Vazou and Daan Leijen. PADL 2016. [.pdf]
2015
Bounded Refinement Types by Niki Vazou, Alexander Bakst, and Ranjit Jhala. ICFP 2015. [.pdf, slides, video]
Type Targeted Testing by Eric L. Seidel, Niki Vazou, Ranjit Jhala. ESOP 2015. [.pdf]
2014
Refinement Types for Haskell by Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. ICFP 2014. [.pdf, slides, video]
LiquidHaskell: Experience with Refinement Types in the Real World by Niki Vazou, Eric L. Seidel, and Ranjit Jhala. Haskell 2014. [.pdf]
2013
- Abstract Refinement Types by Niki Vazou, Patric M. Rondon, and Ranjit Jhala. ESOP 2013. [.pdf, slides]
2011
- Memory Safety and Race Freedom in Concurrent Programming with Linear Capabilities by Niki Vazou, Michalis Papakyriakou, and Nikolaos Papaspyrou. FedCSIS 2011. [.pdf]