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

We apply the Agda-flat proof assistant (Vezzosi, 2019) to computational semantics. Computational semantics in Agda-flat is distinguished from the approach based on Coq (Chatzikyriakidis and Luo, 2014) in that it allows an implementation of the classical, intensional semantic analyses of Montague (1973). That is, it synthesizes the modern dependent type theory and Montague intensional logic traditions in the computational semantics setting. To demonstrate this, we show how to replicate Montague’s analyses in the type theory of Zwanziger (2018), which closely corresponds to the Agda-flat system. Accompanying code type-checks these analyses in Agdaflat.

Dependently-Typed Montague Semantics in the Proof Assistant Agda-flat