Heterogeneous Substitution Systems Revisited
DOI10.4230/LIPIcs.TYPES.2015.2zbMath1433.68220arXiv1601.04299OpenAlexW4394790805MaRDI QIDQ4580223
Benedikt Ahrens, Ralph Matthes
Publication date: 13 August 2018
Full work available at URL: https://arxiv.org/abs/1601.04299
nested datatypesformalization of category theoryMendler-style recursion schemesrepresentation of substitution in languages with variable binding
Abstract data types; algebraic specification (68Q65) Categorical semantics of formal languages (18C50) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Map fusion for nested datatypes in intensional type theory
- Substitution in non-wellfounded syntax with variable binding
- Modules over monads and initial semantics
- 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
- From signatures to monads in \textsf{UniMath}
- Inductive types and type constraints in the second-order lambda calculus
- Some Wellfounded Trees in UniMath
- Universe Polymorphism in Coq
- Constructing categories and setoids of setoids in type theory
- Modules over Monads and Linearity
- de Bruijn notation as a nested datatype
- Termination checking with types
- Monads need not be endofunctors
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Univalent categories and the Rezk completion
- An experimental library of formalized Mathematics based on the univalent foundations
This page was built for publication: Heterogeneous Substitution Systems Revisited
