Coq Related Project:
A Sudoku game developed by Coq from the mathematical proof perspective for CS386L Final Project
Sudoku Engine (Basic Log and Interactive Control) + Game Board + Game Repo
This page is used to share my solutions of Software Foundations textbook used for 2016 fall Programming Language class of SNU.
Notify
- I'll upload assignments' solution after due dates.
- I don't solve informal forms of problems.
- All excersied ared being solved in Aquamacs using coq-company package.
Progress of my travel to coq
- Basics: clear
- Induction: 1 excercise unsolved(binary_inverse)
- Lists: 1 excercise unsolved(bag_theorem)
- Poly: 1 excercise unsolved(church_numerals: exp)
- Tactics: 3 excercises unsolved(split combine, filter_excercise, forall_exists_challenge)
- Logic: 2 excercise unsolved(tr_rev, classical_axioms)
- IndProp: I skipped everything related with regualr expressions.
- Map: someday...