LFCS Seminar Thursday 26th June: John Longley

Lecture 1: Gödel's System T

Abstract

This talk is the 1st in a short series of 4 tutorial lectures covering
some classic material from higher-order computability theory. The
lectures cover classic material rather than very recent research.
They contain fundamental ideas that have proved to be of enduring
interest, but are perhaps not so easy to learn from books and papers.
These lectures reflect some of my recent ideas for presenting this
material as I work on the second edition of my book with Dag Normann on the
subject.


Lecture 1 will cover the following core material:

Motivations and historical background.
Logical relations as a key proof technique:

Additional potential material:

normalization and continuity results.
Some surprising programs possible in T.
The Berger-Schwichtenberg normalization by evaluation theorem.


These lectures follow a special format.  We will have a formal
50 minute seminar covering all or most of the core material that the later lecture
will build in. John kindly agreed to continue with an informal session following the
talk including an extended Q&A and covering additional material that later lectures
do not require.

We are recording both parts of the talk. Subject to unforeseen technical
problems and subject to my available time for editing the videos, I plan to
upload them to our YouTube channel:

https://www.youtube.com/@lfcsseminar9233/playlists<https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.youtube.com%2F%40lfcsseminar9233%2Fplaylists&data=05%7C02%7C%7Ccebb650e1c2f42a8aef308ddb7b14e34%7C2e9f06b016694589878910a06934dc61%7C0%7C0%7C638868694320099223%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=zqx1mHR1RyYn%2B4AoWtV78N58Y%2BjAyWeavl7wKtQ6ARU%3D&reserved=0>