A Walk-through of Computational Reflection in Coq
Details
This month we are pleased to welcome Gregory Malecha (https://gmalecha.github.io/) as our speaker.
Abstract
Foundational proof assistants such as Coq and Agda leverage the Curry-Howard correspondance and dependent type theory to prove deep properties about mathematics, programming languages, and programs. In this talk, I will give an overview of computational reflection, a proof technique where we write functional programs to prove properties for us. Beyond the concepts of computational reflection, the talk will also highlight some of interesting aspects of Curry-Howard. While the presentation will be done on Coq, it should be accessible to anyone familiar with functional programming.
Note: the presentation will be live coding, and questions and discussion will be highly encouraged.
Bio
Gregory Malecha got his PhD from Harvard in 2015 doing research on program verification and computational reflection. During his graduate studies, he built verified webservers and a database and developed the reflective automation behind the Bedrock program verification system. After graduate school, Gregory did a post-doc with Sorin Lerner at UCSD on verification of safety and stability properties of cyber physical systems with the VeriDrone project ( http://ucsd-pl.github.io/veridrone/papers.html ). Gregory now works at Target on supply chain optimization in Haskell.
Website: https://gmalecha.github.io/
Logistics
The meetup will be at the Thoughtbot location in downtown Boston as usual. Food should be available near the 6:30PM start time, and the talk will begin shortly after that.
Food and beverages will be provided by Thoughtbot.
Streaming
For people who are unable to attend in person, we plan to stream/record the talk. The stream will happen on the Boston Haskell YouTube channel (https://www.youtube.com/channel/UCUCpgCWjaniUkX88wZrK_Ig). Links to the stream will be posted here once it's scheduled.