Pages that link to "Item:Q4256148"
From MaRDI portal
The following pages link to de Bruijn notation as a nested datatype (Q4256148):
Displayed 31 items.
- Map fusion for nested datatypes in intensional type theory (Q627204) (← links)
- Substitution in non-wellfounded syntax with variable binding (Q703526) (← links)
- A principled approach to programming with nested types in Haskell (Q848745) (← links)
- Explicit substitutions and higher-order syntax (Q853744) (← links)
- Modules over monads and initial semantics (Q964503) (← links)
- Iteration and coiteration schemes for higher-order and nested datatypes (Q1770412) (← links)
- Confluence of the coinductive \(\lambda\)-calculus (Q1884931) (← links)
- Nested abstract syntax in Coq (Q1945918) (← links)
- A formalized general theory of syntax with bindings: extended version (Q1984791) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- Rensets and renaming-based recursion for syntax with bindings (Q2104549) (← links)
- Deep induction: induction rules for (truly) nested types (Q2200833) (← links)
- From signatures to monads in \textsf{UniMath} (Q2319990) (← links)
- Strongly typed term representations in Coq (Q2392480) (← links)
- Some Wellfounded Trees in UniMath (Q2819193) (← links)
- A unified treatment of syntax with binders (Q3165528) (← links)
- (Q3384910) (← links)
- Why Would You Trust B? (Q3498474) (← links)
- Polarised subtyping for sized types (Q3535676) (← links)
- Implementing a normalizer using sized heterogeneous types (Q3638918) (← links)
- An induction principle for nested datatypes in intensional type theory (Q3638923) (← links)
- Heterogeneous Substitution Systems Revisited (Q4580223) (← links)
- (Q5013813) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- 2-Dimensional Directed Type Theory (Q5739362) (← links)
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic (Q6060672) (← links)
- Rensets and renaming-based recursion for syntax with bindings extended version (Q6111524) (← links)
- Variable binding and substitution for (nameless) dummies (Q6151566) (← links)
- Fantastic morphisms and where to find them. A guide to recursion schemes (Q6164203) (← links)
- Variable binding and substitution for (nameless) dummies (Q6181939) (← links)
- Towards an induction principle for nested data types (Q6199585) (← links)