Skip to content

Gordon-Sau/Proofs

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

25 Commits
 
 
 
 
 
 

Repository files navigation

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)

About

Some proofs in HOL and Dafny

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published