Matthew had his functional programming epiphany surrounded by the Angle Brackets of Doom (C++ template metaprogramming). He learned some Haskell, and began to appreciate the simple things: composition, meaningful types, and the assurance that what you see is what you get. At some point, he heard about dependent types, and taught himself some Coq. He still occasionally enjoys some C++, for old times sake.
YOW! Lambda Jam 2015 Brisbane
Pattern matching dependent types in Coq
Pattern matching with dependent types in Coq can be awkward, while the same program in Agda might be straightforward and elegant. Yet despite the awkwardness, there may still be reasons to choose Coq for your next dependently-typed development, for example if you want a tactic language to develop domain-specific proof-search procedures.
The purpose of this talk is to demonstrate a small collection of tricks you can use to overcome the awkwardness of pattern matching with dependent types in Coq.
We’ll first review what it means to pattern match on inductive families, contrasting Coq with Agda, and examining what it is about Coq that complicates pattern matching. Using a simple running example, we’ll show how to use Coq “match” annotations to eliminate nonsense cases, and the convoy pattern for refining the types of things already in scope. Finally, we’ll show that by equipping an inductive family with some well-chosen combinators, it is often possible to regain some semblance of elegance.
The techniques described in this talk have been distilled from: Adam Chlipala, Certified Programming with Dependent Types, MIT Press, 2013. http://adam.chlipala.net/cpdt/
Software Foundations Workshop
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.
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: