Matthews, Seán Programming Logics, MPI for Informatics, Max Planck Society;
https://rdcu.be/dt9vd (Publisher version)
Matthews, S. (1996). Implementing FS0 in Isabelle: Adding Structure at the Metalevel. In L. C. Paulson (Ed.), Design and Implementation of Symbolic Computation Systems (pp. 228-239). Berlin, Germany: Springer.