Pinned Loading

1. Register-Machine-in-HOL4 Register-Machine-in-HOL4 Public

   Mechanising the equivalence proof from Register Machine to Recursive Functions in HOL4

   Standard ML 1

2. BilbyInCakeML BilbyInCakeML Public

   Translating specification of BilbyFS (written in Isabelle/HOL) into the same language environment as CakeML (HOL4)

   Isabelle 1

3. JamesShaker/TCSReadingGroup JamesShaker/TCSReadingGroup Public

   Running efforts of a HOL reading group mechanising M̶i̶c̶h̶a̶e̶l̶ ̶S̶i̶p̶s̶e̶r̶'̶s̶ ̶I̶n̶t̶r̶o̶d̶u̶c̶t̶i̶o̶n̶ ̶t̶o̶ ̶t̶h̶e̶ ̶T̶h̶e̶o̶r̶y̶ ̶o̶f̶ ̶C̶o̶m̶p̶u̶t̶a̶t̶i̶o̶n̶ Sidney Morris's Topology With…

   Standard ML 8 5

4. HOL-wcbv-reasonable HOL-wcbv-reasonable Public

   HOL4 transaltion of the Coq code provided by "The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space" (https://ps.uni-saarland.de/extras/wcbv-reasonable/)

   Standard ML