de Bruijn notation as a nested datatype
From MaRDI portal
De Bruijn notation as a nested datatype
Recommendations
- scientific article; zbMATH DE number 3908332
- scientific article; zbMATH DE number 1890156
- Intersection type system with de Bruijn indices
- Notes on de Bruijn sequences
- scientific article; zbMATH DE number 3995075
- A Class of de Bruijn Sequences
- DE BRUIJN SEQUENCES REVISITED
- De Bruijn sequences revisited
- De Bruijn sequences for fixed-weight binary strings
- scientific article; zbMATH DE number 1615230
Cited in
(43)- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Syntax monads for the working formal metatheorist
- scientific article; zbMATH DE number 7447767 (Why is no real title available?)
- From signatures to monads in \textsf{UniMath}
- Rensets and renaming-based recursion for syntax with bindings
- Viewing \({\lambda}\)-terms through maps
- scientific article; zbMATH DE number 1615230 (Why is no real title available?)
- Nameless, painless
- scientific article; zbMATH DE number 2090073 (Why is no real title available?)
- Substitution in non-wellfounded syntax with variable binding
- Variable binding and substitution for (nameless) dummies
- Explicit substitutions and higher-order syntax
- An induction principle for nested datatypes in intensional type theory
- Fantastic morphisms and where to find them. A guide to recursion schemes
- A formalized general theory of syntax with bindings: extended version
- Confluence of the coinductive \(\lambda\)-calculus
- Why Would You Trust B?
- \(\mathrm{HO}\pi\) in Coq
- de Bruijn Indices for Metaterms
- Variable binding and substitution for (nameless) dummies
- Polarised subtyping for sized types
- Some Wellfounded Trees in UniMath
- Modules over monads and initial semantics
- Towards an induction principle for nested data types
- Map fusion for nested datatypes in intensional type theory
- A principled approach to programming with nested types in Haskell
- Strongly typed term representations in Coq
- A unified treatment of syntax with binders
- A proof of the substitution lemma in de Bruijn's notation
- Substitution for non-wellfounded syntax with binders through monoidal categories
- Implementing a normalizer using sized heterogeneous types
- Call-by-value and call-by-name: a simple proof of a classic theorem
- Nested abstract syntax in Coq
- Structured monads for generic first-order syntax metatheory
- Rensets and renaming-based recursion for syntax with bindings extended version
- Nested term graphs (work in progress)
- Iteration and coiteration schemes for higher-order and nested datatypes
- Heterogeneous substitution systems revisited
- 2-Dimensional Directed Type Theory
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Deep induction: induction rules for (truly) nested types
- Proof Pearl: De Bruijn Terms Really Do Work
- Generating bijections between HOAS and the natural numbers
This page was built for publication: de Bruijn notation as a nested datatype
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4256148)
