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.
- Peter-Michael Osera and Steve Zdancewic. Teaching Induction with Functional Programming and a Proof Assistant. SPLASH-E, 2013. [pdf | slides | poster]
(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.
- Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. Ironclad C++: A Library-Augmented Type-Safe Subset of C++. Object-oriented Programming Systems, Languages, and Applications (OOPSLA), 2013. [pdf (local)]
- Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, and Steve Zdancewic. Ironclad C++: A Library-Augmented Type-Safe Subset of C++. CIS Technical Report #MS-CIS-13-05, 2013. [pdf (local) | pdf (UPenn)]
- Peter-Michael Osera, Richard Eisenberg, Christian DeLozier, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Core Ironclad. CIS Technical Report, #MS-13-06, 2013. [pdf (local) | pdf (UPenn)]
(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.
- 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]
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:
- Homotopy Type Theory Reading Group - Fall 2013 (organizer)
- Penn Institute for Computational Sciences (PICS) C/C++ Bootcamp - Fall 2013 (instructor)
- CIS 277: Introduction to Computer Graphics Techniques - Spring 2013 (co-instructor)
- CIS 110: Introduction to Computer Programming - Fall 2011 (instructor)
- 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)
- 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 founded and act as the current organizer for the CIS education seminar (CISed), a bi-weekly seminar for graduate students and staff interested in Computer Science education and/or an education-focused career in academia.
- I am the faculty sponsor for the University of Pennsylvania League of Legends club.
- I was formerly a CTL graduate fellow for teaching excellence for the 2012-2013 school year.
I keep my hacks and other miscellaneous software publicly available on Github.
- 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.