Operational Semantics I
Due on Wednesday, March 4th at 11:59 PM. This is a team lab. You may work alone or you may work with a partner. If you’d like to work with a partner, make sure to indicate your preferred partner using Teammaker and be familiar with the Partner Etiquette guidelines. You may discuss the concepts of this lab with other classmates, but you may not share your code with anyone other than course staff and your lab partner(s). Do not look at solutions written by students other than your team. If your team needs help, please post on the Piazza forum or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask than to risk violating the Academic Integrity Policy.
Overview
This lab will require you to work with operational semantics and encodings. You will construct proofs of F♭ evaluation using the operational semantics defined in the book. You will also define encodings and operational semantics of your own. As usual, you will use Teammaker to form your repositories.
Assignment Structure
This assignment is largely written with a small F♭ programming component. For the written portion, you are required to use LaTeX. Furthermore, you are required to use the proof notation which appears in the textbook. If you have any difficulty using LaTeX or irtex.py to produce this notation or any questions about correct notation, please ask your instructor.
As in the previous assignment, your repository contains a document assignment4.tex which contains the questions you are to answer. You may begin the assignment by running make assignment4.pdf. Each question will indicate whether its answer is to be written in LaTeX (in which case it should be written in answers.tex) or in F♭ (in which case the question will indicate the appropriate source file). You may run make answers.pdf or just make in order to build the PDF containing your answers.
To ease the process of writing proofs, this lab includes a script irtex.py that will generate appropriate LaTeX code from a textual description of your rules and proofs. You can write your description in the file assignment4.irf according to the syntax described in the irtex.py guide; when you run make, a file assignment4.irf.tex will be generated which will containg the LaTeX version of your proofs and rules; you may then typeset them into the document by using the appropriate commands. You will not need to run irtex.py yourself, but you may do so if you like or inspect the generated output at your leisure.
To support development of your F♭ encodings, a working F♭ interpreter fb.byte has been provided. You may run it using ocamlrun fb.byte (or rlwrap ocamlrun fb.byte).
Deliverables
For the LaTeX portion of the assignment, the contents of answers.tex will be considered. For the F♭ programming portion, the appropriate .fb files will be considered. In both cases, files which contain syntax errors or other flaws which prevent them from being compiled or interpreted will not receive full credit.
Submitting
To submit your lab, just commit and push your work. The most recent pushed commit as of the due date will be graded. For more information on when assignments are due, see the Policies page.
Lab Questionnaire
In addition to completing the lab itself, you’ll also need to complete a questionnaire describing your experience in the lab. Under most circumstances, this questionnaire will take only about a minute to complete and is part of your participation grade. Please make sure to do this; the information is useful to develop the course and the credit you get is basically free!
If You Have Trouble…
…then please contact your instructor! Piazza is the preferred method, but you can reach out via e-mail as well. Good luck!