Pinned Repositories
TCSReadingGroup
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 Without Tears.
artin-algebra
Solutions to Algebra, by Michael Artin.
BilbyInCakeML
Translating specification of BilbyFS (written in Isabelle/HOL) into the same language environment as CakeML (HOL4)
cakeml
CakeML: A Verified Implementation of ML
cogent
Proof-Code Cogeneration
Completeness-Proof
Mechanising modal logic completeness proof in HOL4
HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
HOL-cbvlcm
HOL4 transaltion of the Coq code provided by "Formal Verification of a Call-by-value Lambda Calculus Machine" (https://www.ps.uni-saarland.de/extras/cbvlcm2/)
HOL-wcbv-reasonable
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/)
Register-Machine-in-HOL4
Mechanising the equivalence proof from Register Machine to Recursive Functions in HOL4
ZhuoZoeyChen's Repositories
ZhuoZoeyChen/BilbyInCakeML
Translating specification of BilbyFS (written in Isabelle/HOL) into the same language environment as CakeML (HOL4)
ZhuoZoeyChen/Register-Machine-in-HOL4
Mechanising the equivalence proof from Register Machine to Recursive Functions in HOL4
ZhuoZoeyChen/artin-algebra
Solutions to Algebra, by Michael Artin.
ZhuoZoeyChen/cakeml
CakeML: A Verified Implementation of ML
ZhuoZoeyChen/cogent
Proof-Code Cogeneration
ZhuoZoeyChen/Completeness-Proof
Mechanising modal logic completeness proof in HOL4
ZhuoZoeyChen/HOL
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
ZhuoZoeyChen/HOL-cbvlcm
HOL4 transaltion of the Coq code provided by "Formal Verification of a Call-by-value Lambda Calculus Machine" (https://www.ps.uni-saarland.de/extras/cbvlcm2/)
ZhuoZoeyChen/HOL-wcbv-reasonable
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/)
ZhuoZoeyChen/QuickFuzz
An experimental grammar fuzzer in Haskell using QuickCheck