- Conference Paper
The functorial structure of type constructors is the foundation for many definition and proof principles in higher-order logic (HOL). For example, inductive and coinductive datatypes can be built modularly from bounded natural functors (BNFs), a class of well-behaved type constructors. Composition, fixpoints, and—under certain conditions—subtypes are known to preserve the BNF structure. In this paper, we tackle the preservation question for quotients, the last important principle for introducing new types in HOL. We identify sufficient conditions under which a quotient inherits the BNF structure from its underlying type. We extend the Isabelle proof assistant with a command that automates the registration of a quotient type as a BNF by lifting the underlying type’s BNF structure. We demonstrate the command’s usefulness through several case studies. Show more
Book titleAutomated Reasoning
Journal / seriesLecture Notes in Computer Science
Pages / Article No.
Organisational unit03634 - Basin, David / Basin, David
NotesDue to the Coronavirus (COVID-19) the conference was conducted virtually.
MoreShow all metadata