Nominal logic programming

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Nominal logic programming

Full text

Pdf (632 KB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 30 , Issue 5 (August 2008) table of contents

Article No. 26

Year of Publication: 2008

ISSN:0164-0925

Authors

James Cheney	University of Edinburgh, Edinburgh, Scotland
Christian Urban	Technische Universität, München

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 16, Downloads (12 Months): 183, Citation Count: 0

Additional Information:

appendices and supplements abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1387673.1387675 What is a DOI?

APPENDICES and SUPPLEMENTS

Cheney Appendix

Online appendix to designing mediation for context-aware applications. The appendix supports the information on article 26.

ABSTRACT

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, α-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J. 1991. Explicit substitutions. J. Funct. Prog. 4, 375--416.
	2	Aydemir, B. E., Bohannon, A., Fairbairn, M., Foster, J. N., Pierce, B. C., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., and Zdancewic, S. 2005. Mechanized metatheory for the masses: The PoplMark Challenge. In Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'05), J. Hurd and T. F. Melham, Eds. Lecture Notes in Computer Science, vol. 3603. Springer, 50--65.
	3	Barendregt, H. P. 1984. The Lambda Calculus. North-Holland.
	4	Iliano Cervesato, Proof-theoretic foundation of compilation in logic programming languages, Proceedings of the 1998 joint international conference and symposium on Logic programming, p.115-129, August 1998, Manchester, United Kingdom
	5	Iliano Cervesato , Frank Pfenning, A linear logical framework, Information and Computation, v.179 n.1, p.19-75, November 25, 2002 [doi>10.1006/inco.2001.2951]
	6	Cheney, J. 2004a. The complexity of equivariant unification. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04). Lecture Notes in Computer Science, vol. 3142. Springer-Verlag, 332--344.
	7	James Robert Cheney , Greg Morrisett, Nominal logic programming, Cornell University, Ithaca, NY, 2004
	8	Cheney, J. 2005a. Equivariant unification. In Proceedings of the Conference on Rewriting Techniques and Applications (RTA'05). Lecture Notes in Computer Science, vol. 3467, Springer-Verlag, 74--89.
	9	Cheney, J. 2005b. Relating nominal and higher-order pattern unification. In Proceedings of the 19th International Workshop on Unification (UNIF'05). 104--119.
	10	James Cheney, Scrap your nameplate: (functional pearl), Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
	11	Cheney, J. 2005d. A simpler proof theory for nominal logic. In Proceedings of the 8th International Conference on the Foundations of Software Science and Computational Structures (FOSSACS'05). Lecture Notes in Computer Science, vol. 3441, Springer-Verlag, 379--394.
	12	Cheney, J. 2006a. Completeness and Herbrand theorems for nominal logic. J. Symb. Logic 71, 1, 299--320.
	13	Cheney, J. 2006b. The semantics of nominal logic programs. In Proceedings of the International Conference on Logic Programing. Lecture Notes in Computer Science, vol. 4079. 361--375.
	14	Cheney, J. and Urban, C. 2004. Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In Proceedings of the 20th International Conference on Logic Programming (ICLP'04). Lecture Notes in Computer Science, vol. 3132, Springer-Verlag, 269--283.
	15	Cheng, A. S. K., Robinson, P. J., and Staples, J. 1991. Higher level meta programming in Qu-Prolog 3.0. In Proceedings of the International Conference on Logic Programming. 285--298.
	16	Church, A. 1940. A formulation of the simple theory of types. J. Symb. Logic 5, 56--68.
	17	Keith Clark , Peter J. Robinson , Richard Hagen, Multi-threading and message communication in Qu-Prolog, Theory and Practice of Logic Programming, v.1 n.3, p.283-301, May 2001 [doi>10.1017/S147106840100120X]
	18	W. F. Clocksin , Christopher S. Mellish, Programming in Prolog (3rd ed.), Springer-Verlag New York, Inc., New York, NY, 1987
	19	John Darlington , Yike Guo, Constraint Logic Programming in the Sequent Calculus, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, p.200-214, July 16-22, 1994
	20	Davey, B. A. and Priestley, H. A. 2002. Introduction to Lattices and Order. Cambridge University Press.
	21	Felty, A. 1993. Implementing tactics and tacticals in a higher-order logic programming language. J. Automa. Reason. 11, 1, 41--81.
	22	Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
	23	Murdoch Gabbay , James Cheney, A Sequent Calculus for Nominal Logic, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.139-148, July 13-17, 2004 [doi>10.1109/LICS.2004.6]
	24	Gabbay, M. J. and Pitts, A. M. 2002. A new approach to abstract syntax with variable binding. Formal Aspects Comput. 13, 341--363.
	25	Jean-Yves Girard, Linear logic, Theoretical Computer Science, v.50 n.1, p.1-102, Jan. 30, 1987 [doi>10.1016/0304-3975(87)90045-4]
	26	Makoto Hamana, A Logic Programming Language Based on Binding Algebras, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.243-262, October 29-31, 2001
	27	Hannan, J. and Miller, D. 1988. Uses of higher-order unification for implementing program transformers. In Proceedings of the 5th International Conference and Symposium on Logic Programming, Volume 2, R. A. Kowalski and K. A. Bowen, Eds. MIT Press, Cambridge, MA, 942--959.
	28	Michael Hanus, Horn clause programs with polymorphic types: semantics and resolution, Theoretical Computer Science, v.89 n.1, p.63-106, Oct. 21, 1991
	29	Hanus, M. 1994. The integration of functions into logic programming: From theory to practice. J. Logic Program. 19--20, 583--628.
	30	David Harel , Jerzy Tiuryn , Dexter Kozen, Dynamic Logic, MIT Press, Cambridge, MA, 2000
	31	Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
	32	Martin Hofmann, Semantical Analysis of Higher-Order Abstract Syntax, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.204, July 02-05, 1999
	33	Jaffar, J., Maher, M. J., Marriott, K., and Stuckey, P. J. 1998. The semantics of constraint logic programs. J. Logic Program. 37, 1--3, 1--46.
	34	Javier Leach , Susana Nieva , Mario Rodríguez-Artalejo, Constraint Logic Programming with Hereditary Harrop formulas, Theory and Practice of Logic Programming, v.1 n.4, p.409-445, July 2001 [doi>10.1017/S1471068401001041]
	35	J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
	36	Mason, I. A. 1987. Hoare's logic in the LF. Tech. rep. ECS-LFCS-87-32, University of Edinburgh.
	37	Dale Miller, A logical analysis of modules in logic programming, Journal of Logic Programming, v.6 n.1-2, p.79-108, Jan./Mar. 1989 [doi>10.1016/0743-1066(89)90031-9]
	38	Miller, D. 1990. An extension to ML to handle bound variables in data structures. In Proceedings of the 1st ESPRIT BRA Workshop on Logical Frameworks. 323--335.
	39	Miller, D. 1991. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Logic Computat. 1, 4, 497--536.
	40	Dale Miller, A Proposal for Modules in Lambda-Prolog, Proceedings of the 4th International Workshop on Extensions of Logic Programming, p.206-221, March 29-April 01, 1993
	41	Miller, D. and Nadathur, G. 1987. A logic programming approach to manipulating formulas and programs. In Proceedings of the Symposium on Logic Programming. 379--388.
	42	Miller, D., Nadathur, G., Pfenning, F., and Scedrov, A. 1991. Uniform proofs as a foundation for logic programming. Annals Pure Appl. Logic 51, 125--157.
	43	Dale Miller , Alwen Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic (TOCL), v.6 n.4, p.749-783, October 2005 [doi>10.1145/1094622.1094628]
	44	Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 3, 348--375.
	45	Robin Milner , Joachim Parrow , David Walker, A calculus of mobile processes, I, Information and Computation, v.100 n.1, p.1-40, Sept. 1992 [doi>10.1016/0890-5401(92)90008-4]
	46	John C. Mitchell , Krzysztof Apt, Concepts in Programming Languages, Cambridge University Press, New York, NY, 2001
	47	Alan Mycroft , Richard A. O'Keefe, A polymorphic type system for PROLOG., Artificial Intelligence, v.23 n.3, p.295-307, August 1984 [doi>10.1016/0004-3702(84)90017-1]
	48	Nadathur, G. and Miller, D. 1998. Higher-order logic programming. In Handbook of Logic in Artificial Intelligence and Logic Programming, D. M. Gabbay, C. J. Hogger, and J. A. Robinson, Eds. Vol. 5. Oxford University Press, Chapter 8, 499--590.
	49	Gopalan Nadathur , Dustin J. Mitchell, System Description: Teyjus - A Compiler and Abstract Machine Based Implementation of lambda-Prolog, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.287-291, July 07-10, 1999
	50	Nadathur, G. and Qi, X. 2005. Optimizing the runtime processing of types in polymorphic logic programming languages. In Proceedings of the International Conference on Logic Programming, Artificial Intelligence, and Reasoning, G. Sutcliffe and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 3835. Springer, 110--124.
	51	Peter Nickolas , Peter J. Robinson, The Qu-Prolog unification algorithm: formalisation and correctness, Theoretical Computer Science, v.169 n.1, p.81-112, Nov. 30, 1996 [doi>10.1016/S0304-3975(96)00115-6]
	52	O'Hearn, P. and Pym, D. J. 1999. The logic of bunched implications. Bull. Sym. Logic 5, 2, 215--244.
	53	Emir Pasalic , Tim Sheard , Walid Taha, DalI: An Untyped CBV Operational Semantics and Equational Theoryofr Datatypes with Binders(Technical Development), Oregon Graduate Institute School of Science & Engineering, 2000
	54	Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
	55	Frank Pfenning, Logical frameworks, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	56	F. Pfenning , C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.199-208, June 20-24, 1988, Atlanta, Georgia, United States
	57	Frank Pfenning , Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.202-206, July 07-10, 1999
	58	Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
	59	Andrew M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, v.186 n.2, p.165-193, 01 November 2003 [doi>10.1016/S0890-5401(03)00138-X]
	60	Andrew M. Pitts, Alpha-structural recursion and induction, Journal of the ACM (JACM), v.53 n.3, p.459-506, May 2006 [doi>10.1145/1147954.1147961]
	61	Pitts, A. M. and Gabbay, M. J. 2000. A metalanguage for programming with bound names modulo renaming. Lecture Notes in Computer Science, vol. 1837, Springer-Verlag, 230--255.
	62	Andrew M. Pitts , Mark R. Shinwell, Generative unbinding of names, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
	63	Pottier, F. 2005. An overview of Cαml. In Proceedings of the ACM SIGPLAN Workshop on ML (ML'05). ACM, 27--52.
	64	Francois Pottier, Static Name Control for FreshML, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.356-365, July 10-14, 2007 [doi>10.1109/LICS.2007.44]
	65	John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
	66	Davide Sangiorgi , David Walker, PI-Calculus: A Theory of Mobile Processes, Cambridge University Press, New York, NY, 2001
	67	Ulrich Schöpp, Modelling Generic Judgements, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.5, p.19-35, June, 2007 [doi>10.1016/j.entcs.2007.01.027]
	68	Mark R. Shinwell , Andrew M. Pitts, On a monadic semantics for freshness, Theoretical Computer Science, v.342 n.1, p.28-55, 6 September 2005 [doi>10.1016/j.tcs.2005.06.003]
	69	Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.263-274, August 25-29, 2003, Uppsala, Sweden
	70	J. Staples , P. J. Robinson , R. A. Paterson , R. A. Hagen , A. J. Craddock , P. C. Wallis, Qu-Prolog: an extended Prolog for meta level programming, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
	71	Leon Sterling , Ehud Shapiro, The art of Prolog (2nd ed.): advanced programming techniques, MIT Press, Cambridge, MA, 1994
	72	Alwen Tiu, A Logic for Reasoning about Generic Judgments, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.5, p.3-18, June, 2007 [doi>10.1016/j.entcs.2007.01.016]
	73	Urban, C. and Cheney, J. 2005. Avoiding equivariace in Alpha-Prolog. In Proceedings of the 2005 Conference on Typed Lambda Calculus and Applications (TLCA 2005). Lecture Notes in Computer Science, vol. 3461, Springer-Verlag, 74--89.
	74	Christian Urban , Andrew M. Pitts , Murdoch J. Gabbay, Nominal unification, Theoretical Computer Science, v.323 n.1-3, p.473-497, 14 September 2004 [doi>10.1016/j.tcs.2004.06.016]
	75	Urban, C. and Tasson, C. 2005. Nominal techniques in Isabelle/HOL. In Proceedings of the 20th International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 3632. 38--53.
	76	M. H. Van Emden , R. A. Kowalski, The Semantics of Predicate Logic as a Programming Language, Journal of the ACM (JACM), v.23 n.4, p.733-742, Oct. 1976 [doi>10.1145/321978.321991]
	77	Watkins, K., Cervesato, I., Pfenning, F., and Walker, D. 2003. A concurrent logical framework: The propositional fragment. In Proceedings of TYPES. 355--377.