Ludos sicut Mathematica

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).