This tech talk has been canceled and will be rescheduled. We apologize for the inconvenience!
This talk will be live-streamed at: https://www.youtube.com/c/GaloisInc/live
Abstract:
“My programs just write themselves!” This phrase is frequently exclaimed by users of functional programming languages with advanced type systems who observe that rich types often guide them directly towards correct programs. In reality, this paradigm known as type-directed programming is far from automatic. To take advantage of rich types, a developer must reason carefully and precisely about the types of their programs, a seemingly mechanical, yet cognitively demanding process.
To this end, I will describe our efforts to understand better and ultimately automate the type-directed programming process. Our primary technique is type-directed program synthesis, where we derive synthesis algorithms from type checking systems, allowing us to build synthesizers that take advantage of rich types. In addition to describing the type-directed program synthesis process, I will present Scythe, a program assistant for type-directed programming in the Haskell programming language, and our next steps towards evolving Scythe into a next-generation live programming assistant built upon program synthesis technology.
Bio:
Peter-Michael Osera received his B.S. in Computer Science and Applied and Computational Math Sciences and B.A. in the Comparative History of Ideas from the University of Washington in 2006 and received his Ph.D. in Computer Science from the University of Pennsylvania in 2015. He is currently an Assistant Professor of Computer Science at Grinnell College. Peter-Michael’s mission is to help people harness the power of computation in its many forms, in particular, through computer programming. He does this by studying problems at the intersection of programming languages and systems, human-computing interaction, and computer science education.