I'm a sixth year Ph.D. student with the programming languages research group and ExCape group at Penn advised by Steve Zdancewic.

Research

My research spans the theory and implementation of programming languages and systems. In particular, I try to bridge the gap between type theory and practical software development concerns by seeking out real-world applications of the former towards tools and language features for the latter. These concerns include concurrency, language interoperability, low-level software safety, and computer science education.

Program Synthesis and Types

Program synthesis is the process by which we derive programs from specification. Traditionally a pursuit of the formal methods community, program synthesis has strong ties with goal-oriented programming and type/term inference in dependently-typed programming languages. We are investigating how rich types can make better the process of program synthesis as well as how types and synthesis can allow for new, goal-based programming paradigms.

Ironclad C++

(With Milo Martin, Christian DeLozier, Santosh Nagarakatte, and Richard Eisenberg). Traditional inquiries into the safety of low languages have focused exclusively on C. Our work extends previous efforts for C temporal and spatial memory safety to C++. Unlike C, good C++ code is type-safe, affording us extra information during alias we can leverage to make pointer checks more efficient. Furthermore, C++ is a rich enough language that we can code up safe pointers as libraries rather than additional language primitives. We exploit these facts in identifying a type-safe subset of C++, Ironclad C++, that, when using our safe libraries, guarantees reasonably performant memory safety.

Language Interoperability

(With Vilhelm Sj÷berg). Most software systems are not created with a single language but instead with a collection of languages each carefully chosen for the task at hand. We investigated the sorts runtime checks and machinery involved in building interoperability layers between richly-typed, e.g., dependently-typed or linear types, and simply- or untyped languages.

Join Diesel (@UW)

(With Craig Chambers). I investigated the integration of Join Calculus-style primitives in the spirit of Polyphonic C# and into Diesel. Our main challenge was ensuring that the semantics of join-style function calls played nicely with the classless objects, multimethods, and static type-checking guarantees of Diesel.

Teaching

I am the TA coordinator for the CIS introductory series. I created the department's intro TA training program in 2011. Since then, I have been responsible for the training of the 70+ TAs of the intro series, assisted by the head TAs of the introductory courses.

During the summer, I am the instructor for Penn's computer science offering in the Summer Academy in Applied Science and Technology (SAAST), a CS1 college-level course packed into a month for exceptional high school students.

I have also been involved with numerous courses and other educational efforts at Penn:

Service

Useful Bits

I keep my hacks and other miscellaneous software publicly available on Github.

Personal

I'm a fervent supporter of the indie game scene and e-sports, in particular Starcraft 2. A few choice links:

Peter-Michael Osera's Facebook profile