Document Open Access Logo

Dependent Types for Nominal Terms with Atom Substitutions

Authors Elliot Fairweather, Maribel Fernández, Nora Szasz, Alvaro Tasistro

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.180.pdf
  • Filesize: 454 kB
  • 16 pages

Document Identifiers

Author Details

Elliot Fairweather
Maribel Fernández
Nora Szasz
Alvaro Tasistro

Cite As Get BibTex

Elliot Fairweather, Maribel Fernández, Nora Szasz, and Alvaro Tasistro. Dependent Types for Nominal Terms with Atom Substitutions. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 180-195, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.180

Abstract

Nominal terms are an extended first-order language for specifying and verifying properties of syntax with binding. Founded upon the semantics of nominal sets, the success of nominal terms with regard to systems of equational reasoning is already well established. This work first extends the untyped language of nominal terms with a notion of non-capturing atom substitution for object-level names and then proposes a dependent type system for this extended language. Both these contributions are intended to serve as a prelude to a future nominal logical framework based upon nominal equational reasoning and thus an extended example is given to demonstrate that this system is capable of encoding various other formal systems of interest.

Subject Classification

Keywords
  • alpha-equivalence
  • nominal term
  • substitution
  • dependent type

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Robin Adams. Lambda-free logical frameworks. CoRR, abs/0804.1879, 2008. Google Scholar
  2. Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, and Lori Lorigo. The Nuprl open logical environment. In Automated Deduction - CADE-17, 2000. Google Scholar
  3. Franz Baader and Wayne Snyder. Unification theory. In Handbook of Automated Reasoning. Elsevier, 2001. Google Scholar
  4. Christophe Calvès and Maribel Fernández. Matching and alpha-equivalence check for nominal terms. Journal of Computer System Sciences, 76, 2010. Google Scholar
  5. Christophe Calvès and Maribel Fernández. The first-order nominal link. In Logic-Based Program Synthesis and Transformation - 20th International Symposium, LOPSTR 2010, Hagenberg, Austria, July 23-25, 2010, Revised Selected Papers, volume 6564 of Lecture Notes in Computer Science, pages 234-248. Springer, 2011. Google Scholar
  6. James Cheney. A simpler proof theory for nominal logic. In FoSSaCS, 2005. Google Scholar
  7. James Cheney. Completeness and Herbrand theorems for nominal logic. Journal of Symbolic Logic, 71, 2006. Google Scholar
  8. James Cheney. A simple nominal type theory. Electronic Notes in Theoretical Computer Science, 228, 2009. Google Scholar
  9. James Cheney. A dependent nominal type theory. Logical Methods in Computer Science, 8, 2012. Google Scholar
  10. Ranald A. Clouston. Equational Logic for Names and Binding. PhD thesis, University of Cambridge, 2010. Google Scholar
  11. Roy L. Crole and Frank Nebel. Nominal lambda calculus: An internal language for fm-cartesian closed categories. Electr. Notes Theor. Comput. Sci., 298:93-117, 2013. Google Scholar
  12. Elliot Fairweather. Type Systems for Nominal Terms. PhD thesis, King’s College London, 2014. Google Scholar
  13. Elliot Fairweather, Maribel Fernández, and Murdoch J. Gabbay. Principal types for nominal theories. In Proceedings of the 18th International Symposium on Fundamentals of Computation Theory (FCT 2011), 2011. Google Scholar
  14. Maribel Fernández and Murdoch J. Gabbay. Curry-style types for nominal terms. In Types for Proofs and Programs (TYPES'06). Springer, 2007. Google Scholar
  15. Maribel Fernández and Murdoch J. Gabbay. Nominal rewriting. Information and Computation, 205, 2007. Google Scholar
  16. Maribel Fernández and Murdoch J. Gabbay. Closed nominal rewriting and efficiently computable nominal algebra equality. In Proceedings of the 5th International Workshop on Logical Frameworks and Meta-Languages (LFMTP 2010), 2010. Google Scholar
  17. Murdoch J. Gabbay. A study of substitution, using nominal techniques and Fraenkel-Mostowski sets. Theoretical Computer Science, 410, 2009. Google Scholar
  18. Murdoch J. Gabbay. Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables. Mathematical Structures in Computer Science, 21, 2011. Google Scholar
  19. Murdoch J. Gabbay and James Cheney. A sequent calculus for nominal logic. In Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004. Google Scholar
  20. Murdoch J. Gabbay and Aad Mathijssen. Nominal algebra. In 18th Nordic Workshop on Programming Theory, 2006. Google Scholar
  21. Murdoch J. Gabbay and Aad Mathijssen. Capture-avoiding substitution as a nominal algebra. Formal Aspects of Computing, 20, 2008. Google Scholar
  22. Murdoch J. Gabbay and Aad Mathijssen. Nominal universal algebra: Equational logic with names and binding. Journal of Logic and Computation, 19, 2009. Google Scholar
  23. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proceedings of the 14th Annual Symposium on Logic in Computer Science (LICS 1999), pages 214-224. IEEE Computer Society Press, July 1999. Google Scholar
  24. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Proceedings of the 2nd IEEE Symposium on Logic in Computer Science (LICS 1987). IEEE Computer Society Press, 1987. Google Scholar
  25. Jordi Levy and Mateu Villaret. An efficient nominal unification algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), 2010. Google Scholar
  26. Zhaohui Luo. PAL^+: a lambda-free logical framework. Journal of Functional Programming, 13, 2003. Google Scholar
  27. Lena Magnusson and Bengt Nordström. The ALF proof editor and its proof engine. In Types for Proofs and Programs, (TYPES'93), 1994. Google Scholar
  28. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Transactions on Computational Logic, 9, 2008. Google Scholar
  29. Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. Google Scholar
  30. Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In Automated Deduction - CADE-16, 1999. Google Scholar
  31. Andrew M. Pitts. Nominal logic: A first order theory of names and binding. In Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software (STACS 2001), 2001. Google Scholar
  32. Andrew M. Pitts. Nominal system T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), 2010. Google Scholar
  33. Gordon Plotkin. An algebraic framework for logics and type theories, 2006. Talk given at LFMTP'06. Google Scholar
  34. Ulrich Schöpp and Ian Stark. A Dependent Type Theory with Names and Binding. In CSL, 2004. Google Scholar
  35. Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay. Nominal unification. Theoretical Computer Science, 323, 2004. Google Scholar
  36. Edwin Westbrook. Higher-order Encodings with Constructors. PhD thesis, Washington University in St. Louis, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact