Topic

Program Verification with Proof Assistants:
The Time Has Come

Speaker

Bob Cotton

When

Monday, November 20, 2017       7:30 PM

Where

Marist College, Hancock Center (Building 14 on map), Room 2023. Park just north of Hancock Center, or in parking lot on south-east corner of Route 9 and Fulton Street. We thank Marist College for hosting the chapter's meetings.

More Information

This program is free and open to the public. Attendees should RSVP at Meetup.com.

All are welcome to join us beforehand for dinner at the Palace Diner at 6:00 PM.

RSVP to ACM Poughkeepsie at  

About the Topic

Software security breaches have become a news staple. While computer hardware has become very reliable, software has not. The ultimate security weapons among computer languages are the proof assistants, such as Coq, F* (FStar), and Idris. These permit computerized proofs of correctness of code. We make an economic case for their likely ascendancy.

Next, we trace some of the ideas and concepts that surround proof verification in both mathematics and programming, and exhibit some of the literature and tools that allow a programmer to learn how to use these languages.

About the Speaker

Bob is the Poughkeepsie ACM program chair and organizer of the Hudson Valley Programmers meetup. He spent 30 years in computing software and support, most recently at the Clearing House in New York. Prior to that he taught mathematics at the University of Pennsylvania, Drexel, Bucknell, and SUNY New Paltz. Bob's interests include two long-standing projects in music and voting theory. He continues to trot for exercise.