Recursive Boolean Functions in HOL. - Flemming Andersen; Kim Dam Petersen (TPHOLs, 1991)

Program Verification using HOL-UNITY. - Flemming Andersen; Kim Dam Petersen; Jimmi S. Pettersson (HUG, 1993)

Graph model of LAMBDA in Higher Order Logic. - Kim Dam Petersen (HUG, 1993)

A Graphical Tool for Proving Unity Progress. - Flemming Andersen; Kim Dam Petersen; Jimmi S. Pettersson (TPHOLs, 1994)

The HOL-UNITY Verification System. - Flemming Andersen; Ulla Binau; Karsten Nyblad; Kim Dam Petersen; Jimmi S. Pettersson (TAPSOFT, 1995)