SIGACT news logic column 14

ABSTRACT

For this issue, James Cheney describes nominal logic, an approach to solve the problems involved with reasoning about bindings in formal languages that has been gaining in popularity in recent years, and surveys its major application areas.

REFERENCES

• 1: M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375--416, 1991.
• 2: Andreas Abel. A third-order representation of the λ μ-calculus. In S. J. Ambler, R. L. Crole, and A. Momigliano, editors, MERLIN 2001: Mechanized Reasoning about Languages with Variable Binding, volume 58(1) of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.
• 3: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLmark Challenge. In Proceedings of the Eighteenth International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), 2005. To appear.
• 4: Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, July 2005
• 5: H. P. Barendregt. The Lambda Calculus. North-Holland, 1984.
• 6: Henk Barendregt. The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic, 3(2):181--215, June 1997.
• 7: Eli Barzilay and Stuart F. Allen. Reflecting higher-order abstract syntax in Nuprl. In Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02), pages 23--32, 2002.
• 8: Luís Caires , Luca Cardelli, A Spatial Logic for Concurrency (Part II), Proceedings of the 13th International Conference on Concurrency Theory, p.209-225, August 20-23, 2002
• 9: L. Cardelli, P. A. Gardner, and G. Ghelli. Manipulating trees with hidden labels. In A. D. Gordon, editor, Proc. of the Sixth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '03), Lecture Notes in Computer Science, pages 216--232. Springer-Verlag, 2003.
• 10: 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]
• 11: James Cheney. The complexity of equivariant unification. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP 2004), volume 3142 of LNCS, pages 332--344. Springer-Verlag, 2004.
• 12: James Cheney. Completeness and Herbrand theorems for nominal logic. Journal of Symbolic Logic, 2005. Accepted for publication.
• 13: James Cheney. Equivariant unification. In Proceedings of the 2005 Conference on Rewriting Techniques and Applications (RTA 2005), number 3467 in LNCS, pages 74--89, 2005.
• 14: James Cheney, Scrap your nameplate: (functional pearl), Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 15: James Cheney. A simpler proof theory for nominal logic. In Proceedings of the 2005 Conference on Foundations of Software Science and Computation Structures (FOSSACS 2005), number 3441 in LNCS, pages 379--394. Springer-Verlag, 2005.
• 16: James Robert Cheney , Greg Morrisett, Nominal logic programming, 2004
• 17: Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56--68, 1940.
• 18: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7 ]
• 19: H. B. Curry. Grundlagen der kombinatorischen Logik. American Journal of Mathematics, 52:509--536, 789--834, 1930.
• 20: H. B. Curry and R. Feys. Combinatory Logic. North-Holland, 1958.
• 21: N. G. de Bruijn. Lambda-calculus notation with nameless dummies, a tool for automatic formula manipulation. Indagationes Mathematicae, 34(5):381--392, 1972.
• 22: Joëlle Despeyroux , Amy P. Felty , André Hirschowitz, Higher-Order Abstract Syntax in Coq, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.124-138, April 10-12, 1995
• 23: Ulrich Felgner. Models of ZF-Set Theory. Number 223 in Lecture Notes in Mathematics. Springer-Verlag, 1970.
• 24: Maribel Fernández and Murdoch Gabbay. Nominal rewriting with name generation: abstraction vs. locality. In Barahona and Felty {4}, pages 47--58.
• 25: Maribel Fernández , Murdoch J. Gabbay , Ian Mackie, Nominal rewriting systems, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.108-119, August 24-26, 2004, Verona, Italy [doi>10.1145/1013963.1013978]
• 26: Gian Luigi Ferrari, Ugo Montanari, and Emilio Tuosto. Model cheeking for nominal calculi. In Sassone {70}, pages 1--24.
• 27: 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
• 28: A. Fraenkel. The concept "definite" and the independence of the Auswahlsaxiom. In J. van Heijenoort, editor, From Frege to Gödel, pages 284--289. Harvard University Press, 1967.
• 29: G. Frege, Begriffsschrift: a formula language, modeled upon that of arithmetic, for pure thought. In J. van Heijenoort, editor, From Frege to Gödel, pages 1--82. Harvard University Press, 1967.
• 30: M. J. Gabbay. A Theory of Inductive Definitions with Alpha-Equivalence. PhD thesis, University of Cambridge, 2001.
• 31: M. J. Gabbay. FM-HOL, a higher-order theory of names. In F. Kamareddine, editor, Workshop on Thirty Five years of Automath, Heriot Watt, UK, April 2002.
• 32: M. J. Gabbay. Fresh logic: A logic of FM, 2003. Preprint.
• 33: M. J. Gabbay. The π-calculus in FM. In Fairouz Kamareddine, editor, Thirty-five years of Automath. Kluwer, 2003.
• 34: Murdoch Gabbay , James Cheney, A Sequent Calculus for Nominal Logic, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.139-148, July 13-17, 2004 [doi>10.1109/LICS.2004.6]
• 35: Murdoch Gabbay , Andrew Pitts, A New Approach to Abstract Syntax Involving Binders, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.214, July 02-05, 1999
• 36: M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13:341--363, 2002.
• 37: Murdoch J. Gabbay, A new calculus of contexts, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.94-105, July 11-13, 2005, Lisbon, Portugal [doi>10.1145/1069774.1069783]
• 38: H. Ganzinger, editor. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), Turku, Finland, 2004. IEEE.
• 39: John Hanna. Type systems for closure conversions. In Proceedings of the Workshop on Types for Program Analysis, pages 48--62, 1995.
• 40: J. Hannan , D. Miller, A meta-logic for functional programming, Meta-programming in logic programming, MIT Press, Cambridge, MA, 1989
• 41: Robert Harper. Systems of polymorphic type assignment in LF. Technical report, Carnegie Mellon University, 1990. CMU-CS-90-144.
• 42: D. Hilbert and W. Ackermann. Grundzüge der Mathematischen Logik. Springer-Verlag, 1928.
• 43: 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
• 44: Furio Honsell and Marino Miculan. A natural deduction approach to dynamic logic. In S. Berardi et al, editor, Types '95 Conf. Proc., volume 1158 of Lecture Notes in Computer Science, pages 165--182, 1996.
• 45: Furio Honsell , Marino Miculan , Ivan Scagnetto, An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.963-978, July 08-12, 2001
• 46: Gérard Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27--67, 1975.
• 47: Thomas J. Jech. About the axiom of choice. In J. Barwise, editor, Handbook of Mathematical Logic, pages 345--370. North-Holland, 1977.
• 48: Ralf Lämmel and Simon Peyton Jones. Scrap your boilerplate with class. In Benjamin Pierce, editor, Proceedings of the 10th International Conference on Functional Programming (ICFP 2005), Tallinn, Estonia, 2005.
• 49: Leonid Libkin, Elements Of Finite Model Theory (Texts in Theoretical Computer Science. An Eatcs Series), SpringerVerlag, 2004
• 50: Giuseppe Longo, editor. Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, 1999. IEEE, IEEE Press.
• 51: Ian A. Mason. Hoare's logic in the LF. Technical Report ECS-LFCS-87-32, University of Edinburgh, 1987.
• 52: James Mckinna , Robert Pollack, Some Lambda Calculus and Type Theory Formalized, Journal of Automated Reasoning, v.23 n.3, p.373-409, November 1999 [doi>10.1023/A:1006294005493 ]
• 53: Marino Miculan , Ivan Scagnetto , Furio Honsell, Translating specifications from nominal logic to CIC with the theory of contexts, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.41-49, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088454.1088460]
• 54: M./ Miculan and K. Yemane. A uniying model of variables and names. In Sassone {70}, pages 170--186.
• 55: Dale Miller. An extension to ML to handle bound variables in data structures. In Proceedings of the First ESPRIT BRA Workshop on Logical Frameworks, pages 323--335, 1990.
• 56: Dale Miller , Alwen Tiu, A Proof Theory for Generic Judgments: An extended abstract, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.118, June 22-25, 2003
• 57: G. Nadathur and D. Miller. Higher-order logic programming. In D. M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, chapter 8, pages 499--590. Oxford University Press, 1998.
• 58: M. Norrish. Recursive function definitions for types with binders. In Proceedings of the 2004 Conference on Theorem Proving and Higher-Order Logics, number 3223 in LNCS, pages 241--256. Springer-Verlag, 2004.
• 59: Martin Odersky, A functional theory of local names, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.48-59, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.175187]
• 60: Frank Pfenning, Logical frameworks, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 61: 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
• 62: 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
• 63: 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]
• 64: A. M. Pitts. Alpha-structural recursion and induction (extended abstract). In J. Hurd and T. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford UK, August 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 17--34. Springer-Verlag, 2005.
• 65: Andrew M. Pitts , Murdoch Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.230-255, July 03-05, 2000
• 66: Andrew M. Pitts , Ian D. B. Stark, Observable Properties of Higher Order Functions that Dynamically Create Local Names, or What's new?, Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, p.122-141, August 30-September 03, 1993
• 67: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, September 2005
• 68: François Pottier. An overview of Cαml. In Proceedings of the 2005 ACM SIGPLAN Workshop on ML (ML 05), Tallinn, Estonia, September 2005.
• 69: D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer ACademic Publishers, 2002.
• 70: V. Sassone, editor. Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2005), volume 3441 of LNCS, Edinburgh, UK, April 2005. Springer-Verlag.
• 71: M. Schönfinkel. On the building blocks of mathematical logic. In J. van Heijenoort, editor, From Frege to Gödel, pages 355--366. Harvard University Press, 1967.
• 72: Ulrich Schöpp and Ian Stark. A dependent type theory with names and binding. In Proceedings of the 2004 Computer Science Logic Conference, number 3210 in Lecture notes in Computer Science, pages 235--249, Karpacz, Poland, 2004.
• 73: C. Schürmann, R. Fontana, and Y. Liao. Delphin: Functional programming with deductive systems. Available at http://cs-www.cs.yale.edu/homes/carsten/, 2002.
• 74: Carsten Schurmann , Joelle Despeyroux , Frank Pfenning, Primitive recursion for higher-order abstract syntax, Theoretical Computer Science, v.266 n.1-2, p.1-57, 09/06/2001 [doi>10.1016/S0304-3975(00)00418-7 ]
• 75: 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
• 76: Mark R. Shinwell, Swapping the atom: Programming with binders in Fresh O'Caml. In Furio Honsell, Marino Miculan, and Alberto Momigliano, editors, Proceedings of the Second ACM SIGPLAN Workshop on Mecahnized Reasoning about Languages with Binding (MERLIN 2003), pages 171--175, 2003.
• 77: M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761--783, 1982.
• 78: Ian Stark. Free-algebra models for the π-calculus. In Sassone {70}, pages 155--169.
• 79: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1981
• 80: Christian Urban , Michael Norrish, A formal treatment of the barendregt variable convention in rule inductions, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.25-32, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088454.1088458]
• 81: 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]
• 82: C. Urban and C. Tasson. Nominal techniques in Isabelle/HOL. In R. Nieuwenhuis, editor, Proc. of the 20th International Conference on Automated Deduction (CADE), volume 3632 of Lecture Notes in Computer Science, pages 38--53, 2005.
• 83: Christian Urban and James Cheney. Avoiding equivariant unification. In Proceedings of the 2005 Conference on Typed Lambda Calculus and Applications (TLCA 2005), number 3461 in LNCS, pages 74--89. Springer-Verlag, 2005.
• 84: Myra Ellen Vaninwegen , Carl Gunter, The machine-assisted proof of programming language properties, 1996
• 85: René Vestergaard , James Brotherston, A formalised first-order confluence proof for the λ-calculus using one-sorted variable names, Information and Computation, v.183 n.2, p.212-244, 15 June 2003 [doi>10.1016/S0890-5401(03)00023-3]
• 86: Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework: The propositional fragment. In Proceedings of TYPES 2003, pages 355--377, 2003.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Operations on languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Languages, Theory