Sean Chalmers

Share

Langauge hacker & functional programmer
mankyKitty.github.io
@mankykitty

I’m software developer working in Brisbane. I fell down the statically typed, functional programming rabbit hole about three years ago and I’ve never looked back. Interested in type theory, language hacking, and all manner of neat things that can be done with and without code. Currently digging into UrWeb and ML.

I would enjoy long walks on the beach if the wifi was better.

YOW! Lambda Jam 2015 Brisbane

Software Foundations Workshop

WORKSHOP/JAM

The Software Foundations syllabus first teaches theorem proving in Coq, without any prerequisites other than basic functional programming. It then gives a broad introduction to Programming Language Theory, completely formalised in Coq. Created by Benjamin Pierce and co-contributors at the University of Pennsylvania, it is freely available, and has been used in several university-level courses.

http://www.cis.upenn.edu/~bcpierce/sf/current/index.html

Programming Language Theory is of interest to anyone who values working software systems, because it gives us tools for understanding the precise meanings of our programs, and the properties of the languages we use to build our programs. And theorem proving is a powerful discipline for challenging our beliefs that we know what we’re doing.

Although Software Foundations is self-contained and suited to self-study, it is easy to be intimidated by such a lengthy course on a topic and using tools that might be considered academic. However, the presenters firmly believe that formalising PLT in Coq actually makes it much more accessible for programmers. Fair warning: it’s also addictive.

In this workshop, you’ll find a supportive and collaborative environment in which newcomers to theorem proving and PLT can begin to explore this discipline, and the more experienced can refine their knowledge. The presenters will demonstrate a selection of exercises and techniques throughout the workshop, including some from early parts of the course, to help people get started, and some from latter parts, as a taste of what’s to come.

Please come prepared…

To make the most of the time available at the workshop, you should bring a laptop with some software already installed. Head over to this address, where we will provide some resources to help you get set-up for the workshop:

http://software-foundations.bfpg.org/