Skip to Content.
Sympa Menu

lfcs-interest - [LFCS seminar] Today, 27 Jun: John Longley, Lecture 2: The Dialectica interpretation

Subject: Events and news relevant to the Laboratory for Foundations of Computer Science

List archive

Chronological Thread  
  • From: Ohad Kammar <ohad.kammar@ed.ac.uk>
  • To: Seminars <inf-seminars@mlist.is.ed.ac.uk>, LFCS Interest <lfcs-interest@mlist.is.ed.ac.uk>
  • Cc: John Longley <J.R.Longley@ed.ac.uk>
  • Subject: [LFCS seminar] Today, 27 Jun: John Longley, Lecture 2: The Dialectica interpretation
  • Date: Fri, 27 Jun 2025 07:00:00 +0000

Hi,

Reminding that we'll have an LFCS seminar today:

Lecture 2)  Friday, 27 Jun, 4.10pm

  This seminar is hybrid.
  
  Venue: IF G.03
  
  To attend remotely:
  URL: https://ed-ac-uk.zoom.us/j/83334756668 
  Password: 517r2GbZ

We're synchronising the seminar time with the teaching timetable, and
plan to start the talk at the advertised time, so please arrive a minute or two
earlier.


In detail:

----------------------------------------------------------------------
John Longley, University of Edinburgh
https://homepages.inf.ed.ac.uk/jrl/

  Fri, 27 Jun, 4.10pm
  Venue: IF G.03
  Remote participation:
  URL: https://ed-ac-uk.zoom.us/j/83334756668 
  Password: 517r2GbZ



Lecture 2: The Dialectica interpretation

Abstract

This talk is the 2nd 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 2 will cover the following material:


Extracting T programs from classical proofs. Examples and
applications in proof theory.

Spector's extension to full second-order arithmetic using bar
induction.

----------------------------------------------------------------------

Upcoming seminars:
------------------
01 Jul: John Longley, Lecture 3, University of Edinburgh: Plotkin's PCF and its
        sublanguages
08 Jul: John Longley, Lecture 4, University of Edinburgh: Computability theory of PCF
05 Aug: Michael Sperber, Active Group GmbH



If you would like to propose a speaker, or speak yourself, please contact me.
The seminar webpages:
http://web.inf.ed.ac.uk/lfcs/events/lfcs-seminars

Yours,
Ohad.


The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.

  • [LFCS seminar] Today, 27 Jun: John Longley, Lecture 2: The Dialectica interpretation, Ohad Kammar, 06/27/2025

Archive powered by MHonArc 2.6.24.

Top of Page