Ph.D. Student of Computer Science
PLClub @ University of Pennsylvania
email : email@example.com
@euisuny on Twitter
@euisuny on GitHub
@euisuny on Goodreads
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.
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.
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]