/software-foundations

solutions for software foundations textbook problems

Primary LanguageCoqMIT LicenseMIT

#f03c15 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

  1. Basics: clear
  2. Induction: 1 excercise unsolved(binary_inverse)
  3. Lists: 1 excercise unsolved(bag_theorem)
  4. Poly: 1 excercise unsolved(church_numerals: exp)
  5. Tactics: 3 excercises unsolved(split combine, filter_excercise, forall_exists_challenge)
  6. Logic: 2 excercise unsolved(tr_rev, classical_axioms)
  7. IndProp: I skipped everything related with regualr expressions.
  8. Map: someday...