Linear Additives

• We introduce LAM, a subsystem of IMALL2 with restricted additive rules able to manage duplication linearly, called linear additive rules. LAM is presented as the type assignment system for a calculus endowed with copy constructors, which deal with substitution in a linear fashion. As opposed to the standard additive rules, the linear additive rules do not affect the complexity of term reduction: typable terms of LAM enjoy linear strong normalization. Moreover, a mildly weakened version of cut-elimination for this system is proven which takes a cubic number of steps. Finally, we define a sound translation from LAM’s proofs into IMLL2’s linear lambda terms, and we study its complexity.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap (Datateknik) (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences (hsv//eng)

Nyckelord

Second-Order Linear Logic

Additives

Type Assignment

Cut-elimination (cost)

Publikations- och innehållstyp

ref (ämneskategori)

art (ämneskategori)