# The Bedwyr system for model checking over syntactic expressions

## D. Baelde, A. Gacek, D. Miller, G. Nadathur, A. Tiu

### 21st Conference on Automated Deduction (Frank Pfenning, ed.), LNAI, no. 4603, Springer, 2007, pp. 391-397

Bedwyr is a generalization of logic programming that allows model
checking directly on syntactic expressions possibly containing
bindings. This system, written in OCaml, is a direct implementation of
two recent advances in the theory of proof search. The first is
centered on the fact that both finite success and finite failure can
be captured in the sequent calculus by incorporating inference rules
for definitions that allow fixed points to be explored. As a result,
proof search in such a sequent calculus can capture simple model
checking problems as well as may and must behavior in operational
semantics. The second is that higher-order abstract syntax is directly
supported using term-level lambda and the nabla. These features allow
reasoning directly on expressions containing bound variables.