Matthews, Seán Programming Logics, MPI for Informatics, Max Planck Society;
Matthews, S. (1996). Implementing $\textrm FS_0$ in Isabelle: Adding Structure at the Metalevel. In L. C. Paulson (Ed.), Design and Implementation of Symbolic Computation Systems (DISCO'96) (pp. 228-239). Berlin, Germany: Springer.