Philip Wadler's home page 
 
Projects 
Currently: 
Formerly: 
ACM Special Interest Group on Programming Languages ,
    Chair (2009–2012), Past Chair (2012–2015).
Avaya Labs ,
  Basking Ridge, Researcher (2000–2003).
 Bell Labs 
 1127 ,
 Lucent Technologies ,
 Murray Hill, Researcher (1996–2000). 
Glasgow University ,
 Professor (1993–1996), Reader (1990–1993), Lecturer (1987–1990).University of Sydney ,
  Guest professor (Jan–Feb 1991).University of Copenhagen ,
  Guest professor (Aug 1989).Oxford University ,
 Postdoc (1983–1987)Chalmers Tekniska Högskola ,
  Göteborg, Visiting Fellow (Sep 1986–Feb 1987).Carnegie-Mellon University ,
 Graduate student (1977–1982)Stanford University ,
 Undergraduate (1973–1977) 
For details see my vita 
or short biography .
Upcoming events 
Chalmers FP , 8 June 2020, invited talk.
  pdf 
  video 
ZuriHac , Zurich, 13 June 2020. Keynote. (Virtual.)
  video 
HOPL IV , London, 14—16 June 2020. Program committee.
       (Postponed to 2021.)
Rigorous Methods for Smart Contracts ,
       Dagstuhl, June 2020. Invited attendee.
       (Postponed.)
Monadic Party , Poznan, 18—19 June 2020. Invited speaker.
       (Postponed.)
Logic Mentoring Workshop , Saarbrücken, 6 July 2020.
       Invited speaker. (Virtual.)
  pdf 
IOHK Cardano Virtual Summit ,
       2—3 July 2020. Invited speaker (three times). (Virtual.)
Logic Mentoring Workshop 
       Saarbrücken, Germany, 6 July 2020. Invited speaker. (Virtual.)
Scala Symposium , Berlin, July 2020. Member of program committee.
Formal Methods for Blockchains (FMBC) , Los Angeles, July 2020.
       Member of program committee.
       (Virtual.)
Haskell Love , 31 July—1 August 2020. Invited speaker.
       (Virtual.)
Verified Software , Newton Institute, Cambridge,
       2—22 August 2020. Invited attendee.
       (Postponed.)
Brazilian Symposium on Programming Languages (SBLP) ,
      9am BRT (1pm BST) 20 October 2020. Keynote speaker.
      (Virtual.)
 
Research interests 
Concurrency.  A recent
result 
shows how to extend the Curry-Howard correspondence to session types.
With
Simon Gay  and
Nobuko Yoshida ,
I am leading the EPSRC programme grant
From Data Types to Session Types: A Basis for Concurrency and Distribution (ABCD) 
(EPSRC ).
 
  
    Agda.  With Wen Kokke I coauthored the textbook,
    Programming Language Foundations in Agda .
    A paper 
    describing the book appeared in SBMF 2018, and won the prize
    for best paper.
  
 
   
Blame.   The
blame calculus ,
developed with Robby Findler ,
Jeremy Siek ,
and Amal Ahmed ,
integrates different type systems via casts.  Casts may mediate between dynamic
and static types, or between simple and dependent types.  The key
result is that when a cast fails, blame must lie on the less precise
side of the cast.
 
Links. 
I led the team that developed
Links 
a programming language for web application development.
My collaborators include
Ezra Cooper ,
Sam Lindley ,
and Jeremy Yallop .
Our work on
formlets 
has been included in 
Intellifactory 
Web Sharper ,
and in libraries for
Common Lisp ,
F# ,
JavaScript ,
Haskell ,
Racket , and
Scala .
 
XML. 
I represented Avaya on the 
W3C XML Query 
working group, which designed
XQuery 
a query language for XML .
My work on XQuery was done in close collaboration with
Jerome Simeon 
and
Mary Fernandez ,
who have an implementation of XQuery called Galax .
I ran a workshop on
XML and Data Binding .
I formerly served on the
W3C XSL  working group,
and I wrote a simple
formal model 
for pattern matching in XSLT.
 
Java. 
With
Gilad Bracha ,
Martin Odersky ,
and
David Stoutamire ,
I designed
GJ ,
an extension of Java
that incorporates generic types.
With
Benjamin Pierce  and
Atsushi Igarashi ,
I designed
Featherweight Java ,
a small formal model of Java, comparable in simplicity to lambda calculus.
With
Maurice Naftalin 
I wrote
Java Generics and Collections ,
published by O'Rielly.
 
