A few notes from the Isabelle rewrite

zilch-lang / zilch

A statically-typed, low-level, functional programming language with some focus on runtime performance

BSD 3-Clause "New" or "Revised" License

25 stars 0 forks source link

A few notes from the Isabelle rewrite #22

Closed Mesabloo closed 1 year ago

Mesabloo commented 1 year ago

Here's a list of things that are to be done but that I can't do right now:

[ ] prove the termination of the function in src/Syntax/CST.thy, which computes the height of a CST it shouldn't be quite hard, as this is merely a structural mutual induction;
[ ] prove the termination of the import resolver in src/Syntax/ImportResolver.thy

Mesabloo commented 1 year ago

This is now irrelevant. All of the code is being rewritten following a refinement-style implementation. So the "old" code does not really matter anymore.