One of the reasons we hold conferences rather than simply mailing out copies of our papers to one another is to enable us to talk to each one another. This creates a setting in which we can communicate semiformal ideas – the rules of thumbs, experience reports, and folklore that contain the craft wisdom of the discipline. These proverbs are also often woolly, debatable and possibly even false, and so are best communicated in the pub after the day’s session.
Alas, we are unable to retire to the pub during this ICFP. Instead, I will take the risk of taking some of these conversations out of their natural habitat and transplant them to videoconferencing.
The format will be somewhat experimental. If there are only a handful of people at the session, then we will just have a conversation. If there are more people, then we will select a topic, and an ad-hoc panel will be assembled from the audience to discuss the topic (and inevitably, something else). Depending on how long things go, this might repeat two or three times during the session.
Some potential topics are:
-
The logic of bunched implications embodies the Buddhist notion of dukkha, the fundamental unsatisfactoriness of life?
-
Type theory has multiple incompatible notions of equality?
-
Dependent types embodies the power of positive thinking and SMT solvers embodies the via negativa?
-
Functional languages with call/cc offer a vision of a universe where dialtheia – true contradiction – is possible?
-
Variables¸ de Bruijn indices, and whether PL research will ever discover an equivalance relation other than α-equivalence?
-
Should Haskell have had modules instead of typeclasses, and ML typeclasses instead of modules?
Wed 26 AugDisplayed time zone: Eastern Time (US & Canada) change
04:30 - 05:30 | |||
04:30 60mTalk | Some Proverbs in Type Theory Social Events Neel Krishnaswami Computer Laboratory, University of Cambridge |