Cargando…

Deep Induction: Induction Rules for (Truly) Nested Types

This paper introduces deep induction, and shows that it is the notion of induction most appropriate to nested types and other data types defined over, or mutually recursively with, (other) such types. Standard induction rules induct over only the top-level structure of data, leaving any data interna...

Descripción completa

Detalles Bibliográficos
Autores principales: Johann, Patricia, Polonsky, Andrew
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7788624/
http://dx.doi.org/10.1007/978-3-030-45231-5_18