Functional languages .
I was a principal designer of
Haskell .
With Simon Marlow, I developed a
type tool 
for
Erlang .
I am a founding member of
IFIP WG 2.8 Functional Programming ,
and served as editor-in-chief of the
Journal of Functional Programming .
 
Logic and programming .
I occasionally write and speak on the 
history of logic and programming languages ,
most recently a paper on
Propositions as Types ,
which appeared in CACM and was presented at Strange Loop
 (video ).
At The Stand in Edinburgh, I performed a routine on Computability
 (video ).
 
 
 
  
 
Awards 
Best paper, SBMF  2018, for
    Programming Language Foundations in Agda .
  
 SIGPLAN Distinguished Service Award , 2016.
ACM Fellow , 2007.
Fellow Royal Society of Edinburgh , 2005.
Wolfon-Royal Society Research Merit Award , 2004–2009. 
EUSA Teaching Awards , Overall High Performer, runner up, 2009.
Most Influential POPL Paper Award  2003 (for 1993),
    Imperative functional programming ,
  by Simon Peyton Jones and Philip Wadler.
 
Recent events 
Lambda Days , Krakow, 12&em;13 June 2025.	 
FME Teaching , online, 6 June 2025.
FLOPS , Akita, Japan, 23—25 April 2020. Program committee.
WTSC , Malaysia, 14 February 2020. Program committee.
WGT , New Orleans, 25 January 2020.
    pdf 
PADL , New Orleans, 20—21 January 2020. Panel.
    pdf 
Collège de France , Paris, 12 December 2019. Invited talk.
  pdf 
Loft, Sao Paul, 27 November 2019.
  video 
  pdf 
 SBMF , Sao Paulo, 27—29 November 2019. Program co-chair.
PURPL , PurPL Fest, Purdue University, 23—24 September 2019.
  Keynote speaker.
  pdf 
  key 
GPCE , Athens, 21—22 October 2019. Program committee.
FMBC , Porto, 11 October 2019. Program committee.
Bright Club , Edinburgh, 29 October 2019. A Profound Pun.
       video 
ICFP Tutorial , Berlin, 23 August 2019.
Full Stack Fest , Barcelona, 3—6 September 2019. Speaker.
RADICAL , Amsterdam, 26 August 2019. Program committee.
Scottish Programming Languages and Verification
       Summer School (SPLV) ,
  Strathclyde University, Glasgow, 5—9 August 2019. Core course.
Curry On , London, 15—16 July 2019. Invited speaker.	 
BuzzConf , Buenos Aires, 12—14 June 2019. Keynote speaker.
    pdf 
Lecture series, Padova, 27—31 May 2019. Lecturer.
 UNSW/Data62. 20 May. Speaker.
 Melbourne University. 16 May. Speaker.
  
 Yow! Lambda Jam , Melbourne, 13—15 May. Keynote
IOHK Summit , Miami, 17—18 April 2019. Speaker.
IOHK School, Addis Ababa, 11—22 March 2019. Lecturer.
 POPL  (and HOPL IV PC), Lisbon, 12—20 January 2019.
ABCD , London, 17—18 December 2018. PI.
Plutusfest ,
  Edinburgh, 11 December 2018. Keynote speaker.
  
SBMF , Salvador, 28—30 November 2018.
       Programming Language Foundation in Agda
       (key ,
        pdf )    
       and Panel Speaker
       (key ,
        pdf ).
Hughes 60, Chalmers, Gothenburg, 17 October 201
       (key ,
        pdf ).
 Strange Loop , St Louis, 27—28 September 2018.
       Categories for the Working Hacker 
       (key ,
        pdf ).
ICFP , St Louis, 23—29 September 2018. Member of ERC & attending.
LambdUp , Prague, 13 September 2018. Keynote speaker.
Curry On & ECOOP, 15—21 July 2018. Attending.
 Facebook, 20 June 2018.
 WG2.8, Asilomar, 10—15 June 2018. Attending.
 2nd Workshop on Trusted Smart Contracts (WTSC) ,
  1—2 March 2018, Santa Barbara Beach Resort, Curacao.
  Programme committee.
Sysmics Workshop ,
  Vienna, 26—28 February 2018,
  Propositions as Sessions:
  pdf ,
  pdf 
