### Current browse context:

cs.LO

### Change to browse by:

### References & Citations

# Computer Science > Logic in Computer Science

# Title: Semimodules and the (syntactically-)linear lambda calculus

(Submitted on 4 May 2022)

Abstract: In a recent paper, the $\mathcal L^{\mathcal S}$-calculus has been defined. It is a proof-language for a significant fragment of intuitionistic linear logic. Its main feature is that the linearity properties can be expressed in its syntax, since it has interstitial logical rules whose proof-terms are a sum and a multiplication by scalar.

The calculus is parametrized on the structure $\mathcal S$. This structure was originally identified with the field of complex numbers, since the calculus is designed as a quantum lambda calculus. However, in this paper we show that a semiring is enough, and we provide a categorical semantics for this calculus in the category of cancellative semimodules over the given semiring. We prove the semantics to be sound and adequate.

Link back to: arXiv, form interface, contact.