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 Plus annual

Presents the access of premium content as premium feature

Premium Content

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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

There are several ways to formally represent families of data, such as lambdaterms, in a type theory such as the dependent type theory of Coq. Mathematicalrepresentations are very compact ones and usually rely on the use of dependenttypes, but they tend to be difficult to handle in practice. On the contrary,implementations based on a larger (and simpler) data structure combined with arestriction property are much easier to deal with.  In this work, we study several families related to lambda terms, among whichMotzkin trees, seen as lambda term skeletons, closable Motzkin trees,corresponding to closed lambda terms, and a parameterized family of open lambdaterms. For each of these families, we define two different representations,show that they are isomorphic and provide tools to switch from onerepresentation to another. All these datatypes and their associatedtransformations are implemented in the Coq proof assistant. Furthermore weimplement random generators for each representation, using the QuickChickplugin.

Pragmatic isomorphism proofs between Coq representations: application to lambda-term families