Refinement types for Haskell N Vazou, EL Seidel, R Jhala, D Vytiniotis, S Peyton-Jones ACM SIGPLAN Notices 49 (9), 269-282, 2014 | 144 | 2014 |

Abstract refinement types N Vazou, PM Rondon, R Jhala European Symposium on Programming, 209-228, 2013 | 91 | 2013 |

Liquidhaskell: Experience with refinement types in the real world N Vazou, EL Seidel, R Jhala ACM SIGPLAN Notices 49 (12), 39-51, 2014 | 46 | 2014 |

Type targeted testing EL Seidel, N Vazou, R Jhala European Symposium on Programming Languages and Systems, 812-836, 2015 | 28 | 2015 |

Bounded Refinement Types N Vazou, A Bakst, R Jhala ICFP, 2015 | 24 | 2015 |

Refinement reflection: complete verification with SMT N Vazou, A Tondwalkar, V Choudhury, RG Scott, RR Newton, P Wadler, ... Proceedings of the ACM on Programming Languages 2 (POPL), 53, 2017 | 17 | 2017 |

Liquid Haskell: Haskell as a theorem prover N Vazou UC San Diego, 2016 | 16 | 2016 |

A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq N Vazou, L Lampropoulos, J Polakow ACM SIGPLAN Notices 52 (10), 63-74, 2017 | 14 | 2017 |

Refinement Types for Ruby M Kazerounian, N Vazou, A Bourgerie, JS Foster, E Torlak International Conference on Verification, Model Checking, and Abstract …, 2018 | 5 | 2018 |

Refinement reflection: complete verification with SMT. PACMPL 2, POPL, 53: 1–53: 31 N Vazou, A Tondwalkar, V Choudhury, RG Scott, RR Newton, P Wadler, ... | 5 | 2018 |

From Monads to Effects and Back N Vazou, D Leijen International Symposium on Practical Aspects of Declarative Languages, 169-186, 2016 | 5 | 2016 |

Meta-F: Proof Automation with SMT, Tactics, and Metaprograms G Martínez, D Ahman, V Dumitrescu, N Giannarakis, C Hawblitzel, ... European Symposium on Programming, 30-59, 2019 | 4 | 2019 |

LWeb: information flow security for multi-tier web applications J Parker, N Vazou, M Hicks Proceedings of the ACM on Programming Languages 3 (POPL), 75, 2019 | 4 | 2019 |

Refinement Reflection (or, how to turn your favorite language into a proof assistant using SMT) N Vazou, R Jhala arXiv preprint arXiv:1610.04641, 2016 | 4 | 2016 |

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages N Vazou, EL Seidel, R Jhala arXiv preprint arXiv:1401.6227, 2014 | 3 | 2014 |

Remarrying effects and monads N Vazou, D Leijen Proceedings of MSFP, 2014 | 3 | 2014 |

Programming Languages and Systems E Seidel, N Vazou, R Jhala | 2 | 2015 |

Gradual liquid type inference N Vazou, É Tanter, D Van Horn Proceedings of the ACM on Programming Languages 2 (OOPSLA), 132, 2018 | 1 | 2018 |

Theorem proving for all: equational reasoning in Liquid Haskell N Vazou, J Breitner, R Kunkel, D Van Horn, G Hutton | 1 | 2018 |

Memory safety and race freedom in concurrent programming languages with linear capabilities N Vazou, M Papakyriakou, N Papaspyrou 2011 Federated Conference on Computer Science and Information Systems …, 2011 | 1 | 2011 |