The Pioneer PL research group at Grinnell College, led by Peter-Michael Osera investigates problems at the intersection of programming language theory, systems, human-computing interaction, and computer science education.

Current Projects

  • Scythe: Program synthesis is the process by which we derive programs automatically from specification. Pursued since the 70s by a variety of sub-fields of computer science, program synthesis has strong ties to type-directed programming, type checking, and type inference. In the Scythe project, we are building type-theoretic foundations for program synthesis and applying those foundations towards building tools to help automate the type-directed programming process. Scythe is generously supported by a NSF EAGER award (CCF-1651817).
  • Orca: Many people believe that there is a fundamental divide between everyday computer programming and formal reasoning. However, the two are closely related; formal reasoning is really just one end of a spectrum of program reasoning that programmers apply daily in their work. We are building an undergraduate-focused proof assistant, Orca, to teach undergraduates how to apply formal reasoning techniques towards practical programming problems.


Pioneer PL is an undergraduate-focused research group. It operates primarily during the summers with the assistance of Grinnell’s Mentored Advanced Project program.

Summer 2016 Cohort

  • Jerry Chen
  • Kevin Connors
  • Medha Gopalaswamy
  • Reily Grant
  • Prabir Pradhan
  • Zachary Segall
  • Sooji Son

Summer 2017 Cohort:

  • Myles Becker
  • Liat Berkowtiz
  • Addison Gould
  • Hadley Luker
  • Andrew Mack
  • Eli Most
  • Dhruv Phumbhra
  • Jonathan Sadun
  • Zachary Susag

Summer 2018 Cohort:

  • Bogdan Abaev
  • Elise Brod
  • Shelby Frazier
  • Yash Gupta
  • Griffin Mareske
  • Ankit Pandey
  • Dhruv Phumbhra
  • Lukas Resch