Lambda Days ,
  Krakow, 22—23 February 2018,
  Categories for the Working Hacker,
  pdf 
IOHK School, Barbados, 5—9 February 2018.
 University of Lisbon, 23 January 2018,
  pdf ,
  pdf .
 IOHK annual meeting, Lisbon, 15—20 January 2018,
  video .
 Principles of Programming Languages (POPL) ,
  Los Angeles, 8—13 January 2018.
  Programme committe &
  coauthor of
  Refinement Reflection: Complete Verification with SMT .
On sabbatical in Rio de Janeiro, 26 December 2017—11 July 2018. 
 Google X, 16 November 2017.
  Quoted Domain-Specific Languages:		
    pdf .
 QCon San Francisco , 13—15 November 2017.
  Presenting Category Theory for the Working Hacker :		
    key ,
    pdf .
Apple Computer, 10 November 2017:
    key ,
    pdf .
 International Conference on Functional Programming (ICFP) ,
  Oxford, 3—9 September 2017.  Coauthor of
  Gradual Session Types  &
  Theorems for Free for Free .
Domain-Specific Language Design and Implementation (DSLDI) ,
  Vacouver, Sun 22 October 2017. Programme committee.
Generative Programming: Concepts and Experience (GPCE) ,
  Vancouver, October 2017. Programme committee.
Recent Advances in Concurrency and Logic (RADICAL) ,
  colocated with QONFEST, Berlin, 4 September 2017. Programme committee.
WG 2.8 meeting , Edinburgh,
  Sunday 11--Friday 16 June 2017. Local host.
QCon São Paulo , 24—26 April 2017.
  Presenting
  Theorems for Free, Blame for All .
Strachey 100 ,
  18—19 November 2016, Oxford. Speaker:
   pdf ,
   keynote .
Data Science CDT, 20 October 2016
  (slides ).
 Papers We Love ,
  John Reynolds, Definitional Interpreters for Higher-Order Languages,
  18 October 2016, Remote Meetup
  (slides pdf ,
   slides key ,
   links to papers ,
   video ).
Lambda World ,
  1 October 2016, Cadiz. Keynote
  (slides ).
Programming Language Mentoring Workshop (PLMW) ,
  colocated with
  ICFP 
  18 September 2016, Nara. Speaker
  (slides ).
International Summer School on Metaprogramming ,
  8—12 August 2016, Cambridge. Lecturer
  (slides ).
Coherence Generalises Duality:
  a logical explanation of multiparty session types ,
  Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler,
  CONCUR ,
  Quebec, August 2016.
BETTY Summer School ,
  27 June—1 July 2016, Limassol, Cyprus; lecturer
  (slides1 ,
   slides2 ,
   paper1 ,
   paper2 ).
  
ACSD ,
  22—24 June 2016, Torun; keynote speaker.  
Joy of Coding ,
  17 June 2016, De Doelen, Rotterdam; keynote speaker
  (slides pdf ,
   video ).
Papers We Love ,
  John Reynolds, Definitional Interpreters for Higher-Order Programming Languages,
  7 June 2016, Skills Matter, London
  (slides pdf ,
   slides key ,
   links to papers ,
   video ).
Stanford EE380 ,
  Palo Alto, 11 May 2016,
  Propositions as Types 
  (slides ).
CHI ,
  7—12 May 2016, San Jose,
  SIG on Usability of Programming Languages 
  (programminglanguageusability.com ).
Facebook ,
  Mountain View, 5 May 2016,
  Everything old is new again 
  (slides ).
IBM Watson, Yorktown, 2 May 2016, 
  Everything old is new again ,
  (slides ).
 Paul Hudak Symposium , Yale, 29 April 2016; speaker
  (slides pdf ,
  slides keynote ).
Everything old is new again ,
  25 April 2016, Chalmers, Gothenburg, Sweden,
  (slides ).
Wadlerfest 
  11—12 April 2016, Edinburgh
  (slides ).
LFCS30 
  13 April 2016, Edinburgh
  (slides ).
Colloquium Polaris ,
  25 February 2016, Lille; presenting
  Propositions as Types  (cancelled).
Lambda Days , 
  18—19 February 2016, Krakow; keynote speaker
  (slides ).
POPL  and
  PEPM ,
  17—23 January 2016, St Petersberg, Florida;
  presenting
  Everything Old is New Again  at PEPM.
