Ron Pressler (https://twitter.com/pressron, https://pron.github.io) presents a talk with title "On the Nature of Abstraction: An introduction to the mathematical analysis of programs" inspired by the papers "Binary Relations for Abstraction and Refinement" by David A Schmidt and "The Existence of Refinement Mappings" by Martín Abadi and Leslie Lamport.
Download the papers at:
There are two main approaches to analysing programs mathematically: representing the program as a formal object, a syntax with some meaning, or as an object representing its possible behaviours, regardless of the language used to encode it. Programming language theory analyses programs using the first approach, while program analysis (formal methods) research uses the latter.
The second, language-agnostic approach will be the focus of the talk, which will be a brief introduction to the mathematical analysis of programs and its core ideas. I will present Kripke structures as a general, language-agnostic, representation of programs, introduce the central principle of abstraction as Galois connections, and finally show an important result that enables a simple yet powerful technique for analysing programs.
Ron Pressler is a veteran programmer, working at Oracle, where he leads the project to add delimited continuations, lightweight concurrency and tail-calls to the Java Virtual Machine.
We meet at ZPG (https://www.uswitch.com/about-us/contact-us/) offices near Tower Bridge (https://goo.gl/maps/qJXZek4fMNU2) with the following schedule:
• 6.30pm: networking, pizza and drinks.
• 7:00pm: presentation starts
Meetup are captured on video and uploaded at https://www.youtube.com/channel/UCEYe-1uDIkjPtuH_qhoybnA