mechanical proof checkers for type soundness?

• To: types@cis.upenn.edu
• Subject: mechanical proof checkers for type soundness?
• From: Eric Allen <ericeallen@mac.com>
• Date: Tue, 14 Oct 2003 20:30:29 -0400

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.

Thanks,

Eric Allen
Sun Microsystems Laboratories

• Prev: Call for PhD and Post PhD Grant Applications
• Next: ICLP'03: call for participation
• Index(es):
  • Main
  • Thread