rder Abstract Syntax in Isabelle/HOL Douglas J. Howe Carleton University July 13, 2010 Douglas J. Howe (Carleton University) HOAS in Isabelle/HOL July 13, 2010 1 / 8
Abstract. In order to make existing formalizations available for settheoretic developments, we present an automated translation of theories from Isabelle/HOL to Isabelle/ZF. This c...
Using HOL4, we mechanise termination and correctness for two unification algorithms, written in a recursive descent style. One computes unifiers for first order terms, the other fo...