In celebration of Philip Wadler's 60th birthday

Dates: Monday 11th–Tuesday 12th April 2016

Location: Room G.07, Informatics Forum, Edinburgh

Phil holds the chair in theoretical computer science (Robin Milner's old chair) at the Laboratory for Foundations of Computer Science (LFCS). A separate event, LFCS30, to celebrate the 30th anniversary of the founding of the LFCS will take place on Wednesday 13th April.

Accepted papers

Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, and Perdita Stevens
Reflections on monadic lenses

Robert Atkey, Sam Lindley, and J. Garrett Morris
Conflation confers concurrency

Nick Benton, Andrew Kennedy, Martin Hofmann, and Vivek Nigam
Counting successes: effects and transformations for non-deterministic programs

Andrew Black, Kim Bruce, and James Noble
The essence of inheritance

John T. O'Donnell and Cordelia Hall
Pointlessness is better than listlessness

Hugh Leather and Janne Irgens
The lambda calculus: practice and principle

Simon Gay
Subtyping supports safe session substitution

Neil Ghani, Fredrik Nordvall Forsberg, and Federico Orsanigo
Proof relevant parametricity

Jeremy Gibbons
Comprehending ringads

Ralf Hinze and Dan Marsden
Dragging proofs out of pictures

John Hughes
Experiences with QuickCheck: testing the hard stuff and staying sane

Graham Hutton and Patrick Bahr
Cutting out continuations

Conor McBride
I got plenty o’ nuttin’

Martin Odersky, Nada Amin, Tiark Rompf, Sandro Stucki, and Samuel Gruetter
The essence of dependent object types

Jennifer Paykin and Steve Zdancewic
Linear lambda-mu is CP (more or less)

Simon Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, and Dimitrios Vytiniotis
A reflection on types

Tiark Rompf
The essence of multi-stage evaluation in LMS

Andreas Rossberg
1ML with special effects

Manuel Serrano
The computer scientist nightmare

Avraham Shinnar and Jerome Simeon
A branding strategy for business types

Jeremy Siek and Sam Tobin-Hochstadt
The recursive union of some gradual types

Bernardo Toninho and Nobuko Yoshida
Certifying data in multiparty session types

Peter Thiemann
A delta for hybrid type checking

David Turner
Recursion equations as a programming language

Programme of talks

There is not a one-to-one correspondence between accepted papers and talks.
The video recording setup was rather flakey, so only some talks were recorded and the quality is variable.

Monday 11th April

0830–0900: Registration
0900–1000 (John): John Hughes
Experiences with QuickCheck: testing the hard stuff and staying sane (slides)
1000–1030: Coffee break
1030–1130 (mathematically structured functional programming): Jeremy Yallop
Causal commutative arrows revisited (slides); Jeremy Gibbons
Comprehending ringads (slides) (video)
1130–1200: Break
1200–1300 (effects): Andreas Rossberg
1ML with special effects (slides) (video); Nick Benton, Andrew Kennedy, Martin Hofmann, and Vivek Nigam
Counting successes: effects and transformations for non-deterministic programs (slides)
1300–1400: Lunch
1400–1500 (linearity): Conor McBride
I got plenty o’ nuttin’; Jennifer Paykin and Steve Zdancewic
Linear lambda-mu is CP (more or less) (slides)
1500–1530: Coffee break
1530–1630 (session typing): Simon Gay
Subtyping supports safe session substitution (slides) (video); Bernardo Toninho and Nobuko Yoshida
Certifying data in multiparty session types (slides)
1630–1700: Break
1700–1800 (optimisation and success): John O'Donnell and Cordelia Hall
Pointlessness is better than listlessness (video); Philip Wadler
A list of successes that has not yet changed the world (slides) (video)

Tuesday 12th April

0900–1000 (Simon): Simon Peyton Jones
A reflection on types (slides) (video)
1000–1030: Coffee break
1030–1130 (gradual typing): Peter Thiemann
A delta for hybrid type checking (slides); Jeremy Siek and Sam Tobin-Hochstadt
The recursive union of some gradual types (slides)
1130–1200: Break
1200–1300 (objects): Andrew Black, Kim Bruce, and James Noble
The essence of inheritance (video); Martin Odersky, Nada Amin, Tiark Rompf, Sandro Stucki, and Samuel Gruetter
The essence of dependent object types (slides) (video)
1300–1400: Lunch
1400–1500 (sociology): Maurice Naftalin
"Well grubbed, old mole!”: open source and the undermining of capitalism (slides) (video); Manuel Serrano
The computer scientist nightmare
1500–1530: Coffee break
1530–1630 (semantics): Neil Ghani, Fredrik Nordvall Forsberg, and Federico Orsanigo
Proof relevant parametricity (video); Ralf Hinze and Dan Marsden
Dragging proofs out of pictures (slides)
1630–1700: Break
1700–1730 (embedded domain-specific languages): Tiark Rompf
The essence of multi-stage evaluation in LMS (slides) (video)
1730–1745: A list of successes that can change the world (video)
1900–: Banquet

Social programme

Coffee and lunch will be provided on both days.
A banquet will be held on Tuesday evening jointly with LFCS30.

Registration (closed)

Attendees will be charged a registration fee of £25.
Registration includes both WadlerFest and LFCS30.

Festschrift

Phil will be presented with a festschrift entitled A list of successes that can change the world to be published by Springer as a volume in the LNCS series. Update: The Festschrift is now available.

Editors

Sam Lindley (The University of Edinburgh)
Conor McBride (University of Strathclyde)
Phil Trinder (University of Glasgow)
Don Sannella (The University of Edinburgh)

Local organisers

Stephen Gilmore
Sam Lindley
Don Sannella

WadlerFest 2016