The development of quantum information and computation entails the need for formal tools to model, verify and reason rigorously about quantum programs. This course explores
Feb 06 (11:00 - 13:00) | Introduction to the course: objectives, learning outcomes, organisation. Logic and (quantum) computation. |
Feb 13 (11:00 - 13:00) | CARNIVAL |
Feb 20 (11:00 - 13:00) | Intuitionistic logic: formulae, sequents and proofs; natural deduction for intuitionistic logic; admissibility. |
Feb 27 (11:00 - 13:00) | Untyped lambda-calculus:(untyped) terms; alpha-equivalence; substitution; beta-reduction. |
Mar 5 (11:00 - 13:00) | Simply-typed lambda-calculus: types; (typed) terms; Curry-Howard-isomorphisms; beta-reduction; eta-reduction; subject reduction; confluence; strong normalisation. |
Mar 12 (11:00 - 13:00) | Category theory: categories; monos and epis; isomorphisms; initial and terminal objects; products; exponents; functors; natural transformations. |
Mar 19 (11:00 - 13:00) | Category theory (continued), categorical logic and intuitionistic linear logic: Yoneda lemma; adjoints; categorical semantics of simply-typed lambda calculus in Cartesian closed categories; soundness and completeness; intuitionistic linear logic. |
Apr 2 (11:00 - 13:00) | Linear and quantum lambda-calculi and monoidal categories: linear and quantum lambda-calculi; symmetric monoidal closed categories; categorical semantics of linear and quantum lambda-calculi. |
Apr 9 (11:00 - 13:00) | Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture. Closing of the course Module 1. |
Apr 16 (11:00 - 13:00) | Introduction to module 2. Diagrams and categories. Diagramatic languages for processes. Circuits [lecture notes]. String diagrams: definitions, examples, constructions [lecture notes]. |
Apr 24 (16:00 - 18:00) | The process theory of linear maps. Matricial representation. Completeness for string diagrams. [lecture notes] .(Room DI 1.20) |
Apr 30 (11:00 - 11:00) | The process theory of pure quantum maps. Doubling to retrieve probabilities as scalars and get rid of global phases. [lecture notes] . |
May 14 (11:00 - 11:00) | Quantum processes: adding discarding and non determinism. [lecture notes] . |
Feb 06 (09:00 - 11:00) | Premiliminaries on logic and quentum computation. |
Feb 13 (09:00 - 11:00) | CARNIVAL |
Feb 20 (09:00 - 11:00) | Intuitionistic logic: how to write proofs in natural deduction; how to show the admissibility of a rule. |
Feb 27 (09:00 - 11:00) | Untyped lambda-calculus: how to check if an expression is (not) a term; how to execute alpha-conversion and beta-reduction. |
Mar 5 (09:00 - 11:00) | Simply-typed lambda-calculus: how to construct a term; how to execute beta- and eta-reductions. |
Mar 12 (09:00 - 11:00) | Category theory: how to prove that a concrete structure is a category; how to show that initial and terminal objects as well as products are unique. |
Mar 19 (09:00 - 11:00) | Category theory (continued), categorical logic and intuitionistic linear logic: how to interpret some concrete terms; how to prove that a concrete structure is an adjoint; how to prove that exponents are right adjoints to products. |
Apr 2 (09:00 - 11:00) | Linear and quantum lambda-calculi and monoidal categories: how to write examples of linear and quantum terms; how to interpret examples of linear and quantum terms; how to prove an instance of a coherence theorem for monoidal categories. |
Apr 9 (09:00 - 11:00) | Linear and quantum lambda-calculi and monoidal categories: conclusion of the previous lecture. |
Apr 16 (09:00 - 11:00) | Exercises on circuits and string diagrams. |
Apr 23 (09:00 - 11:00) | The ZX calculus [Wetering, 2020] |
Apr 30 (09:00 - 11:00) | Exercises with linear maps |
May 14 (09:00 - 11:00) | Exercises. Project review. |