skip to main content
10.1145/1088454.1088457acmconferencesArticle/Chapter ViewAbstractPublication PagesicfpConference Proceedingsconference-collections
Article

A unified category-theoretic formulation of typed binding signatures

Published: 27 September 2005 Publication History

Abstract

We generalise Fiore et al's account of variable binding for untyped cartesian contexts and Tanaka's account of variable binding for untyped linear contexts to give an account of variable binding for simply typed axiomatically defined contexts. In line with earlier work by us, we axiomatise the notion of context by means of a pseudo-monad S on Cat: Fiore et al implicitly used the pseudo-monad Tfp for small categories with finite products, and Tanaka implicitly used the pseudo-monad Tsm for small symmetric monoidal categories. But here we also extend from untyped variable binding to typed variable binding. Given a set A of types, this involves generalising from Fiore et al's use of [F,Set] to [(SA)op,SetA]. We define a substitution monoidal structure on [(SA)op,SetA], give a definition of binding signature at this level of generality, and extend initial algebra semantics to this typed, axiomatic setting. This generalises and axiomatises previous work by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, and it yields an improved axiomatic definition of binding signature even in the case of untyped binders.

References

[1]
M. Fiore, Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proc. PPDP 02, ACM Press, pages 26--37, 2002.]]
[2]
M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. LICS 99, pages 193--202. IEEE Press, 1999.]]
[3]
M. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In Proc. LICS 99, pages 214--224. IEEE Press, 1999.]]
[4]
M. Hofmann, Semantical analysis of higher-order abstract syntax. In Proc. LICS 99, IEEE Press, pages 204--213, 1999.]]
[5]
M. Hyland and A. J. Power. Pseudo-commutative monads and pseudo-closed 2-categories. J. Pure and Applied Algebra 175:141--185, 2002.]]
[6]
B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.]]
[7]
G. B. Im and G. M. Kelly. A universal property of the convolution monoidal structure. J. Pure Appl. Algebra, 43:75--88, 1986.]]
[8]
G. M. Kelly. An abstract approach to coherence. In Coherence in categories, LNM 281, pages 106--147, 1972.]]
[9]
G. M. Kelly. Basic Concepts of Enriched Category Theory, London Math. Soc. Lecture Notes Series 64 Cambridge University Press, 1982.]]
[10]
S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.]]
[11]
M. Miculan and I. Scagnetto, A framework for typed HOAS and semantics. In Proc. PPDP 2003, ACM Press, pages 184--194, 2003.]]
[12]
P. O'Hearn, On Bunched Typing, Journal of functional Programming, 13:747-796, Cambridge University Press, 2003.]]
[13]
P. O'Hearn and R. D. Tennent, Algol-like Languages, Progress in Theoretical Computer Science Series, Birkhauser, 1997.]]
[14]
G. D. Plotkin and A. J. Power. Algebraic Operations and Generic Effects. In Proc. MFCSIT 2000, Applied Categorical Structures 11:69--94, 2003.]]
[15]
A. J. Power. Why Tricategories? Information and Computation, 120:251--262, 1995.]]
[16]
A. J. Power. Enriched Lawvere theories. Theory and Applications of Categories, 6:83--93, 1999.]]
[17]
A. J. Power. A Unified Category-Theoretic Approach to Variable Binding. In Proc. MERLIN 2003, ACM Digital Library, 2003.]]
[18]
A. J. Power. Countable Lawvere theories and Computational Effects. Submitted.]]
[19]
A. J. Power and M. Tanaka. Pseudo-Distributive Laws and Axiomatics for Variable Binding. Submitted.]]
[20]
A. J. Power and M. Tanaka. Binding Signatures for Generic Contexts In Proc. Typed Lambda Calculi and Applications 2005, LNCS 3461, pages 308--323, 2005.]]
[21]
A. J. Power and M. Tanaka. A Unified Category-Theoretic Semantics for Binding Signatures in Substructural Logics. Submitted.]]
[22]
D. Pym. The Semantics and Proof Theory of the Logic of Bunched Implications, Applied Logic Series. Kluwer, 2002.]]
[23]
M. Tanaka. Abstract syntax and variable binding for linear binders. In Proc. MFCS 2000, LNCS 1893, pages 670--679, 2000.]]
[24]
M. Tanaka. Pseudo-Distributive Laws and a Unified Framework for Variable Binding. Edinburgh Ph.D. thesis, 2004.]]

Cited By

View all
  • (2022)Implementing a category-theoretic framework for typed abstract syntaxProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503678(307-323)Online publication date: 17-Jan-2022
  • (2014)Modules over relative monads for syntax and semanticsMathematical Structures in Computer Science10.1017/S096012951400010326:1(3-37)Online publication date: 5-Dec-2014
  • (2010)Modules over monads and initial semanticsInformation and Computation10.1016/j.ic.2009.07.003208:5(545-564)Online publication date: 1-May-2010
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding
September 2005
72 pages
ISBN:1595930728
DOI:10.1145/1088454
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 September 2005

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. binding signature
  2. pseudo-distributive law
  3. pseudo-monad
  4. substitution monoidal structure
  5. variable binding

Qualifiers

  • Article

Conference

MERLIN05
Sponsor:

Upcoming Conference

ICFP '25
ACM SIGPLAN International Conference on Functional Programming
October 12 - 18, 2025
Singapore , Singapore

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)2
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Implementing a category-theoretic framework for typed abstract syntaxProceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3497775.3503678(307-323)Online publication date: 17-Jan-2022
  • (2014)Modules over relative monads for syntax and semanticsMathematical Structures in Computer Science10.1017/S096012951400010326:1(3-37)Online publication date: 5-Dec-2014
  • (2010)Modules over monads and initial semanticsInformation and Computation10.1016/j.ic.2009.07.003208:5(545-564)Online publication date: 1-May-2010
  • (2008)Category Theoretic Semantics for Typed Binding Signatures with RecursionFundamenta Informaticae10.5555/2365856.236586184:2(221-240)Online publication date: 1-Apr-2008
  • (2008)Category Theoretic Semantics for Typed Binding Signatures with RecursionFundamenta Informaticae10.5555/1402673.140267884:2(221-240)Online publication date: 1-Apr-2008
  • (2008)Second-Order and Dependently-Sorted Abstract SyntaxProceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science10.1109/LICS.2008.38(57-68)Online publication date: 24-Jun-2008
  • (2008)Capture-avoiding substitution as a nominal algebraFormal Aspects of Computing10.1007/s00165-007-0056-120:4-5(451-479)Online publication date: 15-Jan-2008
  • (2007)Modules over monads and linearityProceedings of the 14th international conference on Logic, language, information and computation10.5555/1770176.1770192(218-237)Online publication date: 2-Jul-2007
  • (2007)Higher-order semantic labelling for inductive datatype systemsProceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1273920.1273933(97-108)Online publication date: 14-Jul-2007
  • (2007)Modules over Monads and LinearityLogic, Language, Information and Computation10.1007/978-3-540-73445-1_16(218-237)Online publication date: 2007
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media