LAUSR

Abstract The Sweedler semantics of intuitionistic differential linear logic takes values in the category of vector spaces, using the cofree cocommutative coalgebra to interpret the exponential and primitive elements to interpret the differential structure. In this paper, we explicitly compute the denotations under this semantics of an interesting class of proofs in linear logic, introduced by Girard: the encodings of step functions of Turing machines. Along the way we prove some useful technical results about linear independence of denotations of Church numerals and binary integers.