dafny/deque.dfy (an implementation of deque in dafny)
dafny/free_list.dfy (an implementation of a free list in dafny)
hol/myPairScript.sml (an implementation of product type in HOL)
hol/mySumScript.sml (an implementation of sum type using my product type)
hol/surjEpicScript.sml (a proof that surjective function is epic)
Interesting ones
dafny/funopw.dfy (an implemenation of a higher order function funpow that accept a partial function as argument in dafny, which is more clumsy than what I expected)
hol/partialFunctionScript.sml (an implementation of a partial function type in HOL)
hol/fibScript.sml (an proof and implementation of calculating fibonacci using matrix and exponentiation by squaring (using the fact that matrix multiplicatoin is associative)
hol/posetScript.sml (some proofs about proset (poset without antisym) and completet lattices)