# FinalProjectInstructions

# General Instructions

# Topics

- Bourbaki-Witt fixpoint theorem and its three applications
- Knaster-Tarski fixpoint theorem and one of its application
- Equivalence among 3 denotational semantics and small step semantics
- Small-steps vs. denotations for programs with break and continue
- Denotations vs. Hoare logic for programs with break and continue
- Small-steps vs. denotations for programs with function calls
- Equivalence among denotations for programs with function calls
- Denotations vs. Hoare logic for programs with function calls
- Executable semantics for lambda calculus with reference and IO
- Executable semantics for programs with addresses, fork/join and IO
- Denotation-based transformation correctness for constant folding
- Simulation-based transformation correctness for constant folding
- Simulation-based transformation correctness for dead assignment elimination
- Denotation-based transformation correctness for dead assignment elimination
- Algorithm correctness of Strassen's matrix multiplication
- Algorithm correctness of Mobius transformation
- Algorithm correctness of discrete Fourier transform
- Algorithm correctness of splay operation
- Implementation correctness of doubly linked list via VST
- Implementation correctness of splay operation via VST
- Implementation correctness of threaded BST via VST
- Implementation correctness of red-black tree insertion via VST

# Teams

# Schedule and Check Points

## Team member confirmation

## Proposal submission

## Midterm report

## Midterm report - second check

## Final submission

# Grades

- 20 : complete;
- 16 - 19: small number of minor holes appearing in proofs;
- 12 - 15: big number of minor holes appearing in proofs;
- 8 - 11 : one major hole in proofs;
- 0 - 7 : more than one major holes in proofs;
- one or two points may be taken off if you miss check points;
- one or two points may be taken off if important defitions and intermediate results are not clearly stated.

- 1: 4-student team on normal projects
- 3: 3-student team on normal projects
- 4: single student or 2-student team on normal projects
- 5: self designed hard projects (graded when tasks are settled).

# Why you should use a version control system

- Popular version control systems are very accesible.
- Most IT companies use version control systems. You need to get familiar
with it anyway in the future.
- You will not lose your developement (maybe 2 or 3 weeks work) due to
a computer breakdown.
- You may have some back-and-forth when desiging definitions and proofs.
Version control systems can help you find your earlier versions back.
- A version control system help record the contribution of every individual. If your teammates complaint that you does not work hard on the project, you can use these record to justify your own contribution.

(* 2021-05-07 20:38 *)