Propositions as Types , CACM, December 2015.
Code Mesh ,
  London, 2—4 November 2015; keynote speaker.
Strange Loop ,
  St Louis, 24—26 September 2015; presenting
  Propositions as types 
  (video ),
  Everything old is new again 
  (video ).
ESSLLI , Barcelona, 3—7 Aug 2015,
  lecturer, presenting Propositions as Types .
Summer School on DSL Design and Implementation ,
  Lausanne, 12—17 July 2015, lecturer, presenting
  QDSL ,
  
  video .
Curry On , Prague, 6—10 July 2015, invited speaker,
  Curry On slides ,
  video ,
  DSLDI slides .
PLDI , Portland, 15—17 June 2015,
  presenting Blame and coercion: Together again for the first time .
Pervasive Parallelism CDT event , Edinburgh, 2—3 June 2015,
  keynote speaker.
IFIP WG 2.8 
  (local arrangements ), Kefalonia, 24—29 May 2015, member.
SNAPL , Asilomar, 3—6 May 2015,
  member of program committee and
  presenting A complement to blame .
Computability , The Stand, Edinburgh, 28 April 2015.
POPL , Mumbai, 11—18 January 2015, external review committee.
PlanBig , Dagstuhl, 14—19 December 2014.
The Third International Conference on Parallel, Distributed and
  Grid Computing (PDGC) , Himachal Pradesh, 11—13 December 2014, keynote
  speaker.
Imperial College Computing Student Workshop , London, 25—26 September 2014,
  keynote speaker, video .
ABCD Meeting , Arran, 9—11 September 2014.
ICFP 2014 , Göteborg, 1—6 September 2014.
Erlang , workshop colocated with ICFP, Göteborg, 5 September 2014, program committee.
BEAT , workshop colocated with CONCUR, Rome, 1 September 2014, program committee.
Advances in Programming Languages ,
  Heriot Watt, 19—22 August 2014, lecturer.
Summer School on Trends in Computing (SSTiC) ,
  Tarragona, 7–11 July 2014, keynote speaker.
  You and Your Research and The Elements of Style
    slides 
    blog 
   Church's Coincidences/Propositions as Types
    slides 
    paper 
   A Practical Theory of Language-Integrated Query
    slides 
    paper 
   Propositions as Sessions
    slides 
    paper 
    
BETTY Summer School ,
  Lovran, Croatia, 30 June–4 July 2014, instructor.
Software Contracts for Communication, Monitoring, and Security ,
  NII Shonan Meeting, Shonan Village, 26–30 May 2014, co-organizer
  (slides of blame tutorial ).
CoCo , Loch Lomond, 8 May 2014
 (slides on ABCD ).
ESOP , Grenoble, 7–11 April 2014, program committee.
Functional Programming eXchange , London, 14 March 2014,
  invited speaker.
Off the Beaten Track (OBT) , co-located with POPL,
  San Diego, 2014, program committee.
Programming Language Mentoring Workshop (PLMW) ,
  co-located with POPL, San Diego, 2014, invited speaker,
  plmw-sandiego.pdf .
YOW! 2013 
  Australia Developers Conference, Melbourne 5—6 Dec,
  Brisbane 9—10 Dec, Sydney 12—13 Dec 2013,
  keynote speaker.monads-haskell.pdf ,
  monads-scala.pdf ,
  dsl-long.pdf ,
  dsl-short.pdf .
SAPLING ,
  Sydney, 16 Dec 2013, keynote speaker.
ScalaSyd ,
  Sydney, 11 December 2013,
  atlassian.pdf .
Functional Programming with the Stars ,
  Brisbane, 7 Dec 2013, invited speaker.
Programming Languages Workshop , University of Melbourne,
  4 Dec 201, invited speaker.
Workshop on Secure Cloud and Reactive Internet Programming
  Technology (SCRIPT)  Vrije University, Brussels, 12—13
  Nov 2013, invited speaker.
FP Days ,
  Cambridge, 24 Oct 2013, keynote speaker.
Colin Runciman Celebration ,
  York, 23 Oct 2013, keynote speaker.
ICFP 2013 ,
  presenting A practical
  theory of language-integrated query .
DBPL 2013 ,
  Trento, 30 Aug 2013, program committee.
