Introduction to Coq by Kimball Germane HD

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.