Some proofs written in Dafny and HOL4

Simple ones

• 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)