Irene Yoon
Ph.D. Student of Computer Science

PLClub @ University of Pennsylvania
email :

@euisuny on Twitter
@euisuny on GitHub
@euisuny on Goodreads

Curriculum Vitae


I am a second year Ph.D. Student at the University of Pennsylvania.
My main research interests are in programming language theory, type systems, and mechanized formal verification.

Previously, I was an undergraduate at Cornell University, and was part of the Capra research group.


Verified LLVM Semantics (Vellvm) with Interaction Trees

Concurrency in Coq: Denotation of CCS with Interaction Trees

Interaction Trees (ITrees) represent impure and recursive programs in Coq. Weak bisimulation, a method of encapsulating internal interactions within a component, observes behavioral equivalence of ITrees. We use this framework to write a deep embedding of Milner's Calculus of Communicating Systems (CCS), a simple concurrency model, in Coq.

Geometry Types in Graphics Shader Programming

Graphics shader programs (code that runs on the GPU to render graphical objects) rely heavily on computations that involve geometric transformations. We developed a type system that introduces a geometric abstraction to GLSL, providing a natural notion of reference frames at the language-level. [GitHub]

Architectural Design Exploration in Minecraft

Minecraft offers a lenient space for exploring architectural style. [Cornell CIS wrote an article about this project.]


academic honors