International Summer School on Trends in Computing  (SSTC 2013),
  Tarragona, 22–26 July 2013,
  invited lecturer .
Fourth Annual Scala Workshop ,
  Montpellier, 2 July 2013,
  keynote speaker .
Midlands Graduate School in the Foundations of Computing Science ,
  8–12 April 2013, invited lecturer
  (Topics in Lambda Calculus and Life ).
Data Driven Functional Programming (DDFP) ,
  workshop at POPL ,
  22 January 2013, keynote speaker
  (The essence of language-integrated query ).
Programming Languages Mentoring Workshop (PLMW) ,
  workshop at POPL ,
  22 January 2013, invited lecturer
  (You and Your Research and The Elements of Style ).
Tech Mesh , London, 4–6 December 2012,
  keynote speaker  plus
  Faith, Evolution, and Programming Languages .
The essence of language-integrated query ,
  draft paper, 1 December 2012.
Propositions as Sessions ,
  ICFP ,
  Copenhagen, 10–12 September 2012.
SICSA Conference , 20–22 June 2012, keynote speaker,
  slides .
Summer School on Types and Programming Languages ,
  St. Andrews, invited speaker,
  Well-typed programs can't be blamed ,
  slides .
PLDI , Beijing, 11–13 June 2012,
  to chair SIGPLAN EC.  Took a Wild Wall Hiking Tour with
  Stretch-a-leg .
Turing Centenial Celebration at Princeton ,
  10–12 May 2012, invited speaker,
  slides 
The future of functional programming languages ,
  Robin Milner Symposium, 16 April 2012, panel chair.
Faith, Evolution, and Programming Languages 
  QCon, London, 9 March 2012
  (video ).
POPL ,
  Philadelphia, 25–27 January 2012, to chair SIGPLAN EC.
Foundations of Scripting Languages , Dagstuhl, 2–6 January 2012.
Course lecturer, Integrating Static and Dynamic Types Systems ,
  28–29 October, 2–3 December 2011, University of Warsaw,
  slides .
  
Older events .
Recent talks and papers 
  
      Validity, Liquidity, and Fidelity:
      Formal Verification for Smart Contracts in Cardano ,
      Tudor Ferariu, Philip Wadler, Orestis Melkonian.
      6th International Workshop on
        Formal Methods for Blockchains (FMBC 2025) ,
      Editors: Diego Marmsoler and Meng Xu; Article No.6; pp.6:1&em;6:21.
      Open Access Series in Informatics (OASIcs).
      Hamilton, Canada, 4 May 2025.
  
  
      A simple blame calculus for explicit nulls ,
      Ondrej Lhotak and Philip Wadler. 
      Journal of Functional Programming  34 , e15, 26 pages, 2025.
  
      Explicit Weakening 
      Philip Wadler.
      A Second Soul: Celebrating the Many Languages of Programming -
      Festschrift in Honor of Peter Thiemann's Sixtieth Birthday - Freiburg,
      Germany. EPTCS 413. August 2024.
  
      Blame and Coercion, Together Again for the First Time 
      Jeremy G. Siek, Peter Thiemann, Philip Wadler.
      Journal of Functional Programming , 31 e20, 2021.
  
      Featherweight Go 
      Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance
      Taylor, Bernardo Toninho, Philip Wadler, Nobuko Yoshida.
      PACMPL  (volume 4, issue OOPSLA, article 149), November 2020.
  
	 Theoretical Pearl: ≐≃≡ Leibniz equality is
         isomorphic to Martin-Löf identity, parametrically .
    Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany, and
    Philip Wadler.
    Journal of Functional Programming , 30 e17, 2020.
    
Towards Races in Linear Logic ,
  Wen Kokke, J. Garrett Morris, and Philip Wadler,
  Coordination , June 2019.
Principles of Programming Languages (POPL) , Los Angeles, 8—13 January 2018.
  Programme committe &
  coauthor of
  Refinement Reflection: Complete Verification with SMT .
International Conference on Functional Programming (ICFP) ,
  Oxford, 3—9 September 2017.  Coauthor of
  Gradual Session Types  &
  Theorems for Free for Free .
Coherence Generalises Duality:
  a logical explanation of multiparty session types ,
  Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, Philip Wadler,
  CONCUR ,
  Quebec, August 2016.
The key to blame: Gradual typing meets cryptography ,
  Jeremy Siek and Philip Wadler.
  Draft paper, March 2016, updated July 2016.
