My work centers around creating tools that can prove programs correct before they are run. I am particularly interested in type systems, program verification with proof assistants, and functional programming.
A Path To DOT: Formalizing Fully Path-Dependent Types. Marianna Rapoport, Ondřej Lhoták. arXiv: 1904.07298. University of Waterloo, 2019.
A Simple Soundness Proof for Dependent Object Types. Marianna Rapoport, Ifaz Kabir, Paul He, Ondřej Lhoták. arXiv: 1706.03814. University of Waterloo, 2017.
Mutable WadlerFest DOT.
Marianna Rapoport, Ondřej Lhoták. arXiv:1611.07610.
University of Waterloo, 2016.
masters at University of Waterloo
Waterloo, ON, 2012 - 2014
bachelors at MIREA
Moscow, Russia, 2008 - 2012
Automated Reasoning Group with Rustan Leino
Seattle, WA, 2019
Max Planck Institute for Software Systems
Foundations of Programming Group with Derek Dreyer
Saarbrücken, Germany, 2018
IBM Watson Research Centre
York Town Heights, NY, 2015
San Francisco, CA, 2013
DeepSpec Summer School
Philadelphia, PA, Jul 2017
Oregon Programming Languages Summer School
Eugene, OR, Jun 2016
Midland Graduate Summer School in the Foundations of Computing Sciences
Nottingham, UK, Apr 2012
School in Applied Functional Programming
Utrecht, Netherlands, Aug 2010