Polynomial time in untyped elementary linear logic

Olivier Laurent (1, 2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 PLUME - Preuves et Langages

We show how to represent polynomial time computation in an untyped version of proof-nets for elementary linear logic. This follows previous work by P. Baillot but which was developed in a typed and affine setting. We describe how these two properties can be adapted.

Mots clés: Strong Normalization; Implicit Computational Complexity; Polynomial Time Computation; Elementary Linear Logic; Proof Nets

Domaines: Logique en informatique [cs.LO]; Logique [math.LO]

Olivier Laurent. Polynomial time in untyped elementary linear logic. Theoretical Computer Science, 2020, 813, pp.117-142. ⟨10.1016/j.tcs.2019.10.002⟩. ⟨hal-02333452⟩