[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 11:25:46 CEST 2013
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.
More information about the isabelle-dev