Walther Recursion. - David A. McAllester; Kostas Arkoudas (CADE, 1996)

Denotational proof languages. - Konstantinos Arkoudas (2000)