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

Problem Set 7

home work!

Topic Modeling a Full-fledged Language and Proving Type Safety

Purpose This problem set has two distinct goals. First, you will work on a comparison of a program with a model. Second, you will do a proof of type soundness.

image

Problem 1 The solutions to the first six problem sets constitute both an implementation of DADL as well as a model. You are now in a position to compare the two to find out whether they are in sync.

image

Figure 1: Comparing language implementations and models

See figure 1 for a diagramatic overview of the process. Here are the files that implement the mechanics of this comparison process:

  • cmp.bash, a Unix bash script that compares the two for more than a dozen test files located in a local Tests/ directory;

  • 3.rkt and 3-parser.rkt, the Racket solution to Problem Set 3, including an XML-to-S-expression (term) parser;

  • 6.rkt, my Redex solution to Problem Set 6;

  • 7-script.rkt, a Racket file that turns a Redex solution into a Unix script.

The last script, 7-script.rkt re-uses 3-parser.rkt, the raw parser from problem set 3, because the comparison effort focuses on the static (type) checking and the semantics of the model and assumes basic parsing is easy and requires no checks.

Task Your task is to adapt 7-script.rkt to your solutions for Problem Set 3 and Problem Set 6. First, you will have to adjust the path to Racket’s executable in the header of the script so that it points to your Racket installation. Second, you need to read the Redex language definition in 6.rkt and the Racket code in 7-script.rkt. Third, you must modify the parser in 7-script.rkt so that it translates the XML files into your representation of DADL in Redex. Fourth, you export evaluate from your version of 6.rkt so that 7-script.rkt can import it; see my stub solution for how to export a function from a module. Finally, you can run cmp.bash. This comparison script takes the path to the two executable on the command line:

  $ ./cmp.bash ./3.rkt ./7-script.rkt

and assume that the XML test files are located in a "Tests/" directory. It runs the two executables on each file in "Tests/" and diff’s the outcomes.

When the comparison process discovers a discrepancy between your implementation and your model, investigate and fix either the implementation or the model to eliminate the discrepancy. Then describe the discrepancy in a paragraph of at most 30 words in your README file. You may add a five-line sample XML configuration to a paragraph if you wish to illustrate your point.

Problem 2 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 my office by 1pm on March 20th.

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 your 7-script.rkt Racket file.

To grade problem 1, I will use your solutions to Problem Set 3 and Problem Set 6 as turned it with the latter. This gives me a chance to check on the discrepancies you discovered or those that you didn’t discover.

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

  ;; NameOfPartner1, NameOfPartner2

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

appropriately instantiated of course. For this homework, use the README to report on the discrepancies found in problem 1.

    ← prev  up  next →