Final Project

For the final project, you can either (1) choose one of the TAPL-based or ATAPL-based projects described below, (2) choose a topic from the non-book-based projects list (for which there is less details and material to guide you along), or (3) invent your own project, pending approval from the instructor. If you plan to invent your own project, I suggest submitting your idea to me well before the deadline.

If you choose to invent your own project, I will be looking for the following criteria:

  1. It must exercise concepts and techniques covered in CS 225.
  2. There must be some reference material (e.g., a paper, book chapter, blog post, etc.) for me to look at, which you will base your project on. If no reference material exists, you can provide a more detailed sketch of the project goal in your proposal.
  3. The scope of the project must be achievable in the time you have to complete it.

Project descriptions may be mixed and matched, and I expect larger groups to tackle either (i) a more challenging project topic, or (ii) a combination of 2--3 less challenging project topics. Topics that are prefixed with an asterisk (*) are topics which we have already covered in class, but which you may combine with other project topics to enhance the difficulty. E.g., Type Reconstruction can be combined with References for a slightly more challenging project, or combined with Universal and/or Existential Quantification for a moderately more challenging project.

There will be 5 deliverables for the project. All deadlines are final with no extensions.

  1. Due Friday, April 20: Project Proposal
  2. Due Friday, April 27: Project Checkpoint
  3. Due Monday, April 30: Project Presentation Draft
  4. Tuesday May 01 and 03: Project Presentation
  5. Due Monday, May 07: Project Final Submission

Git

You will be required to use Git for your final project.

  1. If you do not already have a github account, make one.
  2. On all of your written materials (including the proposal), include your github handle underneath your names. (See the example proposal doc.)
  3. All team members should be listed as collaborators for your project.
  4. You will be required to set up github pages for your project with a readme and links to code and materials.

LaTeX

You will be required to use LaTeX for your final project.

  1. Install LaTeX on your personal machine if you haven't already. (This step may take a lot of time and/or disk space.)
  2. There are four documents you will need to produce: Proposal, Checkpoint, Draft Presentation, and Final Presentation. These must be typeset in LaTeX, however I will give you templates to work from.

Final Project—Proposal

Due Friday, April 20, 11:59pm

First, download the example LaTeX project and build the document. It should output a file main.pdf after you run make

Form a group of 1–4 people, and select a project topic (or combination of topics) from the final project webpage. In 2–4 pages, write a short description of what you plan on accomplishing, and how you plan to accomplish it.

Every member of your group must create a GitHub account. Select one member of your group to create a new repository and add the other members of the group to the repo as collaborators. In your writeup, you must write the github user names of each member of your group, as well as the url to your project repository. I should be able to build your writeup directly from your repository.

Submit your proposal by emailing it to me (as .pdf) with "CS 225 Project Proposal" in the subject line.

Final Project—Checkpoint

Due Friday, April 27, 11:59pm

I am looking for evidence that you have made progress on completing your final project. At a bare minimum, you should have started to write code, and identified key challenges upon which you are either stuck, or still need more time to complete.

First: Create a file in the root of your project repository called README. Include instructions in this README on how to build your code and run any test cases. Ideally, you will also have a Makefile, and to build your code, one need only run make.

When you commit and push your readme file, you should see it displayed on the front page of your repository on github.com. You do not need to create a writeup document in LaTeX for the checkpoint, however you must write a README file which gives a basic description of your project, and where to find the code you are working on.

When you are ready to submit your checkpoint, go to your project's page on github.com. Next to "commits" and "branch" links is a link called "releases"—click it. Click "Create a new release". For the tag version, write "checkpoint". For the release title, write "Checkpoint". Check the box for "This is a pre-release". Click "Publish release". Go back to your project home page. Normally on your project homepage there is a box that says "Branch: master". If you click this, then go to "Tags", you can click on "checkpoint". This will take you to the version of your code when you created the checkpoint. Feel free to keep working on your code as normal—I will use the checkpoint snapshot of your repository to grade your checkpoint.

Final Project—Presentation Draft

Due Monday, April 30, 11:59pm

You must prepare for a five-minute presentation in-class presentation. You must submit your slides to me the night before Tuesday's class regardless of when you will present. I encourage all group members to participate in the presentation. It is okay if you are still working on your project at this point, and some key deliverables are still TODO.

You must prepare five slides for your presentation:

  1. A title slide: the names of your group members and the project title—nothing else
  2. One slide with one very small program which motivates the need for your type system
  3. One slide with two interesting small-step semantics rules
  4. One slide with two interesting typing rules, or auxiliary rules used in typing rules (such as well-scoped from System F)
  5. One slide with any or all of the following: What was fun? What was hard? What did you learn?

Following your presentation I may ask a small question or two. If there is time we can let your classmates as a question or two.

Final Project—Presentation

In-class Tuesday, May 01 and Thursday, May 03

I will compile all submitted slides into a single presentation, and I will bring a presentation clicker to class for you to use. Each presentation should be five minutes (although it is okay if you go a little over or under).

Here is the presentation order (ascending by TAPL chapter, then ascending by last name):

