Quotients of Bounded Natural Functors

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,...

Full description

Bibliographic Details
Main Authors: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2022-02-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/7354/pdf