Heterogeneous substitution systems revisited

DOI10.4230/LIPICS.TYPES.2015.2MaRDI QIDQ4580223zbMATHOpenAlexFDO

Authors Benedikt Ahrens, Ralph Matthes

Publication date 13 August 2018

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

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)

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.

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

Cites work

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

Cited in

(3)

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

Describes a project that uses

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)