We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Abstract clones for abstract syntax

Abstract: We give a formal treatment of simple type theories, such as the simply-typed $\lambda$-calculus, using the framework of abstract clones. Abstract clones traditionally describe first-order structures, but by equipping them with additional algebraic structure, one can further axiomatize second-order, variable-binding operators. This provides a syntax-independent representation of simple type theories. We describe multisorted second-order presentations, such as the presentation of the simply-typed $\lambda$-calculus, and their clone-theoretic algebras; free algebras on clones abstractly describe the syntax of simple type theories quotiented by equations such as $\beta$- and $\eta$-equality. We give a construction of free algebras and derive a corresponding induction principle, which facilitates syntax-independent proofs of properties such as adequacy and normalization for simple type theories. Working only with clones avoids some of the complexities inherent in presheaf-based frameworks for abstract syntax.
Comments: To appear in the proceedings of FSCD 2021; 16 pages
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
ACM classes: F.3.2; F.4.1
Cite as: arXiv:2105.00969 [cs.LO]
  (or arXiv:2105.00969v1 [cs.LO] for this version)

Submission history

From: Nathanael Arkor [view email]
[v1] Mon, 3 May 2021 16:09:55 GMT (334kb,D)

Link back to: arXiv, form interface, contact.