In CDLE, a pure Curry-style type theory, it is possible to generically derive induction for lambda-encoded data whose types are least fixed points of functors. From this comes fruitful research into the design-space for datatype systems: Firsov et al. build upon this de... View more
Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. Electronic Proceedings in Theoretical Computer Science 43 (Dec 2010), 14-28. https://doi.org/10.4204/eptcs.43.2
Ki Yung Ahn. 2014. The Nax Language: Unifying Functional Programming and Logical Reasoning in a Language based on Mendler-style Recursion Schemes and Term-indexed Types. (2014).
Ki Yung Ahn and Tim Sheard. 2011. A Hierarchy of Mendler Style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences. SIGPLAN Not. 46, 9 (Sept. 2011), 234-246. https://doi.org/10.1145/2034574.2034807
Gilles Barthe, Maria Joao Frade, Eduardo Giménez, Luis Pinto, and Tarmo Uustalu. 2004. Type-based termination of recursive definitions. Mathematical structures in computer science 14, 1 (2004), 97-141.
Frédéric Blanqui. 2005. Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae 65, 1-2 (2005), 61-86.
Corrado Böhm. 1968. Alcune proprieta delle forme β -η-normali nel λ-K-calcolo. Pubblicazioni dell'Istituto per le Applicazioni del Calcolo 696 (1968), 19.
Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 5 (2013), 552-593.
R. M. Burstall, D. B. MacQueen, and D. T. Sannella. 1980. Hope: An Experimental Applicative Language.
Thierry Coquand. 1992a. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks, Vol. 92. 66-79.
Thierry Coquand. 1992b. Pattern matching with dependent types. In Informal proceedings of Logical Frameworks, Vol. 92. 66-79.