Peter-Michael Osera—Publications

Refereed Papers

Peter-Michael Osera and David Wonnacott. A blocks-based language for program correctness proofs. In 2017 IEEE Blocks and Beyond Workshop (B&B), October 2017. [IEEE]

Jianting Chen, Medha Gopalaswamy, Prabir Pradhan, Sooji Son, and Peter-Michael Osera. ORC²A: A proof assistant for undergraduate education. In Symposium on Computer Science Education (SIGCSE), March 2017. [pdf | acm]

Peter-Michael Osera. Programming assistance for type-directed programming (extended abstract). In Type-driven Development (TyDe), September 2016. [pdf]

Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. Example-directed synthesis: A type-theoretic interpretation. In Principles of Programming Languages (POPL), September 2016. [pdf]

Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis. In Programming Language Design and Implementation (PLDI), June 2015. [pdf | acm]

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++. In Object-Oriented Programming, Systems, Languages & Applications (OOPSLA), October 2013. [pdf | acm]

Peter-Michael Osera and Steve Zdancewic. Teaching induction with functional programming and a proof assistant. In SPLASH Educators Symposium (SPLASH-E), October 2013. [pdf]

Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent interoperability. In Programming Languages Meet Program Verification (PLPV), January 2012. [pdf | acm]

Technical Reports

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, University of Pennsylvania, March 2013. [pdf]

Peter-Michael Osera, Richard Eisenberg, Christian Delozier, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. Core ironclad. CIS Technical Report #MS-13-06, University of Pennsylvania, July 2013. [pdf]

Peter-Michael Osera, Vilhelm Sjoberg, and Steve Zdancewic. Dependent interoperability. CIS Technical Report #MS-CIS-11-21, University of Pennsylvania, March 2012. [pdf]

Theses

Peter-Michael Osera. Program Synthesis with Types. PhD thesis, University of Pennsylvania, July 2015. [pdf]

Peter-Michael Osera. Join diesel: Concurrency primitives for diesel. Undergraduate research thesis, University of Washington, December 2005. [pdf]

Invited Talks

Peter-Michael Osera. Programs that make themselves (for everyone!). Talk given at Grinnell College Faculty Colloquium, November 2016.

Janet Davis, Valerie Galluzzi, Nery Chapeton-Lamas, Peter-Michael Osera, and Ali Sekmen. Finding your kind of teaching school: Different paces at different places. In ACM Richard Tapia Celebration of Diversity in Computing (TAPIA), September 2016.

Peter-Michael Osera. Program synthesis with types. Talk given at University of Iowa (October) and University of Chicago (June), 2015—2016.

Mark C. Lewis, Douglas Blank, Kim Bruce, and Peter-Michael Osera. Uncommon teaching languages. In Symposium on Computer Science Education (SIGCSE), March 2016.

Charlie Garrod, Jeffrey Forbes, Colleen Lewis, and Peter-Michael Osera. Mentoring student teaching assistants for computer science. In Symposium on Computer Science Education (SIGCSE), March 2016.

Peter-Michael Osera. Program synthesis with types. Talk given at Smith College, Seattle University, Pomona College, Grinnell College, University of Puget Sound, and Carnegie Mellon University, 2015.

Peter-Michael Osera and Steve Zdancewic. Making proof tutors out of proof assistants. Workshop on Programming Languages Technology for Massive Open Online Courses (PLOOC), June 2015.

Nick Parlante, Julie Zelenski, Peter-Michael Osera, Marty Stepp, Mark Sherriff, Luther Tychonievich, Ryan Layer, Suzanne J. Matthews, Allison Obourn, David R. Raymond, Josh Hug, and Stuart Reges. Nifty assignments. In Symposium on Computer Science Education (SIGCSE), March 2015. [acm]

Peter-Michael Osera and Steve Zdancewic. Teaching induction with functional programming and a proof assistant. ExCAPE Annual Meeting, October 2014.

Peter-Michael Osera and Brent Yorgey. Making induction meaningful, recursively. In Symposium on Computer Science Education (SIGCSE), March 2014. [acm]

Peter-Michael Osera. Safe, expressive language interoperability. Off the Beaten Track (OBT), January 2012. [pdf]

Student Projects

Kevin Connors, Reilly Grant, Zachary Segall, and Peter-Michael Osera. Semi-automated program synthesis. Invited talk delivered at the 2016 Midwest PL Summit, December 2016.

Jianting Chen, Medha Gopalaswamy, Prabir Pradhan, Sooji Son, and Peter-Michael Osera. Introducing ORC²A: A proof assistant for computer science pedagogy. Poster presented at the 2016 Midwest PL Summit, December 2016.

Nathan Close, Amalia Hawkins, Sworupini Sureshkumar, Peter-Michael Osera, Lyle Ungar, and Steve Zdancewic. Judgment of code style. Senior design project, University of Pennsylvania, 2014.