Elizaveta Vasilenko

dblp:329/8707 · DBLP profile ↗
← Back
2ranked-venue papers
2as first author
2since 2021 · last 2024
0000-0001-5983-3347ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 2 · 2 first-author · 2 since 2021
YearPublicationVenuePosition
2024 OBRA: Oracle-Based, Relational, Algorithmic Type Verification
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
APLAS1
2022 Safe couplings: coupled refinement types
abstract
We enhance refinement types with mechanisms to reason about relational properties of probabilistic computations. Our mechanisms, which are inspired from probabilistic couplings, are applicable to a rich set of probabilistic properties, including expected sensitivity, which ensures that the distance between outputs of two probabilistic computations can be controlled from the distance between their inputs. We implement our mechanisms in the type system of Liquid Haskell and we use them to formally verify Haskell implementations of two classic machine learning algorithms: Temporal Difference (TD) reinforcement learning and stochastic gradient descent (SGD). We formalize a fragment of our system for discrete distributions and we prove soundness with respect to a set-theoretical semantics.
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
Proc. ACM Program. Lang.1