Reductions and Causality

Jean-Jacques Lévy ( Tsinghua, 2011 )

  • Advanced course on λ-calculus (31 October -18 November, agenda)
      Class 1 Independence and causality within computations
      (weak memory models, parallel computations, security, λ-calculus) [Pdf, Pdf4]

      Class 2 Parallel reductions. Residuals. Parallel moves. Cube lemma.
      Residuals of reductions. Equivalence by permutations [Pdf, Pdf4]

      Class 3 The lattice of reductions. Canonical reductions. [Pdf, Pdf4]

      Class 4 Redexes and their history. Redex families. Finite developments.
      Finite developments +. Infinite reductions and infinite families [Pdf, Pdf4]

      Class 5 Decidability of redex families. Labeled λ-calculus [Pdf, Pdf4]

      Class 6 Reductions and Winskel's event structures. Causality.
      Other calculi. [Pdf, Pdf4]

  • Several references
      Lambda-calculus and Programming (in French) [Pdf, Video]

  • Course, Tsinghua University, Beijing, 2011