Program requirementsCC+examen
TeacherGuillaume Munch-Maccagnoni et Gabriele Vanoni
Weekly hours 4 h CM
Years Master Logique Mathématique et Fondements de l'Informatique

Syllabus

The Curry-Howard correspondence highlights deep links between proofs and programs. Linear logic has profoundly renewed this connection between the formal semantics of programming languages on one hand and proof theory on the other, by bringing attention to the dynamics of programs (how the computation is performed) and on the use of resources. An outcome of this attention to resources are quantitative and interactive approaches to calculi, to types and to the semantics. Quantitative and interactive systems are able to provide information such as the costs of computation, and to express non-functional and low-level aspects of computation.

Contents

Part I: A quantitative view in Operational Semantics

  • Positive connectives: λ-calculus with sums, call by value. Sequent calculus & abstract machines.
  • Abstract rewriting theory with higher-order rewriting systems.
  • Unifying CBN and CBV, application to focusing proof-search for LJ.
  • Linear logic & tools: proof nets, Girard translations
  • Constructive classical logic through a linear logic lens
  • Linear CBPV: effect and resource modalities
  • Notions of linearity in programming languages

Part II: A quantitative view in Denotational Semantics

  • Models of the lambda-calculus.
  • Intersection types and Engeler’s model.
  • Non-idempotent intersection types.
  • The Krivine’s Abstract Machine.
  • Hoare Logic.
  • Quantitative extensions of Hoare Logic.

Bibliography