There was a symposium in memory of Paul Hudak at Yale on April 29 and 30, 2016.
Please contribute pictures if you have any more — John
I will be putting up slides from the presentations soon.
Friday, April 29 – Putting the Fun in Functional Programming
This will take place at the Sheffield-Sterling-Strathcona Auditorium(SSS Rm 114) on Yale Campus at 1 Prospect Street. The technical presentations will start at 9am and last until 5:30pm. A reception with Paul’s family follows, starting around 6.
Friday will feature technical talks by Paul’s students and collaborators. Speakers include Bob Keller (Paul’s thesis advisor), Phil Wadler, John Hughes, Daniel Winograd-Cort, John Peterson, Henrik Nilsson, and Sheng Liang.
Saturday, April 30 – Paul’s Life and Work
Saturday starts with remembrance of Paul by John Hughes, John Peterson, and members of the Yale community. Following that, we invite everyone to present their personal memories of Paul. The day concludes with an open house at the CS department in which research groups at Yale will be demonstrating their work. There will be posters describing current research and many of the labs will be open. Food will be served in the 2nd floor atrium of Watson Hall and Paul’s family will be attending. The symposium will wrap up around 2pm.
Paul’s students and collaborators have been invited to make technical presentations at this symposium. These presentations will be accessible to anyone with a background in computing and are meant to illustrate Paul’s impact and legacy. The subject material of these presentations will reflect Paul’s commitment to a principled approach to computing, whether in functional programming or any other field he touched. Paul’s commitment to integrating computing and the arts will also be on display. Speakers will also reflect on their personal connections to Paul and his work. If you would like to contribute a talk please contact John Peterson.
9:00 am: Welcome
9:05 am: Dr. Bob Keller, Harvey Mudd College
Dr. Keller was Paul’s thesis advisor at the University of Utah
Tableaux Are Natural Deductions
Natural deduction and analytic tableaux are two formal methods for developing and presenting proofs in first-order logic. Natural deduction proofs provide a formal counterpart to informal discourse. Tableau proofs are often more straightforward to construct, but may not resemble the most natural informal proofs. Tableaux are algorithmic for propositional logic, and are fairly mechanical for predicate calculus as well, although they cannot be completely algorithmic due to the undecidability of predicate calculus in general. While some have offered the sequent calculus as a link between natural deduction and tableaux, the thesis of this paper is that a tableau proof really is a natural deduction proof if we allow ourselves a small set of lemmas to justify the counterparts of tableau rules as derived natural deduction rules. Thus the interim use of sequent calculus becomes unnecessary. The resulting merger of tableaux under the rubric of natural deduction is gratifying in that it suggests a natural way to exploit arbitrary lemmas as steps in tableaux. The appendix will illustrate the thesis by providing a Haskell program that produces both closed tableaux and corresponding natural deduction derivations from tautologies.
9:50 am: Sheng Liang, Rancher Labs
Dr. Liang was one of Paul’s PhD Students
What makes a great programmer?
With software forming the foundation of many businesses, the demand for programmers continues to outpace supply. How can our industry keep up the demand? Are great programmers taught or self-taught? Does experience still matter? If you want to start a venture, how can you attract good programmers given Google and Facebook of the world seem to be sweeping clean all the best talent? In this talk we will discuss how the supply and demand of programming talent is changing and the factors that contribute to the making of a great programmer.
10:35 am: Phil Wadler, University of Edinburgh
Dr. Wadler served on the Haskell committee with Paul.
Behaviours are dual to events
Conal Elliott and Paul Hudak introduced Functional Reactive Programming and applied it to animation and robotics. It remains subject of active interest, most recently in underpinning the programming language Elm. Functional Reactive Programming is not just a clever hack: via the principle of Propositions as Types it has connections with modal logic, where behaviours correspond to validity and events correspond to possibility. This talk will survey work on the Propositions as Types interpretation of Functional Reactive Programming, and suggest directions for future work.
11:20 am: Henrik Nilsson, University of Nottingham
Dr. Nilsson worked with Paul as a research scientist.
Declarative Reactive Abstractions for Games
Video games are usually not programmed very declaratively. There are a number of reasons for this, from critical efficiency requirements, via the nature of languages and frameworks commonly used for games programming, to the conceptual nature of such games themselves, with state and effects being omnipresent. Nevertheless, as in other application domains, a declarative approach can offer important benefits in terms of clarity, correctness, and reusability, for example. This talk will demonstrate how Functional Reactive Programming (FRP) along and other similar abstractions can be used to implement simple video games declaratively and discuss some of the benefits. While this is just a proof of concept, it is already possible to achieve game play and visual standards typical of the 2D genre; for example, as seen in many currently popular games for smartphones and tablets, and we will demonstrate by showing a real game running on such a mobile device.
12:05 pm: Lunch.
Participants are on their own for lunch. Some of us plan to visit the Shake Shack since this was one of Paul’s favorite places.
2:00pm: Dr. John Peterson and Dr. Greg Haynes, Western State Colorado University
Dr. Peterson worked many years in the Yale Haskell group and continued to collaborate with him up until his death. Dr. Haynes met Paul on his visit to Colorado and has helped bring Paul’s vision of computing and music to life.
Music and Computing: Partners in Education
General education is an essential part of the liberal arts experience. It provides students with a broad educational background that compliments their focus of a particular major. The general education curriculum is an ideal place to explore interdisciplinary studies that delve into the connections between traditional fields of study.
Paul believed that there was a strong connection between computer science and music. His domain-specific music language, Euterpea, allows students without formal training in computing to develop music in an algorithmic manner. Euterpea a new sort of musical instrument, one capable of expressing complex musical structures in a natural manner.
We have developed a new general education course at Western, Algorithmic Music, in which students explore music through composition. Students are exposed to a wide range of musical styles, including rhythmic composition, the use of motivic development, minimalism, and chance music. This course combines elements of music theory, functional programming, and creativity in a manner that speaks to the essence of general education, giving students an appreciation of the essential principles of music and computing. This talk will illustrate this innovative approach to music and computing by demonstrating the educational goals, software, and student compositions created during the course.
2:45 pm: Paul Liu, Intel Labs
Dr. Liu was one of Paul’s PhD Students
Fifty Shades of Laziness
Lazy evaluation is commonly understood as non-strict evaluation with sharing. Over the years people have developed many reduction strategies, and between the notion of call-by-name (no sharing at all) and optimal (all reductions of the same virtual redex are shared), there exists concepts with a varying degree of sharing: laziness (or call-by-need), full laziness, and complete laziness, just to name a few. Among them the least understood is perhaps complete laziness, a name first coined by Holst and Gomard, who didn’t formalize it or gave an implementation (and their idea of doing so turned out to be wrong). Thyer later related complete laziness to lazy specialization in an effort to combine lazy evaluation with partial evaluation. More recently, Sinot attempted to give a natural semantics to complete laziness with the idea of not only sharing the evaluation of a function’s argument but also its evaluation context. However we find that Sinot’s formulation to be flawed, and it is in conflict with Thyer’s definition too. In this work, we look at the history of complete laziness, and study its properties in relation to other formalisms. It remains an open question whether we can define a calculus for complete laziness.
3:20 pm: Break
3:30 pm: John Hughes, Chalmers University
Dr. Hughes served on the Haskell committee with Paul.
Quickcheck: Testing the Hard Stuff and Staying Sane
QuickCheck is a testing tool originally developed in and for Haskell, which generates random tests from a formal specification in the form of properties, and minimizes any counterexamples found to small, easily understandable test cases. For the last ten years, QuickCheck has been deployed in industry and has helped track down innumerable bugs in telecom systems, databases, embedded vehicle software, and many others. In this talk I will introduce QuickCheck and describe some of these applications, including debugging notorious race conditions that plagued the DBMS delivered along with Erlang for years.
A video of this talk as presented in 2014: http://www.infoq.com/presentations/automated-testing
4:10 pm: Walid Taha, Halmstad University
Dr. Taha worked with Paul in the Yale Haskell Group
From FRP to P-FRP and Acumen
While at Yale I worked closely with Paul Hudak and Zhanyong Wan to develop resource bounded variants of Functional Reactive Program (FRP). Later, my group at Rice created Prioritized FRP (P-FRP) as a Domain-Specific Language (DSL) for device drivers. This work became the basis for two generations of Acumen, a DSL for modeling Cyber-Physical Systems (CPSs). This talk describes the impact of Paul’s work on and beyond these languages, including the development of a method for correctly simulating Zeno systems 15 years after learning about them from Paul’s work.
4:45: Alastair Reid, ARM
Alastair worked on the Yale Haskell project
How to have your specification and munge it too
Three main themes from my time working with Paul were bringing time and reactivity into Functional Programming with FRP, Embedded Domain Specific Languages, and finding Laws to let you reason about the meaning and correctness of programs. While Paul worked top down on the big picture, my role was often to work bottom up from a working system and we would hope to meet in the middle.
This talk has a similar two part structure. The first part describes a 5 year effort to formalise ARM’s processor specifications, to automatically munge that specification into a form that model checkers can use and to formally verify ARM processors against this specification. This technique is very effective at finding complex bugs early and is now being used by most ARM processor design teams.
The second part describes “Cava”: a Coq Embedded Domain Specific Language for describing hardware based on Lava. Cava’s goal is to learn how to complement the model-checking work of the first part with theorem proving: allowing us to use a little theorem proving to prove the difficult high level properties and a lot of model checking for the low-level details. … and I hope that the two can meet in the middle.
5:15 pm: Zhong Shao, Yale University
Dr. Shao often worked with Paul.
From Modular Semantics to Compositional Certified System Software
The CertiKOS project at Yale aims to develop new language-based technologies for building large-scale certified system software. Initially, we thought that verifying an OS kernel would require new program logics and powerful proof automation tools, but it should not be much different from standard Hoare-style program verification. After several years of trials and errors, we have decided to take a different path from the one we originally planned. We now believe that building large-scale certified system software requires a fundamental shift in the way we design the underlying programming languages, program logics, and proof assistants. In this talk, I outline our new clean-slate approach, explain its rationale, and describe various lessons and insights based on our experience with the development of several new certified OS kernels.
6:00 pm: Reception
The technical program will be followed by a reception that will include Paul’s family. Food will be provided. The reception will be in the same place as the talks – SSS.
Paul Hudak Memorial Prizes in Computer Science
The Yale Computer Science Department is establishing student prizes to honor Paul and his contributions to Computer Science at Yale. The Paul Hudak Memorial Prizes in Computer Science will be awarded annually to one undergraduate and one graduate student for project or thesis work demonstrating exceptional creativity.
We hope you will contribute to the establishment of the prizes. Instructions and a link to contribute are here.
Many of Paul’s former students and colleagues will be attending. They include Charles Consel, Adrienne Bloss, Daniel Winograd-Cort, Mark Tullsen, Amir Kishon, Bob Keller, John Hughes, Alastair Reid, Phil Wadler, Sheng Liang, Kung Chen, Khoo Siau Cheng, Paul Liu, Ben Goldberg, Walid Taha, Greg Morrisett, Tim Sheard, Kai Li, Antony Courtney, Zhan-Yong Wan, and Martin Sulzmann.