►7400:   i  PPL
▼Problem Sets
    ← prev  up  next → 

Problem Set 6

home work!

Topic Type Checking

Purpose The goal of this problem set is to formulate a set of type checking rules.

image

Problem 1 Equip your standard reduction model of DADL with a set of type checking rules that implement the checker of problem set 3. Name the judgment wf-dd.

Design evaluate. The function consumes a configuration. If it type checks, it produces the list of room names visited according to ->dd-std until the first cycle is encountered. Otherwise it produces '("type error!").

Use traces to illustrate the conjecture that for a configuration c every configuration reachable with ->dd-std type checks. You will need the following Racket function:
;  t -> boolean
; (type-checks? t) determines whether the wf-dd judgment holds for t
(define (type-checks? t)
  (judgment-holds (wf-dd ,t)))
Place all such tests into a module+ called sr.

Deliverable Email a tar.gz bundle to my CCS email address whose name combines 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 6.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.

The README.txt file must start with the following lines:

  ;; NameOfPartner1, NameOfPartner2

  ;; email@of.partner1.com, email@of.partner2.org

appropriately instantiated of course.

    ← prev  up  next →