by James Cheney (beware, PDF takes up full screen)

Based on envious observations of the success of formal methods for verifying industrial hardware designs using model-checking, I will argue that "partial" techniques which provide full automation and search for counterexamples, but which do not try to verify correctness, are likely to be more useful [for "metatheory of logics and programming languages"] on a day-to-day basis activities than full verification. I will describe an unsophisticated, yet useful, implementation of such a "model-checking" approach to mechanized metatheory implemented using nominal logic programming (although the basic idea could be employed in many other settings).

Model checking meets POPLMark. I can't tell from this presentation if there's any chance of using tools similar to BLAST to search deeper or produce actual proofs.

## Recent comments

4 hours 12 min ago

5 hours 57 min ago

14 hours 14 min ago

14 hours 14 min ago

14 hours 49 min ago

16 hours 24 min ago

18 hours 42 min ago

21 hours 31 min ago

22 hours 8 min ago

22 hours 57 min ago