Everything Old is New Again ,
  Shayan Najd, Sam Lindley, Josef Svenningsson, Philip Wadler.
  PEPM, January 2016.
Propositions as types ,
  Philip Wadler, CACM, December 2015.
Blame and coercion: Together again for the first time ,
  Jeremy Siek, Peter Thiemann, Philip Wadler.
  PLDI, June 2015.
A complement to blame ,
  Philip Wadler,
  SNAPL, May 2015.
The Implicit Calculus: A New Foundation for Generic Programming ,
  Bruno C. D. S. Oliveira, Tom Schrijvers, Wontae Choi, Wonchan Lee,
  Kwangkeun Yi, Philip Wadler.  Draft paper, 2014.
Propositions as sessions ,
  Philip Wadler, Journal of Functional Programming, Best papers of ICFP 2012.
Blame, coercions, and threesomes, precisely ,
  Jeremy Siek, Peter Thiemann, and Philip Wadler, draft, March 2014.
  (Superseded by Blame and coercion: Together again for the first time ).
A practical theory of language-integrated query ,
  ICFP ,
  Boston, 25–27 September 2013.
You and Your Research and The Elements of Style ,
  PLMW ,
  Rome, POPL ,
  22 January 2013.
Propositions as Sessions ,
  ICFP ,
  Copenhagen, 10–12 September 2012.
Church's Coincidences ,
  Turing Centenial Celebration at Princeton ,
  10–12 May 2012, invited speaker.
Blame for All ,
  POPL 2011 .
The arrow calculus ,
  JFP .
Threesomes, with and without blame ,
  POPL 2010 .
Monadic constaint programming ,
  JFP .
The RPC Calculus ,
  PPDP 2009 .
Blame for all ,
  STOP 2009 .
Threesomes, with and without blame ,
  STOP 2009 .
Well-typed programs can't be blamed .
  ESOP 2009 ,
The essence of form abstraction ,
  APLAS 2008.
Idioms are oblivious, arrows are meticulous,
   monads are promiscuous ,
  MSFP 2008.
The arrow calculus (Functional pearl) ,
  Submitted to ICFP 2008.
Well-typed programs can't be blamed ,
  Submitted to ICFP 2008.
An idiom's guide to formlets ,
  Submitted to ICFP 2008.
Signed and sealed ,
  Submitted to ICFP 2008.
A located lambda calculus ,
  Submitted to ICFP 2008.
Aspect-Oriented Software Development (AOSD 2008) ,
    2–4 April 2008, Brussels (keynote).
    Presented Well-typed programs can't be blamed .
Well-typed programs can't be blamed ,
  Scheme workshop, ICFP, Freiburg, 30 September 2007.
Comprehensive comprehensions ,
  Haskell workshop, ICFP, Freiburg, 30 September 2007.
Links: Web Programming
  Without Tiers , invited talk, FMCO, Amsterdam, 9 November 2006,
  NICTA, Melbourne, 2 February 2006, and
  PADL, Charleston, 9 January 2006.
Faith, Evolution, and Programming
  Languages , invited talk, OOPSLA, Portland, 26 October 2006.
You and Your Research ,
	  my attempt to channel R. W. Hamming in a talk
	  for postgraduate students at Firbush retreat.
	  Here is a transcript of
	  Hamming's original talk .
Call-by-value is dual to call-by-name, Reloaded 
  Invited talk,
  Rewriting Techniques and Applications  (RTA),
  Nara, April 2005.
The unreasonable effectiveness of logic ,
inaugural lecture, University of Edinburgh, 16 November 2004.
 
Down with the bureaucracy of syntax!
  Pattern matching for classical linear logic ,
  manuscript, April 2004.
The Girard-Reynolds Isomorphism (second edition) ,
  manuscript, March 2004.
  XQuery from the Experts ,
    published by Addison-Wesley, 29 August 2003 (contributor).
 
  Call-by-value is dual to call-by-name ,
  ICFP , Uppsala, Sweden, 25-29 August 2003.
  NJPLS , AT&T Labs, Florham Park, 21 February 2003.
 
  A Prettier Printer ,
  In
  The Fun of Programming ,
  A symposium in honour of Professor Richard Bird's 60th birthday,
  Examination Schools, Oxford, 24-25 March 2003.
 
  As Natural as 0, 1, 2 ,
  Edinburgh University
  Informatics Jamboree 
  20 May 2004,
  Bard College
  Distinguished Scientist Lecture ,
  10 April 2003, and
  Evans and Sutherland Distinguished Lecture ,
  20 November 2002.
 
  The Essence of XML ,
  POPL 2003 , New Orleans, January 2003.
  FLOPS 2002 , Aizu, Japan, September 2002 (invited talk).
 
  The Great Type Hope .
  Erlang Workshop, Pittsburgh, October 2002 (invited talk).
 
