Reductions and causality

Jean-Jacques Lévy, INRIA, France

Church’s lambda-calculus is a kernel language for the design of programming languages and the study of their properties. The lambda-calculus is more directly connected to functional languages (Lisp, Scheme, SML, Ocaml, Haskell), but its type theory inspired many other languages (Java, C#, F#, Scala). The lambda calculus has also many implications in mathematical logic. One of the most impressive results is the proof of the consistency of second-order arithmetic by Girard, through Howard correspondance. Another consequence is the formalization of mathematics or the verification of software and hardware in higher-order logics.

This does not need perequisites. It is more addressed to students interested by mathematical logic, formal methods and theory of programming. It is oriented toward the causality and independence of reductions steps in any calculus. It has impact in the proof of optimisation and models of weak memory models for multicore architectures (see Alglave, Maranget, Sewell, Zappa Nardelli, Boudol, Petri recent works). All classes will correspond to exercices. This course might motivate students to the theory of programming languages and to verification with formal methods.

Course contents:

• Causality and Independence in computations. Sequential vs parallel processes in functional languages. Permutations of reads-writes w.r.t (weak) memory models
  
• Lambda-calculus: finite developments theorem. Parallel moves. Cube lemma. Residuals of reductions. Equivalence by permutations.
• The lattice of reductions. Canonical reductions.
• Redexes and their history. Redex families. Generalized finite development theorem. Infinite reductions and infinite families.
  
• Decidability of redex families. Labeled lambda-calculi.
  
• Reductions and Winskel’s event structures. Causality. Other calculi.
  

Course materials:

You can find the course materials by following this link.