Operational Semantics of Structure
Due on Thursday, October 23rd 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 Courselore or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask and learn than to guess!
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 is a written LaTeX assignment about the operational semantics of F♭ and related languages. You are required to use LaTeX for this assignment. Your proofs must be complete and are strongly encouraged to take one of two forms from the textbook: traditional inference proof notation or the equivalent bulleted proof notation. You may optionally the tool irtex.py in your repository to write proofs rather than writing them in LaTeX directly; see below for a description.
As in the previous assignment, your repository contains a document assignment6.tex which contains the questions you are to answer. You may begin the assignment by running make assignment6.pdf and reading the resulting document. Your answers should be written in answers.tex which you can build via make answers.pdf.
irtex.py
Writing inference proofs in LaTeX can be disorienting if you’re not accustomed to the syntax involved: it’s very easy to mistype a brace and have trouble tracking it down. This lab includes a script irtex.py that will generate LaTeX for you. The advantage of this tool is that you don’t have to wrangle the LaTeX yourself; the disadvantage is that you have to learn how to use it.
The irtex.py script reads a file, answers.irf, in your repository and, based on its contents, generates another file: answers.irf.tex. This process is based upon a tiny domain-specific language, IRF, which is built for this purpose; you can read about that language and see simple examples in the irtex.py guide. If you write proofs in answers.irf, you can typeset them in your answers.tex by invoking the appropriate command (e.g. \proofProblemOneA). You will not need to run irtex.py yourself. The Makefile will do that for you.
If you’d rather write the proofs in LaTeX yourself, you’re welcome to do so. Neither approach is clearly easier or simpler than the other; irtex.py is just here as an option if you find the nested proof syntax in LaTeX to be uncomfortable to use.
Deliverables
To complete this assignment, write answers.tex (and, optionally, answers.irf) in such a way that make produces an answers.pdf with correct answers to the questions appearing in assignment6.pdf. Files which do not compile cannot be assigned credit, so please be sure that your document builds correctly. If you have any questions about formatting, requirements, or LaTeX, please let me know! (Especially about LaTeX. I’m happy to help get you unstuck!)
Submitting
It is not enough to push your work. In your repository, you will find a Python script called submit.py. In order to submit your lab assignment, it should be sufficient to run that script by typing python3 submit.py in your terminal. For this script to work correctly, you must have committed all uncommitted files in your repository and pushed your work so that your repository is in sync with your GitHub remote repository.
The aforementioned Python script is designed to create a Git tag: a name for a specific commit in your repository. (The script also performs a series of checks to help ensure that the tag you create contains what you likely think it contains.) The tag will be named using the words “submission”, the name of your assignment, and a version number. Your instructor will know that you have submitted your work because this tag will appear in your repository. If you need to resubmit your work to correct changes after receiving a grade, you can simply create new commits and then create another tag (preferrably with submit.py). At any given time, only your most recent outstanding submission will be graded.
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 lets me know whether I’m asking for the right amount of work and helps to ensure that it’s a good use of your time.
If You Have Trouble…
…then please contact your instructor! Courselore is the preferred method, but you can reach out via e-mail as well. Good luck!