| Irene Yoon Office : INRIA Paris, C332 E-mail : euisun.yoon@inria.fr GitHub : euisuny GitLab : eyoon DBLP Google Scholar ORCID Research interests: Logics and semantics of programming languages, formal verification, functional programming. |  |
Hello, internet. I like writing proofs and programs (especially programs as proofs, via the Coq proof assistant).
I am currently a postdoctoral researcher at the Cambium research team of Inria Paris.
Previously, I obtained my Ph.D. at the University of Pennsylvania under the direction of Steve Zdancewic, and
obtained my Bachelor of Science (B.S.) at Cornell University.
Research
Drafts
- Velliris: A Relational Separation Logic for LLVM IR.
Irene Yoon, Simon Spies, Lennard Gäher, Youngju Song, Derek Dreyer, Steve Zdancewic.
Draft available upon request.
Publications
- 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.
Irene Yoon.
POPL 2020 Student Research Competition. 3rd Place, Graduate Category. [poster]
Thesis
- Modular Semantics and Metatheory for LLVM IR.
Euisun Yoon.
Doctoral Thesis, University of Pennsylvania, Dec 2023. [pdf]
[TeX style sheet]
Notes
- Freedom for Proofs!
Representation Independence is More than Parametricity.
University of Pennsylvania WPE-II Manuscript. June 2021. [pdf] [slides]
Education
- Ph.D. Computer Science
University of Pennsylvania, December, 2023.
Advisor: Steve Zdancewic - B.S. Computer Science
Cornell University, May 2019.
Professional Experience
- Postdoctoral Researcher. Inria.
Paris, France. Current. - 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. - Explore Microsoft Intern. Microsoft.
San Francisco, CA, USA. Summer 2017.
Invited Seminars
- 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.
Teaching
- CIS 5520 Advanced Functional Programming (Teaching Assistant). University of Pennsylvania. Fall 2023.
- CIS 500 Software Foundations (Teaching Assistant). University of Pennsylvania. Fall 2020.
- CS 2043 UNIX Tools & Scripting (Teaching Assistant). Cornell University. Spring 2019.
- CS 4110 Programming Languages & Logics (Teaching Assistant). Cornell University. Fall 2018.
- CS 3110 Functional Programming (Head Consultant). Cornell University. Spring 2018.
Service
- Program Committee: Coq Workshop 2024, HOPE 2024, CPP 2025.
- TOPLAS (2022) Reviewer.
- Artifact Evaluation Committee: PLDI 2021, PLDI 2022.
- Student Volunteer: POPL 2020, PLDI 2020.
- Penn PLClub Seminar Coordinator. Spring 2020 - Spring 2022.
- President, Cornell Association of Computer Science Undergraduates (ACSU). December 2017 - December 2018.
- Instructor, Women in Computing at Cornell (WICC) LearnCS High School Program. February 2016 - June 2016.