XQuery, a typed functional language for querying XML ,
  Advanced Functional Programming, Oxford, August 2002.
XQuery tutorial ,
 XML 2001, Orlando, December 2001 (tutorial).
Et tu, XML?  The fall of the relational empire ,
  VLDB 2001, Rome, September 2001 (keynote).
MSL: A model for W3C XML Schema ,
  WWW01, Hong Kong, May 2001.
From Frege to Gosling ,
  Alan J. Perlis Symposium,
  Programming Languages: Theory Meets the Real World ,
  Yale University, 27 April 2000 (invited talk).
19'th Century Logic and 21'st Century Programming Languages ,
  Dr Dobbs, December 2000.
 
Publications and Talks 
Citations of my work on
Google Scholar ,
Microsoft Academic Search ,
Citeseer .
Google ranks my h-index at 60 (September 2013).
I appear at position 6 in a list of 
most acknowledged researchers .
Bibliography at
DBLP  and
Edinburgh Research Explorer .
Here is my 
Orcid id .
Students 
Current students (PhD):
Jakub Zalewski (PhD), starting fall 2015,
   enrolled in
   Centre for Doctoral Training in Pervasive Parallelism .
 Simon Fowler  (PhD), started fall 2014,
   enrolled in
   Centre for Doctoral Training in Pervasive Parallelism .
Jack Williams  (PhD), started fall 2014,
   recipient of a
   Microsoft Research PhD Scholarship .
Shayan Najd  (PhD), started fall 2013,
   recipient of a 
   Google European Doctoral Fellowship .
Ben Kavanagh  (PhD), started 2004, currently working with James Cheney,
  blog ,
  wiki .
 
Previous students (PhD and MPhil):
Previous students (MSc and UG4):
Of interest to potential students:
Teaching 
Current.
Former.
Service and Editorial 
Please submit to the above!
Unusual applications 
Here are some unusual application of my work.  Please let me know of others!
Computational linguistics. 
Quantum computation. 
A Lambda Calculus for Quantum Computation 
and
Quantum Computation, Categorical Semantics and Linear Logic ,
by
Andre van Tonder 
cites my work on linear logic.
 
Structuring quantum effects: superoperators as arrows ,
by Juliana Vizzotto, Thorsten Altenkirch, and Amr Sabry,
relates quantum computing to monads and arrows.
 
A linear-non-linear model for a computational call-by-value lambda calculus ,
by Peter Selinger and Benoit Valiron,
relates quantum computing to both linear logic and monads.
 
The Arrow Calculus as a Quantum Programming Language ,
by Juliana Kaizer Vizzotto, Andre Rauber Du Bois, and Amr Sabry,
is based on my work with Sam Lindley and Jeremy Yallop on
The Arrow Calculus .
  
eScience. 
Nanotechnology 
Proof Assistants 
The proof monad ,
by Florent Kirchner and Cesar Munoz,
applies monads to support computational features of proof languages,
such as side effects, exception handling, and backtracking.
  
Phenomenology 
 
Jewish calendar 
A request: please avoid scheduling events on 
Shabbat, Rosh Hasanah, Yom Kippur, Sukkot, Chanukkah, Purim, and Passover.
Holiday dates for the next five years .
I am a member of Sukkat Shalom, the Edinburgh Liberal Jewish Community ,
Jews for Justice for Palestinians ,
and Scottish Jews for a Just Peace .
Other 
Personal 
I am the father of Adam and Leora.
 
  We are entering an era where someone might use a large language model
  to generate a document out of a bulleted list, and send it to a person
  who will use a large language model to condense that document into a
  bulleted list. Can anyone seriously argue that this is an improvement?
  — Ted Chiang,
  Why A.I. Isn't Going to Make Art ,
  The New Yorker, 31 August 2024.
 
Other favorite quotes 
 
 
 
 
Philip Wadler ,