Dependent interoperability. - Peter-Michael Osera; Vilhelm Sjöberg; Steve Zdancewic (PLPV, 2012)

Ironclad C++: a library-augmented type-safe subset of c++. - Christian DeLozier; Richard A. Eisenberg; Santosh Nagarakatte; Peter-Michael Osera; Milo M. K. Martin; Steve Zdancewic (OOPSLA, 2013)

Making induction meaningful, recursively (abstract only). - Peter-Michael Osera; Brent A. Yorgey (SIGCSE, 2014)

Type-and-example-directed program synthesis. - Peter-Michael Osera; Steve Zdancewic (PLDI, 2015)

Nifty Assignments. - Nick Parlante; Julie Zelenski; Peter-Michael Osera; Marty Stepp; Mark Sherriff; Luther A. Tychonievich; Ryan Layer; Suzanne J. Matthews; Allison Obourn; David R. Raymond; Josh Hug; Stuart Reges (SIGCSE, 2015)

Programming assistance for type-directed programming (extended abstract). - Peter-Michael Osera (TyDe@ICFP, 2016)

Example-directed synthesis: a type-theoretic interpretation. - Jonathan Frankle; Peter-Michael Osera; David Walker 001; Steve Zdancewic (POPL, 2016)

Mentoring Student Teaching Assistants for Computer Science (Abstract Only). - Charles Garrod; Jeffrey Forbes 001; Colleen M. Lewis; Peter-Michael Osera (SIGCSE, 2016)

Uncommon Teaching Languages. - Mark C. Lewis; Douglas Blank; Kim Bruce 001; Peter-Michael Osera (SIGCSE, 2016)

ORC2A: A Proof Assistant for Undergraduate Education. - Jianting Chen; Medha Gopalaswamy; Prabir Pradhan; Sooji Son; Peter-Michael Osera (SIGCSE, 2017)

Constraint-based type-directed program synthesis. - Peter-Michael Osera (TyDe@ICFP, 2019)

Compiler Error Messages Considered Unhelpful: The Landscape of Text-Based Programming Error Message Research. - Brett A. Becker; Paul Denny 001; Raymond Pettit; Durell Bouchard; Dennis J. Bouvier; Brian Harrington 001; Amir Kamil; Amey Karkare; Chris McDonald; Peter-Michael Osera; Janice L. Pearce; James Prather (ITiCSE-WGR, 2019)

Unexpected Tokens: A Review of Programming Error Messages and Design Guidelines for the Future. - Brett A. Becker; Paul Denny 001; Raymond Pettit; Durell Bouchard; Dennis J. Bouvier; Brian Harrington 001; Amir Kamil; Amey Karkare; Chris McDonald; Peter-Michael Osera; Janice L. Pearce; James Prather (ITiCSE, 2019)

Modernizing the Mathematics Taught in Computer Science. - Barbara M. Anthony; Mia Minnes; David Liben-Nowell; Peter-Michael Osera (SIGCSE, 2019)

A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete Math. - David G. Wonnacott; Peter-Michael Osera (CoRR, 2019)

What Mathematics Should be Required of Computer Science Majors? - James R. Matthews; John P. Dougherty; Peter-Michael Osera (SIGCSE, 2020)

Automation to soul: reflections on tooling support for mathematics and programming education. - Peter-Michael Osera (J. Comput. Sci. Coll., 2022)

Verifying Chemical Reaction Networks with the Isabelle Theorem Prover. - James I. Lathrop; Peter-Michael Osera; Addison W. Schmidt; Jesse Slater (Allerton, 2023)

Snowflake: Supporting Programming and Proofs. - Oluwatobi Alabi; Anh Vu; Peter-Michael Osera (SIGCSE (2), 2023)

The Purpose of Proof. - Bruce W. Char; Peter-Michael Osera; David G. Wonnacott (SIGCSE (2), 2023)

Notional Machine in Mathematics and Introductory Computer Science Courses. - Eamon Worden; Olivia Song; Peter-Michael Osera (SIGCSE (2), 2023)

Reactamole: functional reactive molecular programming. - Titus H. Klinge; James I. Lathrop; Peter-Michael Osera; Allison Rogers (Nat. Comput., 2024)