Matthews, Seán Programming Logics, MPI for Informatics, Max Planck Society;
https://rdcu.be/dt9vd (出版社版)
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.