mechanical proof checkers for type soundness?
I'm looking for a good mechanical proof checker for type soundness
proofs. I'm only interested in checking Wright-Felleisen-style
soundness proofs over small-step operational semantics for Java-like
languages, so I'd prefer it to be tailored as much as possible to that
task. Any recommendations? Right now, I'm leaning toward Isabelle.
Also, I'd prefer something that runs on Mac OS X, if possible.
Sun Microsystems Laboratories