Hello, internet. I like writing proofs and programs (especially programs as proofs, via the Coq proof assistant
- I defended my Ph.D. (Nov 2023)!
- Starting February 2024, I will be a postdoctoral researcher at the
Cambium research team of
- 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]
- Ph.D. Computer Science
University of Pennsylvania, December, 2023 (expected).
Advisor: Steve Zdancewic
- B.S. Computer Science
Cornell University, May 2019.
- 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.