Index of /users/jared/milawa/Sources/Isabelle

Icon  Name                    Last modified      Size  Description
[DIR] Parent Directory                             -   
[DIR] Cheap/                  09-Jun-2009 20:24    -   
[DIR] Demo/                   09-Jun-2009 20:24    -   
[DIR] Isar/                   09-Jun-2009 20:24    -   
[   ] Arithmetic.thy          09-Jun-2009 20:24   12K  
[TXT] Base.thy                09-Jun-2009 20:24   11K  
[TXT] ListUtilities.thy       09-Jun-2009 20:24   30K  
[   ] Makefile                09-Jun-2009 20:24  171   
[TXT] 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.