Niki Vazou

According to our database, Niki Vazou authored at least 41 papers between 2011 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

Mechanizing Refinement Types.

Michael Borkowski, Niki Vazou, Ranjit Jhala

Proc. ACM Program. Lang., January, 2024

OBRA: Oracle-Based, Relational, Algorithmic Type Verification.

Elizaveta Vasilenko, Niki Vazou, Gilles Barthe

Proceedings of the Programming Languages and Systems - 22nd Asian Symposium, 2024

2023

Flux: Liquid Types for Rust.

Nico Lehmann, Adam T. Geller, Niki Vazou, Ranjit Jhala

Proc. ACM Program. Lang., 2023

2022

Safe couplings: coupled refinement types.

Elizaveta Vasilenko, Niki Vazou, Gilles Barthe

Proc. ACM Program. Lang., 2022

REST: Integrating Term Rewriting with Program Verification (Artifact).

Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers

Dagstuhl Artifacts Ser., 2022

Mechanizing Refinement Types (extended).

Michael Borkowski, Niki Vazou, Ranjit Jhala

CoRR, 2022

Flux: Liquid Types for Rust.

Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala

CoRR, 2022

REST: Integrating Term Rewriting with Program Verification (Extended Version).

Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers

CoRR, 2022

ANOSY: approximated knowledge synthesis with refinement types for declassification.

Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

Verified Causal Broadcast with Liquid Haskell.

Patrick Redmond, Gan Shen, Niki Vazou, Lindsey Kuper

Proceedings of the 34th Symposium on Implementation and Application of Functional Languages, 2022

How to safely use extensionality in Liquid Haskell.

Niki Vazou, Michael Greenberg

Proceedings of the Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15, 2022

Coinduction inductively: mechanizing coinductive proofs in Liquid Haskell.

Lykourgos Mastorou, Nikolaos Papaspyrou, Niki Vazou

Proceedings of the Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15, 2022

Liquid proof macros.

Henry Blanchette, Niki Vazou, Leonidas Lampropoulos

Proceedings of the Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15, 2022

REST: Integrating Term Rewriting with Program Verification.

Zachary Grannan, Niki Vazou, Eva Darulova, Alexander J. Summers

Proceedings of the 36th European Conference on Object-Oriented Programming, 2022

2021

Refinement Types: A Tutorial.

Ranjit Jhala, Niki Vazou

Found. Trends Program. Lang., 2021

Functional Extensionality for Refinement Types.

Niki Vazou, Michael Greenberg

CoRR, 2021

STORM: Refinement Types for Secure Web Applications.

Nico Lehmann, Rose Kunkel, Jordan Brown, Jean Yang, Niki Vazou, Nadia Polikarpova, Deian Stefan, Ranjit Jhala

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

2020

Verifying replicated data types with typeclass refinements in Liquid Haskell.

Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, Niki Vazou

Proc. ACM Program. Lang., 2020

Liquidate your assets: reasoning about resource usage in liquid Haskell.

Martin A. T. Handley, Niki Vazou, Graham Hutton

Proc. ACM Program. Lang., 2020

LIO*: Low Level Information Flow Control in F.

Jean-Joseph Marty, Lucas Franceschino, Jean-Pierre Talpin, Niki Vazou

CoRR, 2020

2019

LWeb: information flow security for multi-tier web applications.

James Parker, Niki Vazou, Michael Hicks

Proc. ACM Program. Lang., 2019

Type-level computations for Ruby libraries.

Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, David Van Horn

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

PLAS 2019: ACM SIGSAC Workshop on Programming Languages and Analysis for Security.

Piotr Mardziel, Niki Vazou

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Gradual liquid type inference.

Niki Vazou, Éric Tanter, David Van Horn

Proc. ACM Program. Lang., 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

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 Types for Ruby.

Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, Emina Torlak

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2018

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl).

Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton

Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, 2018

2017

Deriving Law-Abiding Instances.

Ryan G. Scott, Vikraman Choudhury, Ryan Newton, Niki Vazou, Ranjit Jhala

CoRR, 2017

A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq.

Niki Vazou, Leonidas Lampropoulos, Jeff Polakow

Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, 2017

2016

Liquid Haskell: Haskell as a Theorem Prover.

Niki Vazou

PhD thesis, 2016

Verified Parallel String Matching in Haskell.

Niki Vazou, Jeff Polakow

CoRR, 2016

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT).

Niki Vazou, Ranjit Jhala

CoRR, 2016

From Monads to Effects and Back.

Niki Vazou, Daan Leijen

Proceedings of the Practical Aspects of Declarative Languages, 2016

2015

Bounded refinement types.

Niki Vazou, Alexander Bakst, Ranjit Jhala

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

Type Targeted Testing.

Eric L. Seidel, Niki Vazou, Ranjit Jhala

Proceedings of the Programming Languages and Systems, 2015

2014

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages.

Niki Vazou, Eric L. Seidel, Ranjit Jhala

CoRR, 2014

Refinement types for Haskell.

Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, Simon L. Peyton Jones

Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, 2014

LiquidHaskell: experience with refinement types in the real world.

Niki Vazou, Eric L. Seidel, Ranjit Jhala

Proceedings of the 2014 ACM SIGPLAN symposium on Haskell, 2014

2013

Abstract Refinement Types.

Niki Vazou, Patrick Maxim Rondon, Ranjit Jhala

Proceedings of the Programming Languages and Systems, 2013

2011

Memory Safety and Race Freedom in Concurrent Programming Languages with Linear Capabilities.

Niki Vazou, Michalis A. Papakyriakou, Nikolaos Papaspyrou

Proceedings of the Federated Conference on Computer Science and Information Systems, 2011