lambdaman

WadlerFest 2016

In celebration of Philip Wadler's 60th birthday

Dates: Monday 11th–Tuesday 12th April 2016

Location: Room G.07, Informatics Forum, Edinburgh

Local information

LFCS30

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

Sponsors

SICSA LFCS