Kleene star, subexponentials without contraction, and infinite computations

We present an extension of intuitionistic non-commutative linear logic with Kleene star and subexponentials which allow permutation and/or weakening, but not contraction.Subexponentials which allow contraction are useful for specifying correct terminating of computing systems (e.g., Turing machines).Dually, we show that Kleene star axiomatized by an omega-rule allows modelling innite (never terminating) behaviour.Our system belongs to the Π 0 1 complexity class.Actually, it is Buszkowski (2007).We show Π 0 1 -hardness of the unidirectional fragment of this logic with two subexponentials and Kleene star (this result does not follow from Buszkowski's construction).The omega-rule axiomatization can be equivalently reformulated as calculus with non-well-founded proofs (Das & Pous, 2018).We also consider the fragment of this calculus with circular proofs.This fragment is capable of modelling looping of a Turing machine, but, interestingly enough, some non-cyclic computations can also be captured by this circular fragment.