- Abstract:
-
The problem of formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has received comparatively little attention. In this paper, we consider the problem of bounded model-checking for metatheoretic properties of formal systems specified using nominal logic. In contrast to current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the common case that a flaw is detected. Two counterexample search strategies are considered, one employing negation-as-failure and the other based on negation elimination; we compare the two approaches from the point of view of semantic complexity, implementation effort, and efficiency.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-1090,
- author = {
James Cheney
and Alberto Momigliano
},
- title = {Mechanized Metatheory Model-Checking},
- book title = {Proceedings of the 9th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'07) (University of Wroclaw, Poland)},
- publisher = {ACM Press},
- year = 2007,
- month = {Jul},
- pages = {75-86},
- doi = {10.1145/1273920.1273931},
- url = {http://homepages.inf.ed.ac.uk/amomigl1/papers/chenmomi.pdf},
- }
|