CURRENT COURSES

Time: Tuesday 09:00–13:00

Location: Room 2.04 of Building 2

Office Hours:Wednesday 15:30–17:30

Essay topics:

Turing completeness of the untyped lambdacalculus: â€‹Prove that every computable partial function on natural numbers is computable by the untyped lambdacalculus.

Strong normalisation of the simplytyped lambdacalculus: Prove that the betaeta reduction on the (one, product, function)fragment of the simplytyped lambda calculus is strongly normalising.

Subject reduction and confluence of the simplytyped lambdacalculus: Prove that the betaeta reduction on the (one, product, function)fragment of the simplytyped lambda calculus satisfies subject reduction and confluence, for which strong normalisation can be assumed.

Soundness and completeness of the semantics of the (one, product, function)fragment of the simplytyped lambdacalculus in cartesian closed categories: Give detailed proofs of the soundness and the completeness of the semantics.

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.

Linear lambdacalculus: Give the full details of a linear lambdacalculus and prove its basic properties (n.b., there are several variants of a linear lambdacalculus, 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)