From e15be90e6dd69189e0e9e6f778649f8474593fa6 Mon Sep 17 00:00:00 2001 From: Grigore Rosu Date: Tue, 23 Apr 2024 09:29:18 -0500 Subject: [PATCH] Update index.md --- teaching/2024/cs522/index.md | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/teaching/2024/cs522/index.md b/teaching/2024/cs522/index.md index 977d227..d3f207b 100644 --- a/teaching/2024/cs522/index.md +++ b/teaching/2024/cs522/index.md @@ -133,3 +133,32 @@ need* and more topics will be added. - Recursion, Types, Polymorphism * Recursion and Types. [Slides](CS522-Spring-2024-Recursion.pdf) * Polymorphism. [Slides](CS522-Spring-2024-Polymorphism.pdf) + +- ### Extra-Credit (due Friday, May 03, AoE) + + This can be regarded as "Final exam", but it only counts as HW + (and not project) extra-credit and has the same weight as any of the + previous HWs. If you got a good score so far for the 6 HWs above, + then you do not need to do this extra-credit. Choose one, and only + one, of the following and do it well (you will get either 10 or 0 + for this extra-credit problem!): + + 1. Proposition 8 from the slides on simply-typed lambda calculus. Exercises 5 and 6 from the slides on CCCs. + + 2. Consider the PCF language with call-by-value (note that the + slides above define the call-by-name variant). Give it a small-step, + a big-step, and a denotational semantics in Maude, using the + representations of these semantic approaches discussed in the first + part of the class. Provide also 5 (five) PCF programs that can be + used to test all three of your semantics. You can use the builtins + provided as part of the previous HWs (you should only need the + generic substitution from there). + + 3. This has two problems. The first is to define a type checker for + the parametric polymorphic lambda-calculus (or System F). The second + is to define a type checker for the subtype polymorphic + lambda-calculus. In both cases, make sure that you also include the + conditional and a few examples showing that your definition works. + Feel free to pick whatever syntax you want for the various + constructs (both for terms and for types). +