An induction principle for nested datatypes in intensional type theory (Q3638923): Difference between revisions

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Induction-recursion and initial algebras.
@@ Property / cites work: Induction-recursion and initial algebras. / rank @@
+Normal rank
@@ Property / cites work @@
+Mathematics of program construction. 4th international conference, MPC '98, Marstrand, Sweden, June 15--17, 1998. Proceedings
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Substitution: A formal methods case study using monads and transformations
+Normal rank
@@ Property / cites work @@
+Generalised folds for nested datatypes
@@ Property / cites work: Generalised folds for nested datatypes / 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 @@
+Iteration and coiteration schemes for higher-order and nested datatypes
+Normal rank
@@ Property / cites work @@
+Disciplined, efficient, generalised folds for nested datatypes
+Normal rank
@@ Property / cites work @@
+Least and greatest fixed points in intuitionistic natural deduction
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:3638923