Index of /users/jared/milawa/Sources/Isabelle
Name Last modified Size Description
Parent Directory -
Cheap/ 09-Jun-2009 20:24 -
Demo/ 09-Jun-2009 20:24 -
Isar/ 09-Jun-2009 20:24 -
Arithmetic.thy 09-Jun-2009 20:24 12K
Base.thy 09-Jun-2009 20:24 11K
ListUtilities.thy 09-Jun-2009 20:24 30K
Makefile 09-Jun-2009 20:24 171
MapUtilities.thy 09-Jun-2009 20:24 14K
NumericListUtilities..> 09-Jun-2009 20:24 14K
ROOT.ML 09-Jun-2009 20:24 87
debug-trace.sh 09-Jun-2009 20:24 1.7K
root.tex 09-Jun-2009 20:24 811
Milawa/Sources/Isabelle directory
This directory holds the beginnings of an attempt to formalize the Milawa
core proof checker in Isabelle/HOL, as a means to investigate its soundness
mechanically.
This was about the first thing I ever did in Isabelle/HOL, so it is probably
all completely horrible. Also, it's old enough that Milawa still had integers
rather than naturals, so most of what's here is probably needing to be redone.
At any rate, I never got very far with this project. I leave it here since
one day it might be interesting to return to.