Software Foundations Workshop
A SkillsCast for this session is not available.
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.
https://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:
https://software-foundations.bfpg.org/
YOU MAY ALSO LIKE:
Software Foundations Workshop
Fraser Tweedale
Software EngineerRed Hat