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

[Ohad Kammar <ohad.kammar@ed.ac.uk>]

Hi,

We'll have two hybrid LFCS seminars this week on Thu and Fri.

These are the first two talks in a series of 4 tutorials by John Longley.

Lecture 1)  Thursday, 26 Jun, 4.10pm

  John Longley, University of Edinburgh

  

  Venue: IF G.03

  

  To attend remotely:

  URL: https://ed-ac-uk.zoom.us/j/88693880907 

  Password: auT7vjGi

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/

  Thu, 26 Jun, 4.10pm

  Venue: IF G.03

  Remote participation:

  URL: https://ed-ac-uk.zoom.us/j/88693880907 

  Password: auT7vjGi

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 material:

Motivations and historical background. Logical relations as a key

proof technique:

normalization and continuity results. Some surprising programs

possible in T.

The Berger-Schwichtenberg normalization by evaluation theorem.

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

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:

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

27 Jun: John Longley, Lecture 2, University of Edinburgh: The Dialectica interpretation

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.