top of page

CURRENT COURSES

Quantum Logic

  • Time: Tuesday 09:00–13:00

  • Location: Room 2.04 of Building 2

  • Office Hours:Wednesday 15:30–17:30

  • Essay topics: 

  1. Turing completeness of the untyped lambda-calculus: ​Prove that every computable partial function on natural numbers is computable by the untyped lambda-calculus.

  2. Strong normalisation of the simply-typed lambda-calculus: Prove that the beta-eta reduction on the (one, product, function)-fragment of the simply-typed lambda calculus is strongly normalising.

  3. Subject reduction and confluence of the simply-typed lambda-calculus: Prove that the beta-eta reduction on the (one, product, function)-fragment of the simply-typed lambda calculus satisfies subject reduction and confluence, for which strong normalisation can be assumed.

  4. Soundness and completeness of the semantics of the (one, product, function)-fragment of the simply-typed lambda-calculus in cartesian closed categories: Give detailed proofs of the soundness and the completeness of the semantics.

  5. Monads and comonads: Give the precise definitions of monads and comonads together with their examples, explain how they are related to adjoints, and prove (co)monads are equivalent to (co)Kleisli triples.

  6. Linear lambda-calculus: Give the full details of a linear lambda-calculus and prove its basic properties (n.b., there are several variants of a linear lambda-calculus, so just choose one).

PAST COURSES

Mathematical logic (fall 2022, Australian National University)

Advanced linear algebra (spring 2022, the University of Minnesota)

Elementary linear algebra (fall 2021, the University of Minnesota)

bottom of page