Niki Vazou
where else to find them
linkedin:niki-vazou-6258aa2b
what they talk about
all 8 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2023
- OOPSLA2 editions2018–2020
all 11 in the filters
on a stage with
all 24 in the filters
who talks about the same things
- Ranjit Jhala19 talks
- Yiyun Liu5 talks
- Neel Krishnaswami10 talks
- Philip Wadler14 talks
- Nadia Polikarpova24 talks
- Peter Müller28 talks
| title | conference | date |
|---|---|---|
| Liquid Haskell: Verification with Refinement Types | Lambda World 2024 | 2024-10-02 |
Liquid Haskell is a GHC plugin that checks refinement types and lets Haskell programs carry SMT-checkable predicates; it proves safe indexing and non-division… | ||
| Refinement Types from Light to Deep Verification | PLMW @ POPL 2024 | 2024-01-17 |
Shows a working Liquid Haskell plugin integrated with GHC that uses SMT-backed refinement types to prove light properties like safe indexing and… | ||
| Mechanizing Refinement Types | POPL 2024 | 2024-01-14 |
Introduces λRF, a core calculus that actually combines semantic subtyping with parametric polymorphism and proves soundness; develops two mechanizations: one… | ||
| Welcome | Haskell 2023 | 2023-09-08 |
Conference opens with two practical logistics items: two lightning talks slots (one at the end of day, one tomorrow before lunch) with a sign‑up form on the… | ||
| PC Chair Report | Haskell 2023 | 2023-09-08 |
Program committee reports 15 submissions this year (12 regular papers, 1 demo, 1 experience report, 1 functional pearl) and a 53% acceptance rate after three… | ||
| Flux: Liquid Types for Rust | PLDI 2023 | 2023-06-17 |
Flux implements a novel refined type system for Rust as a plug-in to the Rust compiler that indexes mutable locations, introduces strong references for precise… | ||
| How to Safely Use Extensionality in Liquid Haskell | Haskell Symposium 2022 | 2022-09-15 |
Shows that the naive functional extensionality axiom in Liquid Haskell is inconsistent with semantic subtyping and polymorphism, gives a concrete… | ||
| Liquid Proof Macros | Haskell Symposium 2022 | 2022-09-15 |
Liquid Proof Macros is an extensible metaprogramming framework that uses Template Haskell to generate Liquid Haskell proof terms via a tactic-like DSL, and it… | ||
| Coinduction Inductively: Mechanizing Coinductive Proofs in Liquid Haskell | Haskell Symposium 2022 | 2022-09-15 |
Mechanizes coinductive proofs inside Liquid Haskell by encoding coinduction two ways: indexed coinduction (use a natural-number index to reduce stream equality… | ||
| Safe Couplings: Coupled Refinement Types | ICFP 2022 | 2022-09-11 |
Enhances refinement types with a coupling-based connective that captures relational properties like expected sensitivity and proves that output-distance is… | ||
| ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification | PLDI 2022 | 2022-06-13 |
ANOSY verifies attacker-knowledge approximations and synthesizes posterior-update functions using refinement types, then checks them with Liquid Haskell and an… | ||
| RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code | PLDI 2022 | 2022-06-13 |
RustHornBelt gives a formal, mechanized bridge between RustHorn-style automatic specs and RustBelt’s unsafe-code semantics: a Coq model built on Iris… | ||
| STORM: Refinement Types for Secure Web Applications | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
Storm is a web framework that enforces data-dependent security policies at compile time via a Security Typed ORM that refines MVC types with logical… | ||
| Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell | OOPSLA 2020 | 2020-11-15 |
Extension to Liquid Haskell adds refined typeclasses in Liquid Haskell so class laws become checkable at Core; the implementation verifies laws for 34… | ||
| Gradual Liquid Type Inference | OOPSLA 2018 | 2018-11-07 |
Combines Liquid Haskell’s liquid refinement type inference with gradual refinement types to solve two problems: global, non-modular inference that needs… | ||
| LiquidHaskell: Liquid Types for Haskell | Typelevel Summit NYC 2017 | 2017-03-23 |
Code deficiencies and bugs constitute an unavoidable part of software systems. In safety-critical systems, like aircrafts or medical equipment, even a single… | ||
| (...) How to turn (Liquid) Haskell into a theorem prover | Lambda Days 2017 | 2017-02-09 |
Claims a lightweight way to retro-fit theorem proving into Haskell by reflecting function definitions into output refinement types so their code becomes logic… | ||
| nothing matches | ||