Next Meetup

Generating Correct Code with Coq
This month's meet-up is presented by Rob Dickerson. Proving properties of programs is an important part of engineering critical systems today, but the interplay between proof systems and code generation could become key to the future of programming languages and everyday software development. This talk will give a brief introduction to the proof assistant Coq, examine Coq's existing extraction mechanism for generating certified code, and take a look at what is on the horizon for proof-based automatic program generation. Rob is a software engineer with more than ten years of experience building systems and teams at places like Square, Inc. and Riot Games. He is currently cooking something up at a stealth mode Brooklyn-based startup. In his free time he enjoys fencing, woodworking, and playing games. Thanks to Blit Tech for sponsoring this month's meet-up.

Innovation Hub

500 East Walnut Street #104 · Columbia, MO

1 comment

    Past Meetups (56)

    What we're about

    Public Group

    devcomo is a monthly user group Columbia, MO that is focused on development and design. Simply put, if it is interesting then it’ll be discussed!

    Members (306)

    Photos (17)

    Find us also at