Final Project—Final Submission

Due Monday, May 07, 11:59pm

There are two components to your final submission: (1) a written portion, and (2) an implementation portion. For the written portion, you must submit a writeup of your final project summarizing what you were able to accomplish. You should submit your writeup to me by email: David.Darais@uvm.edu. It should be no more than 6 pages, using the default latex layout for margins etc. For the implementation portion, create a snapshot of your project on github.com just like you did for the snapshot. Name the snapshot "final".

TAPL-based Projects

*References—TAPL Chapter 13

We saw references in class. This topic may not be chosen as the core topic for a final project, but may be selected as an "add-on".

Exceptions—TAPL Chapter 14

For supporting functions which throw exceptions, and functions which catch/handle exceptions. E.g., this technique will be similar to Java's checked exceptions. An extra option for this topic is to encode exceptions using monads (not covered in the book), implement exception semantics and typing using monads, and then compare with the approach in the book.

Subtyping—TAPL Chapter 15

For supporting types which form a subtype hierarchy. E.g., this technique will support record subtyping, which are similar to objects in object-oriented languages.

Object-oriented Programming—TAPL Chapters 18 and 19

For supporting classes and objects. E.g., this technique will support object-oriented concepts like super-classes, objects, and inheritance as found in Java.

Recursive Types—TAPL Chapter 20

For supporting recursive data-structure. E.g., this technique will support defining recursive datatypes like linked lists, as found in Java or OCaml.

Type Reconstruction—TAPL Chapter 22

For supporting type inference, which reduces the need to write type annotations in programs. E.g., this technique will support powerful type inference as found in OCaml.

*Univeral Quantification—TAPL Chapter 23

We saw universal quantification in class. This topic may not be chosen as the core topic for a final project, but may be selected as an "add-on".

*Existential Quantification—TAPL Chapter 24

We saw existential quantification in class. This topic may not be chosen as the core topic for a final project, but may be selected as an "add-on".

Bounded Quantification—TAPL Chapter 26

This topic is equivalent to combining Subtyping and Universal Quantification. A benefit of choosing this topic is that the book dedicates an explicit chapter for how to combine these features.

Higher-Order Polymorphism—TAPL Chapter 29

For supporting type operators and type-level computation. E.g., this technique will support parameterized types like lists (in both Java and OCaml), and provide the necessary machinery to typecheck complex instances of data abstraction.

Higher-Order Subtyping—TAPL Chapter 31

This topic is equivalent to combining Subtyping and Higher-Order Polymorphism. A benefit of choosing this topic is that the book dedicates an explicit chapter for how to combine these features.

Purely Functional Objects—TAPL Chapter 32

This topic is an extension of the previous topic, but applied to object oriented programming: classes, objects and inheritance.

ATAPL-based Projects

Linear Types—ATAPL Chapter 1

For supporting types which are "consumable". E.g., after a file is opened, it must be closed, and after it is closed, it may not be used again. Linear types support enforcing these types of invariants at the type level.

Dependent Types—ATAPL Chapter 2

For supporting types which depend on terms. This topic is a generalization of Higher-Order Polymorphism as described in TAPL. E.g., the type of the sort function might look like this: 
  sort : forall (n:nat), int_list n -> int_list n
which tracks at the type-level that the output list is the same length (n) as the input list.

Effect Types and Regions—ATAPL Chapter 3

For supporting the tracking of stack-allocated memory lifetimes. E.g., a function may allocate memory on its stack for a value, and pass a reference to that value to functions called within the body of the function. However, once the function returns, the pointer is no longer valid, because the lifetime of the stack frame has ended. Region types track these lifetimes at the type level. Effect types and regions are one of the core typechecking mechanisms in Rust, a programming language developed by Mozilla for developing efficient and secure web browsers.

Typed Assembly Language—ATAPL Chapter 4

For supporting type-checking of assembly code which is generated by compiling a more expressive, high-level language.

ML-Style Module Systems—ATAPL Chapter 8

For supporting modular data abstraction, linking, and separate compilation. E.g., OCaml's advanced module system is based on these concepts.

Advanced Type Inference (HM(X))—ATAPL Chapter 10

For supporting more advanced type inference (i.e., type reconstruction), as well as mechanisms for ad-hoc polymorphism. E.g., these concepts show up in Haskell's type classes and Rust's traits.

Non-book-based Projects

Information Flow Types

Based on this paper. A security-motivated type discipline which enforces that information about confidential data (e.g., passwords) is not leaked to unauthorized channels (e.g., an unauthorized user). The same mechanism can also apply to the dual problem of data integrity, which enforces that untrusted data (e.g., user input on an HTML form) does not influence high-integrity data (e.g., an internal SQL query).

Gradual Types

Based on this paper. Gradual type systems aim to support the seamless integration of typed languages with untyped languages, e.g., Javascript and a typed-dialect, or Ruby and a typed-dialect. Gradual typing has seen a lot of attention from the web-programming communities, e.g., at Microsoft, Facebook, Google, etc..

Last updated April 23, 2018