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

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Affine type systems are substructural type systems where copying ofinformation is restricted, but discarding of information is permissible at alltypes. Such type systems are well-suited for describing quantum programminglanguages, because copying of quantum information violates the laws of quantummechanics. In this paper, we consider a first-order affine type system withinductive data types and present a novel categorical semantics for it. The mostchallenging aspect of this interpretation comes from the requirement toconstruct appropriate discarding maps for our data types which might be definedby mutual/nested recursion. We show how to achieve this for all types by takingmodels of a first-order linear type system whose atomic types are discardableand then presenting an additional affine interpretation of types within theslice category of the model with the tensor unit. We present some concretecategorical models for the language ranging from classical to quantum. Finally,we discuss potential ways of dualising and extending our methods and using themfor interpreting coalgebraic and lazy data types.

Semantics for first-order affine inductive data types via slice categories