The Caml Hump: Bedwyr

Bedwyr is an extended logic programming language that allows model-checking directly on syntactic expressions possibly containing bindings. We believe that it's an interesting tool for computer scientists, as it allows simple reasoning on declarative specifications, with several good examples, notably bisimulation checking for the pi-calculus. Other examples include type systems, games, logics, etc.