Phillip J. Windley

• The Live Web
• Digital Identity
• Higher order logic theorem proving and its applications
• Formal proof of the AVM-1 microprocessor using the concept of generic interpreters
• Higher Order Logic Theorem Proving and Its Applications
• The formal verification of generic interpreters