Theory files associated with Alan Martin's Ph. D. thesis:

Five formalizations of evaluation, typing, and subject reduction for Mini-ML with references, in Isabelle/HOL 2008 with Hybrid 0.2 (or 0.3, see below) and Brian Huffman's Ordinal theory:

MLref_1l.thy – One-level Approach
MLref_2l_J.thy – Two-level Approach (with intutionistic SL)
MLref_2l_L.thy – Linear Specification Logic
MLref_2l_LL.thy – Evaluation in the (Linear) SL
MLref_2l_O.thy – Ordered Specification Logic

An improved version of Hybrid, adding new lemmas abstr_cases, abstr_LAM, and expand_abstr and supporting compositional proof of abstr conditions via simp or auto:

Hybrid.thy – Hybrid 0.3

September 2010.