[5-8]Sequential algorithms (old and new)
Date:2015-05-06
Title：Sequential algorithms (old and new)
Speaker: Pierre-Louis Curien
Time: 8th May 2015, 10:30 a.m.
Venue: 337, Level 3, Building 5,
Abstract: We shall recall the 37 years old model of sequential algorithms of Berryand Curien of the language PCF (a language that has been very luch studied until now in the field of semantics of progamming languages. We shall give an application by giving a new proof of Loïc Colson's "ultimate obstinacy" theorem (a theorem about the sequential behaviour of primitive recursive functions, which deserves to be more well-known!). Sequential algorithms can also be used with benefit to describe bar recursion (a powerful induction principle in constructive mathematics), but this will be only mentioned at the end of the talk.
Biography: Pierre-Louis Curien is a specialist of the semantics of programming languages (both denotational and operational). After graduating from the Ecole Normale Superieure of Paris, he worked with Gerard Berry on a mathematical account of the notion of sequential program, where programs as functions and programs as algorithms get closer. His most widely-known contributions are outcomes of this early work. They include the Categorical Abstract Machine (for functional programming languages), the theory of Explicit Substitutions, and a core calculus for the Duality of Computation (where the dualities are input versus output, lazy versus eager). During the last decade, he has set up and been the director of the laboratory PPS (Proofs, Programs and Systems, Paris Diderot University and CNRS), which has become a major center worldwide around programming languages and proof theory.