Problem Set 5

Purpose The goal of this problem set is to get some experience with typing derivations, to formulate a set of type checking rules, and to do a proof of type soundness.

Problem 1 due Friday, February 26 at beginning of class.

Problem 2 due Tuesday, March 1 at 1pm.

Problem 3 due Friday, March 4 at beginning of class.

Problem 1 See here. Solutions to this problem should be submitted on paper at the beginning of class on February 26th.

Problem 2 Equip your general reduction model of FSL with a set of type checking rules that implement the checker of problem set 3. Name the judgment wf-fsl.

Design evaluate. The function consumes a configuration. If the configuration fails to type check, it produces "type error!". If the configuration type checks and there exists some path to the required destination according to ->fsl, it produces "Flight plan found"; otherwise it produces "No flights found".

If you think the above conjecture is true, explain why in 30 words or less. If your tests have shown the conjecture to be false, explain why and say how you would alter wf-fsl to make the conjecture hold, making sure to justify the gap between the original and altered wf-fsl.

Problem 3 First, read Chapters 8 and 9 of Types and Programming Languages (TAPL). Make sure you understand the details of proving type soundness for Arith and STLC via progress and preservation.

Next, see here. Solutions to this problem should be submitted on paper at the beginning of class on March 4th.

Deliverable For Problem 2, email a tar.gz bundle to to me and Ben Chung at our CCS email addresses. The name of the bundle should combine the last names of the pair in alphabetical order. The tar bundle must contain a single directory—with the same name as the tar ball—with a README.txt file and a 5.rkt Redex file. Your solution must also contain a solution to problem 3 from Problem Set 3, revised according to grader feedback. Deliver this solution according to the specification in Problem Set 3.