addressalign-toparrow-leftarrow-rightbackbellblockcalendarcameraccwcheckchevron-downchevron-leftchevron-rightchevron-small-downchevron-small-leftchevron-small-rightchevron-small-upchevron-upcircle-with-checkcircle-with-crosscircle-with-pluscrossdots-three-verticaleditemptyheartexporteye-with-lineeyefacebookfolderfullheartglobegmailgooglegroupshelp-with-circleimageimagesinstagramFill 1linklocation-pinm-swarmSearchmailmessagesminusmoremuplabelShape 3 + Rectangle 1ShapeoutlookpersonJoin Group on CardStartprice-ribbonprintShapeShapeShapeShapeImported LayersImported LayersImported Layersshieldstartickettrashtriangle-downtriangle-uptwitteruserwarningyahoo


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.


Join or login to comment.

  • Harold C.

    I have posted the ideas for the Haskell course:!topic/lambda-lounge-ut/-YPSH_efYEs

    ps: car problems just before yesterday's Coq presentation - bummer!

    August 13, 2014

  • Casey A.

    Bummed i had to leave a bit early. Good presentation even though I didn't know anything about Coq until tonight I found it informative. Can anyone tell me what happened with the Haskell group after? I really want to be part of that

    August 12, 2014

    • Ben M.

      Harold wasn't able to make it out tonight so the Haskell break-out session didn't happen tonight. We will start next month. Join the google group mailing list if you haven't already and we may discuss the plans with the group:­

      August 12, 2014

  • Matt

    Good presentation. Thanks.

    August 12, 2014

  • Matt M.

    Sorry I'll miss this one. I'll be at the IFIP WG Functional Programming meeting that week.

    July 10, 2014

28 went

Our Sponsors

  • Red Brain Labs

    Recording gear for the meetings, occasional meals, misc. costs

People in this
Meetup are also in:

Sign up

Meetup members, Log in

By clicking "Sign up" or "Sign up using Facebook", you confirm that you accept our Terms of Service & Privacy Policy