I'm a fourth year Ph.D. student with the programming languages research group at Penn. My battle is against the ever-growing complexity of software. My weapons of choice are the theory and design of programming languages and tools that increase programmer productivity and software reliability in spite of that complexity.
My research advisor is Steve Zdancewic. We have worked on variety of projects related to safe low-level languages and other practical language concerns. We are currently interested in exploring the intersection of programming languages and machine learning for the purposes of building powerful, approximately correct programming tools and systems.
Program Synthesis by Example
How do we choose an appropriate program that meets the user's specification from the obscenely large search space of possible programs? Unlike current approaches that use program verification techniques to refine the search space to a tractable size, we propose instead to use pre-existing code, e.g., example or open source code, to immediately refine the search to a relatively small number of programs. We hypothesize that many times, the code that you wish to synthesize has already been written by someone else. This approach takes advantage of that fact in order to provide reasonably quick program synthesis for everyday programming.
(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.
- Peter-Michael Osera, Richard Eisenberg, Christian DeLozier, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Core Ironclad. Technical Report (Draft), 2012. [pdf]
- Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. Ironclad C++: A Pragmatic Approach for Bringing Type-Safe Programming to C++. In submission to Programming Language Design and Implementation (PLDI), 2013.
(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 are investigating 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.
- Peter-Michael Osera, Vilhelm Sj÷berg, and Steve Zdancewic. Dependent Interoperability. Technical Report MS-CIS-11-21, University of Pennsylvania, 2012. [pdf]
- Peter-Michael Osera, Vilhelm Sj÷berg, and Steve Zdancewic. Dependent Interoperability. Programming Languages Meet Program Verification (PLPV) 2012. [pdf (local) | pdf (ACM)].
- Peter-Michael Osera. Safe, expressive language interoperability. Off the Beaten Track (OBT) 2012. [pdf]
Join Diesel (@UW)
With Craig Chambers, I investigated the integration of Join Calculus-style primitives in the spirit of Polyphonic C# and Cω 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.
- Peter-Michael Osera. Join Diesel: Concurrency Primitives for Diesel. Undergraduate research thesis. December 2005. [pdf]
Teaching and Education
This summer, I will be the instructor for Penn's computer science offering in the Summer Academy in Applied Science and Technology (SAAST).
During the Fall 2011 semester, I was on leave from the PhD program in order to revamp both the content and organization of CIS 110, our introductory course on computer programming. Since then, I have been in charge of organizing and training the TAs for our introductory series --- CIS 110, 120, and 121.
Other courses I've been involved with here at Penn:
- CIS 110: Introduction to Computer Programming - Fall 2011 (instructor), (highlight of the course)
- CIS 190: C++ Programming - Fall 2010 (instructor)
- CIS 193: C# Programming - Spring 2010, 2011 (instructor)
- CIS 399-005: Introduction to Programming in C# - Spring 2009 (TA)
- CIS 262: Automata, Computability, and Complexity - Fall 2008 (grader), Autumn 2009 (TA)
- A Vim mode for Ott: ott.vim (v1)
- plrefgen, a Python script that generates a bibtex file containing standardized crossref entries for a number of popular PL conferences: plrefgen.py (v1)
- GhostKeyboard, a F# program that displays keystrokes and mouse presses that the user executes, useful for accessibility purposes or screencasts where you want to show keystrokes in real-time: GhostKeyboard (v1) [bin | F# src | src+data].
- I am a CTL graduate fellow for teaching excellence for the 2012-2013 school year. As part of my responsibilities as a fellow, I run monthly teaching workshops for the CIS department and the greater UPenn community. The schedule for the workshops is currently forthcoming!
- I am currently the graduate student liason to the CIS faculty. If you are a CIS graduate student and you have any questions, comments, or concerns about the program, feel free to leave a message via Surveymonkey survey
- I co-organize the CIS education lunch which is a bi-weekly seminar for doctoral students interested in Computer Science education and/or an education-focused career in academia. If you would like more information or are interested in attending, please shoot me an email.
- My twitch.tv stream and youtube page where I stream Starcraft 2 ladder games, coaching sessions, casted tournament and league games, and other gaming content.
- Philly Barcraft, where people get together in the Philadelphia area to watch e-sports.
- Rumble in the Bronze, a yearly charity event for Child's Play.