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

We give a categorical semantics for a call-by-value linear lambda calculus.Such a lambda calculus was used by Selinger and Valiron as the backbone of afunctional programming language for quantum computation. One feature of thislambda calculus is its linear type system, which includes a duplicabilityoperator "!" as in linear logic. Another main feature is its call-by-valuereduction strategy, together with a side-effect to model probabilisticmeasurements. The "!" operator gives rise to a comonad, as in the linear logicmodels of Seely, Bierman, and Benton. The side-effects give rise to a monad, asin Moggi's computational lambda calculus. It is this combination of a monad anda comonad that makes the present paper interesting. We show that ourcategorical semantics is sound and complete.

A linear-non-linear model for a computational call-by-value lambda calculus (extended abstract)