Students CAN pick a project which is NOT on this list.

Bourbaki-Witt fixpoint theorem

You should prove Bourbaki-Witt fixpoint theorem and reprove loop_recur using this theorem. For this purpose, you should define concepts like partial ordering w.r.t. an equivalent relation but not only w.r.t. equality. Difficulty estimation: 3. Slots remaining: 3.

Equivalence among 3 denotational semantics

You should first prove a general theorem which can be used to prove equivalence between two recursively defined semantics. Then, you need to prove the equivalence among all three recursively defined denotational semantics that we mentioned in class using this theorem. Difficulty estimation: 1. Slots remaining: 3.

Equivalence among 7 definitions of reflexive transitive closure

You should first formalize 3 definitions that we have not provided in class. Then you should prove the equivalence among 7 definitions of reflexive transitive closure. Difficulty estimation: 0. Slots remaining: 3.

Hoare logic's completeness theorem

Prove Imp's Hoare logic completeness. Difficulty estimation: 5. Slots remaining: 0.

First order logic's soundness theorem

You should prove first order logic's soundness theorem. You need to build all basic properties of FOL by yourself. Difficulty estimation: 4. Slots remaining: 3.

First order logic's completeness theorem

You should prove first order logic's completeness theorem. You do not need to build all basic properties of FOL by yourself. For necessary but elementary facts, you can state them and use them without proving. Difficulty estimation: 8. Slots remaining: 2.

Algorithm Correctness of Mobius transformation

You need to read Chapter 10.2, 10.3 and 10.3.1 of <<Parameterized Algorithm>> by Marek Cygan. You should formalize the algorithm for coloring counting using fast Mobius transformation. Its correctness is theorem 10.16 in the book. You should prove that algorithm's correctness in Coq. You only need to define this algorithm as a Coq function or a Coq relation (small step description of this algorithm). You do not need to implement it in a programming language. You do not need to verify its implementation in any programming language. Difficulty estimation: 5. Slots remaining: 3.

Algorithm Correctness of fast Fourier transform (FFT)

Discrete Fourier transformation can be used to compute big number's multiplication. FFT is a well-known efficient algorithm to calculate discrete fourier transformation. Your should learn how this algorithm works and prove its correctness in Coq. You need to either define this algorithm using complex numbers (you may find some library in Coq's standard library or other Coq's user's contribution) or via an abstract ring with some extra properties. You only need to define this algorithm as a Coq function or a Coq relation (small step description of this algorithm). You do not need to implement it in a programming language. You do not need to verify its implementation in any programming language. Difficulty estimation: 5. Slots remaining: 2.

Algorithm correctness for calculating longest increasing subsequence

LIS (longest increasing subsequence) is a famous problem which can solved in O(nlogn) time, in which n means the length of the whole sequence. Pick an algorithm for LIS with that time bound and prove its correctness. You only need to define this algorithm as a Coq function or a Coq relation (small step description of this algorithm). You do not need to implement it in a programming language. You do not need to verify its implementation in any programming language. Difficulty estimation: 4. Slots remaining: 3.

Implementation Correctness of binary search tree's via VST

You should first write a binary search tree in C and then verify its correctness using VST. This program should at least including insert, query (returning value / returning address), set (by key / by address), next, previous, begin, and end these operations. The following signature describes different query and set functions:

    typedef int value;
    typedef int key;
    value query_value(key k);
    struct tree * query_addr(key k);
    void set_by_key(key k, value v);
    void set_by_addr(struct tree * p, value v);

Difficulty estimation: 6. Slots remaining: 0.

Semantic equivalence for programs with break and continue

You should first define a Hoare logic, a denotational semantics and a small step semantics for a programming language with break and continue. Then you need to prove the equivalence between small step semantics and denotational semantics. Also, you should prove the soundness theorem of Hoare logic. Difficulty estimation: 7. Slots remaining: 0.

Semantic equivalence for programs with run-time error and nondeterminism

You should first define a Hoare logic, a denotational semantics and a small step semantics for a programming language with possible runtime error and some nondeterministic commands. Then you need to prove the equivalence between small step semantics and denotational semantics. Also, you should prove the soundness theorem of Hoare logic. Difficulty estimation: 4. Slots remaining: 3.