de Bruijn notation as a nested datatype
From MaRDI portal
Publication:4256148
DOI10.1017/S0956796899003366zbMath0926.68025MaRDI QIDQ4256148
Richard S. Bird, Ross Paterson
Publication date: 28 June 1999
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items (31)
A unified treatment of syntax with binders ⋮ Confluence of the coinductive \(\lambda\)-calculus ⋮ A principled approach to programming with nested types in Haskell ⋮ Explicit substitutions and higher-order syntax ⋮ Strongly typed term representations in Coq ⋮ Why Would You Trust B? ⋮ Rensets and renaming-based recursion for syntax with bindings extended version ⋮ Map fusion for nested datatypes in intensional type theory ⋮ Variable binding and substitution for (nameless) dummies ⋮ Fantastic morphisms and where to find them. A guide to recursion schemes ⋮ Variable binding and substitution for (nameless) dummies ⋮ Towards an induction principle for nested data types ⋮ Nested abstract syntax in Coq ⋮ Deep induction: induction rules for (truly) nested types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Polarised subtyping for sized types ⋮ A formalized general theory of syntax with bindings: extended version ⋮ Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic ⋮ Modules over monads and initial semantics ⋮ 2-Dimensional Directed Type Theory ⋮ Substitution in non-wellfounded syntax with variable binding ⋮ Iteration and coiteration schemes for higher-order and nested datatypes ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Some Wellfounded Trees in UniMath ⋮ Implementing a normalizer using sized heterogeneous types ⋮ An induction principle for nested datatypes in intensional type theory ⋮ From signatures to monads in \textsf{UniMath} ⋮ Heterogeneous Substitution Systems Revisited ⋮ Rensets and renaming-based recursion for syntax with bindings ⋮ A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
This page was built for publication: de Bruijn notation as a nested datatype
