English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Nested datatypes have been widely studied in the past 25 years, boththeoretically using category theory, and practically in programming languagessuch as Haskell. They consist in recursive polymorphic datatypes where the typeparameter changes throughout the recursion. They have a variety of applicationssuch as modelling memory or modelling constraints over regular datatypeswithout relying on dependent types. In this work, we focus on a specific subsetof nested datatypes which we call Linked Nested DataTypes (LNDT). We show thatsome usual datatypes such has List and Maybe, as well as some well-known nesteddatatypes such as Nest and even Bush can be built as various instances of LNDT.We proceed by presenting LibNDT, a library, developed both in Agda and Coq,which focuses on the set of constructs that can be spread directly from theparameter on which a LNDT is built, to the LNDT itself. These spreadableelements are of two kinds, functions, such as folds and map, and properties,such as the congruence of map or the satisfaction of a given predicate for atleast one, or all, elements of the structure. We make use of the dependent typesystem of both Coq and Agda to model the latter. This paper ends with adiscussion about various interesting topics that were raised throughout ourdevelopment such as the issue of termination, the comparison of our tools andthe proof effort required to extend LibNDT with additional elements.

LibNDT: Towards a Formal Library on Spreadable Properties over Linked Nested Datatypes