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

16 weeks 3 days ago

16 weeks 4 days ago

16 weeks 4 days ago

38 weeks 5 days ago

43 weeks 5 hours ago

44 weeks 4 days ago

44 weeks 4 days ago

47 weeks 2 days ago

51 weeks 6 days ago

51 weeks 6 days ago