INESC-ID Distinguished Lecture, Lisbon

I'm looking forward to speaking in Lisbon. 

On June 4, Professor Philip Wadler will give an INESC-ID Distinguished Lecture organized in the scope of the BIG ERA Chair Project, titled “(Programming Languages) in Agda = Programming (Languages in Agda)”.

Registration: here (free but mandatory)
Date: June 4, 2024
Time: 15h00-16h15
Where: Anfiteatro Abreu Faro – Complexo Interdisciplinar, Instituto Superior Técnico (Alameda)

Abstract: The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. Proof by induction is just programming by recursion.  Finding a proof becomes as fun as hacking a program. Dependently-typed programming languages, such as Agda, exploit this pun. This talk introduces *Programming Language Foundations in Agda*, a textbook that doubles as an executable Agda script—and also explains the role Agda plays in IOG’s Cardano cryptocurrency.

Labels: ,



I am a Highly Ranked Scholar

I am delighted to have made this list. Lesley Lamport and John Reynolds also appear on it, but at positions lower than mine, and Tony Hoare and Robin Milner don't appear at all---so perhaps their methodology needs work.

Congratulations on being named an inaugural Highly Ranked Scholar by ScholarGPS

Dear Dr. Wadler,

ScholarGPS celebrates Highly Ranked Scholars™ for their exceptional performance in various Fields, Disciplines, and Specialties. Your prolific publication record, the high impact of your work, and the outstanding quality of your scholarly contributions have placed you in the top 0.05% of all scholars worldwide.

Listed below is a summary of the areas (and your ranking in those areas) in which you have been awarded Highly Ranked Scholar status based on your accomplishments over the totality of your career (lifetime) and over the prior five years:

Highly Ranked Scholar - Lifetime
#9,339Overall (All Fields)
#1,299Engineering and Computer Science
#265Computer Science
#2Programming language

Please consider sharing your recognition as an inaugural ScholarGPS Highly Ranked Scholar with your employer, colleagues, and friends.

ScholarGPS also includes quantitative rankings for research institutions, universities, and academic programs across all areas of scholarly endeavor. ScholarGPS provides rankings overall (in all Fields), in 14 broad Fields (such as Medicine, Engineering, or Humanities), in 177 Disciplines (such as Surgery, Computer Science, or History), and in over 350,000 Specialties (such as Cancer, Artificial Intelligence, or Ethics).

We are pleased to currently offer you free access to each of the following:Sincerely,
The ScholarGPS Team




Cabaret of Dangerous Ideas

I'll be appearing at the Fringe in the Cabaret of Dangerous Ideas, 12.20-13.20 Monday 5 August and 12.20-13.20 Saturday 17 August, at Stand 5. (The 5 August show is joint with Matthew Knight of the National Museums of Scotland.)

Here's the brief summary:

Chatbots like ChatGPT and Google's Gemini dominate the news. But the answers they give are, literally, bullshit. Historically, artificial intelligence has two strands. One is machine learning, which powers ChatGPT and art-bots like Midjourney, and which threatens to steal the work of writers and artists and put some of us out of work. The other is the 2,000-year-old discipline of logic. Professor Philip Wadler (The University of Edinburgh) takes you on a tour of the risks and promises of these two strands, and explores how they may work better together.
I'm looking forward to the audience interaction. Everyone should laugh and learn something. Do come!


I'm speaking at Lambda Days 2024.

I'm looking forward to Lambda Days 2024 and catching up with friends in Krakow.




Orwell was right


A short comic by Mike Dawson. Stick to the end for a valid point.

Labels: , , ,



The Problem with Counterfeit People


A sensible proposal in The Atlantic from philosopher Daniel Dennett. Is anyone campaigning for a law or regulation to this effect?

Creating counterfeit digital people risks destroying our civilization. Democracy depends on the informed (not misinformed) consent of the governed. By allowing the most economically and politically powerful people, corporations, and governments to control our attention, these systems will control us. Counterfeit people, by distracting and confusing us and by exploiting our most irresistible fears and anxieties, will lead us into temptation and, from there, into acquiescing to our own subjugation.

There may be a way of at least postponing and possibly even extinguishing this ominous development, borrowing from the success—limited but impressive—in keeping counterfeit money merely in the nuisance category for most of us (or do you carefully examine every $20 bill you receive?).

As [historian Yuval Noah] Harari says, we must “make it mandatory for AI to disclose that it is an AI.” How could we do that? By adopting a high-tech “watermark” system like the EURion Constellation, which now protects most of the world’s currencies. The system, though not foolproof, is exceedingly difficult and costly to overpower—not worth the effort, for almost all agents, even governments. Computer scientists similarly have the capacity to create almost indelible patterns that will scream FAKE! under almost all conditions—so long as the manufacturers of cellphones, computers, digital TVs, and other devices cooperate by installing the software that will interrupt any fake messages with a warning.


Will A.I. become the new McKinsey?

Ted Chiang, ever thoughtful, suggests a new metaphor for A.I. Published in The New Yorker.
So, I would like to propose another metaphor for the risks of artificial intelligence. I suggest that we think about A.I. as a management-consulting firm, along the lines of McKinsey & Company. Firms like McKinsey are hired for a wide variety of reasons, and A.I. systems are used for many reasons, too. But the similarities between McKinsey—a consulting firm that works with ninety per cent of the Fortune 100—and A.I. are also clear. Social-media companies use machine learning to keep users glued to their feeds. In a similar way, Purdue Pharma used McKinsey to figure out how to “turbocharge” sales of OxyContin during the opioid epidemic. Just as A.I. promises to offer managers a cheap replacement for human workers, so McKinsey and similar firms helped normalize the practice of mass layoffs as a way of increasing stock prices and executive compensation, contributing to the destruction of the middle class in America.

A former McKinsey employee has described the company as “capital’s willing executioners”: if you want something done but don’t want to get your hands dirty, McKinsey will do it for you. That escape from accountability is one of the most valuable services that management consultancies provide. Bosses have certain goals, but don’t want to be blamed for doing what’s necessary to achieve those goals; by hiring consultants, management can say that they were just following independent, expert advice. Even in its current rudimentary form, A.I. has become a way for a company to evade responsibility by saying that it’s just doing what “the algorithm” says, even though it was the company that commissioned the algorithm in the first place.

Labels: ,



Our Labor Built AI


An introduction for laymen from The Nib. By Dan Nott and Scott Cambo.

Labels: , ,



Gradual Effect Handlers


As part of the SAGE project funded by Huawei, Li-yao Xia has written in Agda a model of a gradual type system for effects and handlers. It is available on GitHub.

Labels: , ,



Writing and Speaking with Style


I instruct all my students to read Strunk and White's The Elements of Style and Pinker's The Sense of Style. Now I have another resource to recommend.

Benjamin Pierce writes:

In 2021, Rajeev Alur and I created a course at Penn called Writing and
Speaking with Style.  Aimed at PhD students in computer science and other
areas of science and engineering, the course is a semester-long immersion
in effective technical writing and speaking.  Since then, I've run it twice
more, improving and polishing each time.  I think it's pretty good now.  :-)

In hopes that the course materials may be useful to others, all the slide
decks, timeline, readings, and detailed notes for instructors are now
publicly available: you can find it all here.


This page is powered by Blogger. Isn't yours?