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/

Zendy Plus

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

Zendy Tools

Zendy Open

Type checking algorithms and theorem provers rely on unification algorithms.In presence of type families or higher-order logic, higher-order(pre)unification (HOU) is required. Many HOU algorithms are expressed in termsof $\lambda$-calculus and require encodings, such as higher-order abstractsyntax, which are sometimes not comfortable to work with for languageimplementors. To facilitate implementations of languages, proof assistants, andtheorem provers, we propose a novel approach based on the second-order abstractsyntax of Fiore, data types \`a la carte of Swierstra, and intrinsic scoping ofBird and Patterson. With our approach, an object language is generated freelyfrom a given bifunctor. Then, given an evaluation function and making a fewreasonable assumptions on it, we derive a higher-order preunification procedureon terms in the object language. More precisely, we apply a variant of$E$-unification for second-order syntax. Finally, we briefly demonstrate anapplication of this technique to implement type checking (with type inference)for Martin-L\"of Type Theory, a dependent type theory.

Free Monads, Intrinsic Scoping, and Higher-Order Preunification