Peter-Michael Osera—Publications

Refereed Papers

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

Peter-Michael Osera. Programming assistance for type-directed programming (extended abstract). In Type-driven Development (TyDe), 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), 2016. [ pdf ]

Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis. In Programming Language Design and Implementation (PLDI), 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), 2013. [ pdf | acm ]

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

Peter-Michael Osera, Vilhelm Sjöberg, and Steve Zdancewic. Dependent interoperability. In Programming Languages Meet Program Verification (PLPV), 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, 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, 2013. [ pdf ]

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

Theses

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

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

Invited Talks

Peter-Michael Osera. Programs that make themselves (for everyone!). Talk given at Grinnell College Faculty Colloquium, 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), 2016.

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

Mark C. Lewis, Douglas Blank, Kim Bruce, and Peter-Michael Osera. Uncommon teaching languages. In Symposium on Computer Science Education (SIGCSE), 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), 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), 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), 2015. [ acm ]

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

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

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

Student Projects

Kevin Connors, Reilly Grant, Zegall Segall, and Peter-Michael Osera. Semi-automated program synthesis. Summer MAP 2016, 2016.

Jianting Chen, Medha Gopalaswamy, Prabir Pradhan, Sooji Son, and Peter-Michael Osera. Introducing ORC2 A: A proof assistant for computer science pedagogy. Summer MAP 2016, 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.