Loading...

Marianna Rapoport

I am a PhD student at the University of Waterloo's school of computer science, in the programming languages research group. My advisor is Ondřej Lhoták.

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. In my PhD I have worked on a core calculus for the Scala programming language.

My projects can be found on github and gitlab.

contact
publications
papers
  • The Future Is Ours: Prophecy Variables in Separation Logic.
    Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, MR, Amin Timany, Derek Dreyer, Bart Jacobs.
    POPL 2020

  • A Path To DOT: Formalizing Fully Path-Dependent Types.
    MR, Ondřej Lhoták.
    OOPSLA 2019
    Distinguished artifact award
    paper | proof | talk

  • A Simple Soundness Proof for Dependent Object Types.
    MR, Ifaz Kabir, Paul He, Ondřej Lhoták.
    OOPSLA 2017
    Distinguished artifact award
    pdf | proof | talk

  • Mutable WadlerFest DOT.
    MR, Ondřej Lhoták.
    FTfJP 2017
    pdf | proof
  • Who You Gonna Call? Analyzing Web Requests in Android Applications.
    MR, Philippe Suter, Erik Wittern, Ondřej Lhoták, Julian Dolby.
    MSR 2017
    pdf | code
  • Type-Based Call Graph Construction Algorithms for Scala.
    Karim Ali, MR, Ondřej Lhoták, Julian Dolby, Frank Tip. TOSEM 2015
    pdf | code
  • Precise data-flow analysis in the presence of correlated method calls.
    MR, Ondřej Lhoták, Frank Tip.
    SAS 2015
    Radhia Cousot best young researcher paper award
    pdf | poster | code
  • Constructing Call Graphs of Scala Programs.
    Karim Ali, MR, Ondřej Lhoták, Julian Dolby, Frank Tip.
    ECOOP 2014
    Distinguished artifact award
    pdf | code

technical reports
  • A Path To DOT: Formalizing Fully Path-Dependent Types.
    MR, Ondřej Lhoták. arXiv: 1904.07298. University of Waterloo, 2019

  • A Simple Soundness Proof for Dependent Object Types.
    MR, Ifaz Kabir, Paul He, Ondřej Lhoták. arXiv: 1706.03814. University of Waterloo, 2017

  • Mutable WadlerFest DOT.
    MR, Ondřej Lhoták. arXiv:1611.07610. University of Waterloo, 2016

theses
  • A Path to DOT: Formalizing Scala with Dependent Object Types.
    PhD thesis, submitted in December 2019
    pdf | proofs

  • Data-flow analysis in the presence of correlated calls.
    Masters thesis, University of Waterloo, 2014
    pdf | code
service
past
blog
This is my blog.
movies
I like movies.