SCIENCE@home

Syntax and Semantics of Abstract Binding Trees

Jonathan Sterling,D. Morrison

Published 2016 in arXiv.org

ABSTRACT

The contribution of this paper is the development of the syntax and semantics of multi-sorted nominal abstract binding trees (abts), an extension of second order universal algebra to support symbol-indexed families of operators. Nominal abts are essential for correctly treating the syntax of languages with generative phenomena, including exceptions and mutable state. Additionally we have developed the categorical semantics for abstract binding trees formally in Constructive Type Theory using the Agda proof assistant. Multi-sorted nominal abts also form the syntactic basis for the upcoming version of the JonPRL proof assistant, an implementation of an extensional constructive type theory in the Nuprl tradition.

PUBLICATION RECORD

  • Publication year

    2016

  • Venue

    arXiv.org

  • Publication date

    2016-01-23

  • Fields of study

    Computer Science

  • Identifiers
    arXiv 1601.06298
  • External record

    Open on Semantic Scholar

  • Source metadata

    Semantic Scholar

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-20 of 20 references · Page 1 of 1

CITED BY