On Tue, 28 May 2013, Christian Sternagel wrote:
Hopefully it is all a bit more precise now. Maybe someone wants to
formalize pattern.ML + unify.ML after > 20 years, to pin down the
remaining uncertaincies about type instantiation within these
non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor.
Unfortunately I'm not a proven expert ;)
For the formalization part, the one who is actually doing it is by
definition the "proving expert". After some decades of prover technology
built around these former core parts of Isabelle, it should be more
feasible than ever before.
What happens at the moment is just the usual attempt to get existing ML
modules in a slightly better form, without breaking down completely.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
