Heterogeneous substitution systems revisited

DOI10.4230/LIPICS.TYPES.2015.2zbMATH Open1433.68220arXiv1601.04299OpenAlexW4394790805MaRDI QIDQ4580223FDOQ4580223

Benedikt Ahrens, Ralph Matthes

Publication date: 13 August 2018

Abstract: Matthes and Uustalu (TCS 327(1-2):155-174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.

Full work available at URL: https://arxiv.org/abs/1601.04299

Recommendations

• Abstract syntax: substitution and binders
• From signatures to monads in \textsf{UniMath}
• Substitution in non-wellfounded syntax with variable binding
• Some Wellfounded Trees in UniMath
• A Unified Category-theoretic Semantics for Binding Signatures in Substructural Logics

zbMATH Keywords

nested datatypesformalization of category theoryMendler-style recursion schemesrepresentation of substitution in languages with variable binding

Mathematics Subject Classification ID

Categorical semantics of formal languages (18C50) Abstract data types; algebraic specification (68Q65) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• From signatures to monads in \textsf{UniMath}
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Constructing categories and setoids of setoids in type theory
• Univalent categories and the Rezk completion
• Substitution: A formal methods case study using monads and transformations
• Iteration and coiteration schemes for higher-order and nested datatypes
• Disciplined, efficient, generalised folds for nested datatypes
• Generalised folds for nested datatypes
• de Bruijn notation as a nested datatype
• Title not available (Why is that?)
• Map fusion for nested datatypes in intensional type theory
• Inductive types and type constraints in the second-order lambda calculus
• Monads need not be endofunctors
• Substitution in non-wellfounded syntax with variable binding
• Termination checking with types
• Modules over monads and initial semantics
• Modules over Monads and Linearity
• An experimental library of formalized Mathematics based on the univalent foundations
• Universe Polymorphism in Coq
• Some Wellfounded Trees in UniMath
• Title not available (Why is that?)

Cited In (3)

• From signatures to monads in \textsf{UniMath}
• Substitution in non-wellfounded syntax with variable binding
• C-system of a module over a \(Jf\)-relative monad

Uses Software

• Coq
• UniMath
• GitHub

This page was built for publication: Heterogeneous substitution systems revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4580223)