Poughkeepsie Chapter of the Association For Computing Machinery

         AAA         CCCCCCC      MMMMM   MMMMM
       A   A       CC     CC     MM MM   MM MM
     AA   AA      CC      C     MM  MM MM  MM
   AAAAAAAAA     CC            MM   MMM   MM
  AA     AA     CC      C     MM    M    MM
 AA     AA     CC     CC     MM         MM
AA     AA      CCCCCCCC     MM         MM
ACM Chapter logo


Program Verification with Proof Assistants:
The Time Has Come


Bob Cotton


Monday, November 20, 2017       7:30 PM


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.

QR code RSVP to ACM Poughkeepsie at   Meetup.com

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.

To Print this Announcement