Please checkout my new website, as this page will become defunct soon.
I am a Ph.D. student advised by Steve Zdancewic at the University of Pennsylvania (Fall 2019 - present).
My research interests lie in programming languages theory, mechanized formal verification, and functional programming.
I received a B.S. in Computer Science from Cornell University (2015 - 2019).
- Formal Reasoning About Layered Monadic Interpreters.
Irene Yoon, Yannick Zakowski, Steve Zdancewic
ICFP 2022. [preprint] [doi] [proof] [repo]
- Modular, Compositional, and Executable Formal Semantics for LLVM IR.
Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, Steve Zdancewic.
ICFP 2021. [pdf] [doi] [repo]
- Geometry Types for Graphics Programming.
Dietrich Geisler, Irene Yoon, Aditi Kabra, Horace He, Yinnon Sanders, Adrian Sampson.
OOPSLA 2020. [pdf] [doi] [repo]
Project page: [url]
- Design Mining for Minecraft Architecture.
Euisun Yoon, Erik Andersen, Bharath Hariharan, Ross Knepper.
AIIDE 2018. [pdf] [doi]
Article from Cornell CIS Department: [url]
Workshops and Presentations
- Equational Proofs of Optimizations with Interaction Trees.
Lucas Silver, Irene Yoon, Yannick Zakowski, Steve Zdancewic.
PERR 2020 (co-located with CAV). Extended Abstract. [abstract]
- Through the Interaction Forest: Modeling Concurrency in Coq.
POPL 2020 Student Research Competition. 3rd Place, Graduate Category. [poster]
- Freedom for Proofs!
Representation Independence is More than Parametricity.
University of Pennsylvania WPE-II Manuscript. June 2021. [pdf] [slides]
- Research Intern. Jane Street Capital.
London, UK. Spring 2023.
- Research Intern. Max Planck Institute for Software Systems (MPI-SWS).
Advisor: Derek Dreyer
Remote. Summer 2021, ongoing collaboration.
- Explore Microsoft Intern. Microsoft.
San Francisco, CA, USA. Summer 2017.
- Formal Reasoning About Layered Monadic Interpreters. Boston University POPV Seminar. December 2022.
- Formal Reasoning About Layered Monadic Interpreters. Cornell PLDG. September 2022.
- Modular, Compositional, and Executable Semantics for LLVM IR. UCSC LSD Seminar. December 2020.