An induction principle for nested datatypes in intensional type theory

DOI10.1017/S095679680900731XzbMath1191.68164MaRDI QIDQ3638923

Ralph Matthes

Publication date: 28 October 2009

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

true nesting

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

68P05: Data structures

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

• Coq

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