Abstract
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 λ-binders and the ∇ quantifier. These features allow reasoning directly on expressions containing bound variables.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A.: A User Guide to Bedwyr (November 2006)
Elliott, C., Pfenning, F.: A semi-functional implementation of a higher-order logic programming language. In: Lee, P. (ed.) Topics in Advanced Language Implementation, pp. 289–325. MIT Press, Cambridge (1991)
Girard, J.-Y.: A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu (February 1992)
McDowell, R., Miller, D.: A logic for reasoning with higher-order abstract syntax. In: Proc. LICS 1997, pp. 434–445. IEEE Comp. Soc. Press, Los Alamitos (1997)
McDowell, R., Miller, D., Palamidessi, C.: Encoding transition systems in sequent calculus. Theoretical Computer Science 294(3), 411–437 (2003)
Miller, D.: Abstract syntax for variable binders: An overview. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 239–253. Springer, Heidelberg (2000)
Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. on Computational Logic 6(4), 749–783 (2005)
Nadathur, G., Linnell, N.: Practical higher-order pattern unification with on-the-fly raising. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 371–386. Springer, Heidelberg (2005)
Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp. 199–208. ACM Press, New York (1988)
Sagonas, K., Swift, T., Warren, D.S., Freire, J., Rao, P., Cui, B., Johnson, E., de Castro, L., Marques, R.F., Dawson, S., Kifer, M.: The XSB Version 3.0, vol. 1: Programmer’s Manual (2006)
Schroeder-Heister, P.: Rules of definitional reflection. In: Proc. LICS 1993, pp. 222–232. IEEE Comp. Soc. Press, Los Alamitos (1993)
Tiu, A.: A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University (May 2004)
Tiu, A.: Model checking for π-calculus using proof search. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 36–50. Springer, Heidelberg (2005)
Tiu, A., Nadathur, G., Miller, D.: Mixing finite success and finite failure in an automated prover. In: Proc. of ESHOL 2005: Empirically Successful Automated Reasoning in Higher-Order Logics, pp. 79–98 (December 2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baelde, D., Gacek, A., Miller, D., Nadathur, G., Tiu, A. (2007). The Bedwyr System for Model Checking over Syntactic Expressions. In: Pfenning, F. (eds) Automated Deduction – CADE-21. CADE 2007. Lecture Notes in Computer Science(), vol 4603. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73595-3_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-73595-3_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73594-6
Online ISBN: 978-3-540-73595-3
eBook Packages: Computer ScienceComputer Science (R0)