Higher-Order Superposition for Dependent Types. - Roberto Virga (RTA, 1996)

Efficient Substitution in Hoare Logic Expressions. - Roberto Virga (HOOTS, 2000)

A Stratified Semantics of General References A Stratified Semantics of General References. - Amal J. Ahmed 001; Andrew W. Appel; Roberto Virga (LICS, 2002)

A Trustworthy Proof Checker. - Andrew W. Appel; Neophytos G. Michael; Aaron Stump; Roberto Virga (J. Autom. Reason., 2003)