Niki Vazou

56 papers A* 4A 5B 2C 9Journal 31Unranked 2
YearRankTypeTitle / Venue / Authors
2025 J jnl
Circuit Width Estimation via Effect Typing and Linear Dependency.
ACM Trans. Program. Lang. Syst.
Andrea Colledan, Ugo Dal Lago, Niki Vazou
2024 J jnl
Mechanizing Refinement Types.
Proc. ACM Program. Lang.
Michael Borkowski, Niki Vazou, Ranjit Jhala
2024 B conf
OBRA: Oracle-Based, Relational, Algorithmic Type Verification.
APLAS
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
2024 C ed.
Proceedings of the 17th ACM SIGPLAN International Haskell Symposium, Haskell 2024, Milan, Italy, September 6-7, 2024
Haskell
Niki Vazou, J. Garrett Morris
2023 J jnl
Flux: Liquid Types for Rust.
Proc. ACM Program. Lang.
Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala
2023 C ed.
Proceedings of the 16th ACM SIGPLAN International Haskell Symposium, Haskell 2023, Seattle, WA, USA, September 8-9, 2023
Haskell
Trevor L. McDonell, Niki Vazou
2022 J jnl
ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification.
CoRR
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker
2022 A* conf
ANOSY: approximated knowledge synthesis with refinement types for declassification.
PLDI
Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker
2022 C conf
Coinduction inductively: mechanizing coinductive proofs in Liquid Haskell.
Haskell
Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou
2022 J jnl
Flux: Liquid Types for Rust.
CoRR
Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala
2022 C conf
How to safely use extensionality in Liquid Haskell.
Haskell
Niki Vazou, Michael Greenberg
2022 C conf
Liquid proof macros.
Haskell
Henry Blanchette, Niki Vazou, Leonidas Lampropoulos
2022 J jnl
Mechanizing Refinement Types (extended).
CoRR
Michael Borkowski, Niki Vazou, Ranjit Jhala
2022 J jnl
REST: Integrating Term Rewriting with Program Verification (Artifact).
Dagstuhl Artifacts Ser.
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 J jnl
REST: Integrating Term Rewriting with Program Verification (Extended Version).
CoRR
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 A conf
REST: Integrating Term Rewriting with Program Verification.
ECOOP
Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers
2022 J jnl
Safe couplings: coupled refinement types.
Proc. ACM Program. Lang.
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
2022 — conf
Verified Causal Broadcast with Liquid Haskell.
IFL
Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper
2022 J jnl
Verified Causal Broadcast with Liquid Haskell.
CoRR
Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper
2021 J jnl
Functional Extensionality for Refinement Types.
CoRR
Niki Vazou, Michael Greenberg
2021 J jnl
Refinement Types: A Tutorial.
Found. Trends Program. Lang.
Ranjit Jhala, Niki Vazou
2021 A* conf
STORM: Refinement Types for Secure Web Applications.
OSDI
Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala
2020 J jnl
LIO*: Low Level Information Flow Control in F.
CoRR
Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou
2020 J jnl
Liquidate your assets: reasoning about resource usage in liquid Haskell.
Proc. ACM Program. Lang.
Martin A. T. Handley, Niki Vazou, Graham Hutton
2020 J jnl
Refinement Types: A Tutorial.
CoRR
Ranjit Jhala, Niki Vazou
2020 J jnl
Verifying replicated data types with typeclass refinements in Liquid Haskell.
Proc. ACM Program. Lang.
Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou
2019 J jnl
LWeb: Information Flow Security for Multi-tier Web Applications.
CoRR
James Parker, Niki Vazou, Michael Hicks
2019 J jnl
LWeb: information flow security for multi-tier web applications.
Proc. ACM Program. Lang.
James Parker, Niki Vazou, Michael Hicks
2019 A* conf
PLAS 2019: ACM SIGSAC Workshop on Programming Languages and Analysis for Security.
CCS
Piotr Mardziel, Niki Vazou
2019 — ed.
Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security, CCS 2019, London, United Kingdom, November 11-15, 2019
PLAS@CCS
Piotr Mardziel, Niki Vazou
2019 J jnl
Type-Level Computations for Ruby Libraries.
CoRR
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
2019 A* conf
Type-level computations for Ruby libraries.
PLDI
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn
2018 J jnl
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell).
CoRR
Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton
2018 J jnl
Gradual Liquid Type Inference.
CoRR
Niki Vazou, Éric Tanter, David Van Horn
2018 J jnl
Gradual liquid type inference.
Proc. ACM Program. Lang.
Niki Vazou, Éric Tanter, David Van Horn
2018 — ed.
Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2018, St. Louis, MO, USA, September 27, 2018
TyDe@ICFP
Richard A. Eisenberg, Niki Vazou
2018 B conf
Refinement Types for Ruby.
VMCAI
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
2018 J jnl
Refinement reflection: complete verification with SMT.
Proc. ACM Program. Lang.
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
2018 — conf
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl).
Haskell@ICFP
Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton
2017 C conf
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq.
Haskell
Niki Vazou, Leonidas Lampropoulos, Jeff Polakow
2017 J jnl
Deriving Law-Abiding Instances.
CoRR
Ryan G. Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala
2017 J jnl
Refinement Reflection: Complete Verification with SMT.
CoRR
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, Ranjit Jhala
2017 J jnl
Refinement Types for Ruby.
CoRR
Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak
2016 C conf
From Monads to Effects and Back.
PADL
Niki Vazou, Daan Leijen
2016 — —
Liquid Haskell: Haskell as a Theorem Prover.
Niki Vazou
2016 J jnl
Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).
CoRR
Niki Vazou, Ranjit Jhala
2016 J jnl
Verified Parallel String Matching in Haskell.
CoRR
Niki Vazou, Jeff Polakow
2015 J jnl
Bounded Refinement Types.
CoRR
Niki Vazou, Alexander Bakst, Ranjit Jhala
2015 A conf
Bounded refinement types.
ICFP
Niki Vazou, Alexander Bakst, Ranjit Jhala
2015 A conf
Type Targeted Testing.
ESOP
Eric L. Seidel, Niki Vazou, Ranjit Jhala
2014 J jnl
From Safety To Termination And Back: SMT-Based Verification For Lazy Languages.
CoRR
Niki Vazou, Eric L. Seidel, Ranjit Jhala
2014 C conf
LiquidHaskell: experience with refinement types in the real world.
Haskell
Niki Vazou, Eric L. Seidel, Ranjit Jhala
2014 A conf
Refinement types for Haskell.
ICFP
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones
2014 J jnl
Type Targeted Testing.
CoRR
Eric L. Seidel, Niki Vazou, Ranjit Jhala
2013 A conf
Abstract Refinement Types.
ESOP
Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala
2011 C conf
Memory Safety and Race Freedom in Concurrent Programming Languages with Linear Capabilities.
FedCSIS
Niki Vazou, Michalis A. Papakyriakou, Nikolaos Papaspyrou