9:00 second breakfast for those who want
9:30 Philip Wadler: The Hen and the Rooster: Agda vs Coq
10:30 coffee
11:00 Simon Peyton Jones: The dream of a lifetime: shaping how our children learn computing
12:00 lunch
14:00 Thomas Arts: Quickchecking blockchains
15:00 coffee
15:30 Koen Lindström Claessen: Random Testing for Fun
16:30 John Launchbury: How I came to love whiskey (via videolink)
19:30 dinner at Chalmersska huset
* Philip Wadler: The Hen and the Rooster: Agda vs Coq
The leading textbook for formal methods is Software Foundations (SF), written by Benjamin Pierce in collaboration with others, and based on Coq. After five years using SF in the classroom, I have come to the conclusion that Coq is not the best vehicle for this purpose, as too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning programming language theory. Accordingly, I have written a new textbook, Programming Language Foundations in Agda (PLFA). PLFA covers much of the same ground as SF, although it is not a slavish imitation.
What did I learn from writing PLFA? First, that it is possible. One might expect that without proof tactics that the proofs become too long, but in fact proofs in PLFA are about the same length as those in SF. Proofs in Coq require an interactive environment to be understood, while proofs in Agda can be read on the page. Second, that constructive proofs of preservation and progress give immediate rise to a prototype evaluator. This fact is obvious in retrospect but it is not exploited in SF (which instead provides a separate normalise tactic) nor can I find it in the literature. Third, that using raw terms with a separate typing relation is far less perspicuous than using inherently-typed terms. SF uses the former presentation, while PLFA presents both; the former uses about 1.6 as many lines of Agda code as the latter, roughly the golden ratio.The textbook is written as a literate Agda script, and can be found here:
http://plfa.inf.ed.ac.uk
* Simon Peyton Jones: The dream of a lifetime: shaping how our children learn computing In September 2014 a radical new computing curriculum was launched in England. For the first time, computing is being taught as a foundational subject discipline that, like natural science, every child learns from primary school onward. That presents us, the tech community, with a huge challenge, and equally huge opportunity. The challenge is that our hard-working teachers are ill-qualified to teach this new subject, and we don’t have much experience of exactly what to teach and how to teach it. What is it important for our children to know? What should they be able to do? The opportunity is that, in the UK at least, the government is openly inviting employers, universities, and professional societies to play a leading role tackling that challenge. That means us! In this talk I’ll give you some perspective on just how far we have come and, using the Royal Society’s recent report “After the Reboot”, I’ll describe where we are now. The UK is not alone in this journey. I know that Sweden is also introducing programming as a compulsory subjects in schools, and John is personally involved in this endeavour. Many other nations are wrestling with the same issues in different ways. The ice has melted and everything is in flux. None of us knows all the answers, but I am convinced that we will get better outcomes if we work together.
* John Launchbury: How I came to Love whiskey
This talk is a personal retrospective on aspects of John’s influential career, focusing particularly on the early days.(Unfortunately, John will not be able to come to Gothenburg, so this talk is via videolink.)