[isabelle-dev] auto raises a TYPE exception

Makarius 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 mailing list