Informatics Report Series


Report   

EDI-INF-RR-1090


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Mechanized Metatheory Model-Checking
Authors: James Cheney ; Alberto Momigliano
Date:Jul 2007
Publication 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
Publication Type:Conference Paper Publication Status:Published
Page Nos:75-86
DOI:10.1145/1273920.1273931 ISBN/ISSN:978-1-59593-769-8
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh