An induction principle for nested datatypes in intensional type theory
From MaRDI portal
Publication:3638923
DOI10.1017/S095679680900731XzbMath1191.68164MaRDI QIDQ3638923
Publication date: 28 October 2009
Published in: Journal of Functional Programming (Search for Journal in Brave)
Related Items
Map fusion for nested datatypes in intensional type theory, Nested abstract syntax in Coq, Deep induction: induction rules for (truly) nested types, Coalgebraic Reasoning in Coq: Bisimulation and the λ-Coiteration Scheme
Uses Software
Cites Work
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Substitution: A formal methods case study using monads and transformations
- Mathematics of program construction. 4th international conference, MPC '98, Marstrand, Sweden, June 15--17, 1998. Proceedings
- Induction-recursion and initial algebras.
- Iteration and coiteration schemes for higher-order and nested datatypes
- Disciplined, efficient, generalised folds for nested datatypes
- Generalised folds for nested datatypes
- de Bruijn notation as a nested datatype
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Least and greatest fixed points in intuitionistic natural deduction