Program requirementsCC+examen
TeacherClaudia Faggian et Gabriele Vanoni
Weekly hours 4.0 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 approaches to calculi, to types and to the semantics. Quantitative systems are able to provide information such as the cost of computation, and are crucial to express paradigms of computation which are intrinsically quantitative, such as probabilistic, differential or quantum computation.

Contents

Part I.

  • A quantitative view in Operational Semantics
  • Tools to analyze the operational semantics of formal systems: Abstract Rewriting Theory.
  • Bridging between lambda-calculus and functional programming: Call-by-Value and Call-by Name.
  • Linear Logic and Proof-Nets.
  • Quantitative computation: Bayesian Reasoning and Probabilistic 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