Come learn about the proof assistant Coq from Kimball Germane!
6:00 - 6:30pm Introductions and dinner
We'll use this time to get to know each other. Dinner will be provided. Please RSVP so we can arrange the for the dinner.
The sponsor for this meeting is Savvysherpa.
Introduction to Coq by Kimball Germane
Coq implements a dependently-typed strongly-normalizing programming language that allows users to express formal specifications of programs. Coq assists the user in finding artifacts that meet a specification and from which it can extract a certified implementation in Haskell, Racket, or OCaml automatically. This talk will iterate through a series of increasingly-precise specifications of a commonly-used function and the experience of a Coq user meeting these specifications.
About Kimball Germane
Kimball graduated from BYU where he studied Mathematics, Statistics, and Computer Science. He completed an MS in Computer Science under Dr. Jay McCarthy developing and proving correct a compiler for continuation marks. He is currently a PhD student at the University of Utah under Dr. Matt Might. His research includes finding functional formulations of data-structure operations, discharging contracts at compile time with static analysis, and applying abstract interpretation to probabilistic programs.
Optional Haskell Break-out session
A smaller Haskell group will meet to discuss future plans of working though one or two Haskell courses. This is a great opportunity to finally learn Haskell in the context of a group.