Nested abstract syntax in Coq (Q1945918): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PoplMark
@@ Property / describes a project that uses: PoplMark / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-010-9207-9
+Normal rank
@@ Property / OpenAlex ID @@
+W2147567862
@@ Property / OpenAlex ID: W2147567862 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4945244
@@ Property / cites work: Q4945244 / rank @@
+Normal rank
@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+Engineering formal metatheory
@@ Property / cites work: Engineering formal metatheory / rank @@
+Normal rank
@@ Property / cites work @@
+de Bruijn notation as a nested datatype
@@ Property / cites work: de Bruijn notation as a nested datatype / rank @@
+Normal rank
@@ Property / cites work @@
+A new approach to abstract syntax with variable binding
+Normal rank
@@ Property / cites work @@
+Modules over Monads and Linearity
@@ Property / cites work: Modules over Monads and Linearity / rank @@
+Normal rank
@@ Property / cites work @@
+Modules over monads and initial semantics
@@ Property / cites work: Modules over monads and initial semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Q4535076
@@ Property / cites work: Q4535076 / rank @@
+Normal rank
@@ Property / cites work @@
+Towards a mechanized metatheory of standard ML
@@ Property / cites work: Towards a mechanized metatheory of standard ML / rank @@
+Normal rank
@@ Property / cites work @@
+Nested Datatypes with Generalized Mendler Iteration: Map Fusion and the Example of the Representation of Untyped Lambda Calculus with Explicit Flattening
+Normal rank
@@ Property / cites work @@
+Recursion on Nested Datatypes in Dependent Type Theory
+Normal rank
@@ Property / cites work @@
+An induction principle for nested datatypes in intensional type theory
+Normal rank