Bindings as bounded natural functors

Conference paper

Blanchette, J., Gheri, L., Popescu, A. and Traytel, D. 2019. Bindings as bounded natural functors. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Hotel Cascais Miragem, Cascais, Portugal 13 - 19 Jan 2019 Association for Computing Machinery (ACM). https://doi.org/10.1145/3290335
TypeConference paper
TitleBindings as bounded natural functors
AuthorsBlanchette, J., Gheri, L., Popescu, A. and Traytel, D.
Abstract

We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is “concrete” enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle/HOL.

Research GroupFoundations of Computing group
Conference46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)
Proceedings TitleProceedings of the ACM on Programming Languages
ISSN2475-1421
Electronic2475-1421
PublisherAssociation for Computing Machinery (ACM)
Publication dates
Print02 Jan 2019
Publication process dates
Deposited12 Nov 2019
Accepted10 Oct 2018
Output statusPublished
Publisher's version
License
Accepted author manuscript
License
Copyright Statement

© 2019 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.

Digital Object Identifier (DOI)https://doi.org/10.1145/3290335
LanguageEnglish
Book titleProceedings of the ACM on Programming Languages, Volume 3 Issue POPL
Permalink -

https://repository.mdx.ac.uk/item/88964

Log in to edit

Download files

Publisher's version
popl19main-p56-p.pdf
License: CC BY 4.0

File access - Request a copy

Restricted files

Accepted author manuscript

  • 25
    total views
  • 8
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as