It would be a very good idea to verify that our type systems are at least sound (no program that does not typecheck is valid, and evaluation preserves typing).
It is not necessary to check that the type system is complete (meaning that no valid program does not typecheck).
The tool of preference here would be Coq, though any theorem prover works.
For now, only the type system for N⋆ can be verified (fortunately, a small-step operational semantics is already defined) but the type system for Zilch will soon be “finished”.
It would be a very good idea to verify that our type systems are at least sound (no program that does not typecheck is valid, and evaluation preserves typing). It is not necessary to check that the type system is complete (meaning that no valid program does not typecheck).
The tool of preference here would be Coq, though any theorem prover works.
For now, only the type system for N⋆ can be verified (fortunately, a small-step operational semantics is already defined) but the type system for Zilch will soon be “finished”.