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
FLOPS , Akita, Japan, 23—25 April 2020. Program committee.
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
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
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 ,
https://orcid.org/0000-0001-7619-6378