Hal will be stopped for maintenance from friday on june 10 at 4pm until monday june 13 at 9am. More information
Skip to Main content Skip to Navigation

A semantic measure of the execution time in Linear Logic

Abstract : We give a semantic account of the execution time (i.e. the number of cut-elimination steps leading to the normal form) of an untyped MELL (proof-)net. We first prove that: 1) a net is head-normalizable (i.e. normalizable at depth 0) if and only if its interpretation in the multiset based relational semantics is not empty and 2) a net is normalizable if and only if its exhaustive interpretation (a suitable restriction of its interpretation) is not empty. We then define a size on every experiment of a net, and we precisely relate the number of cut-elimination steps of every stratified reduction sequence to the size of a particular experiment. Finally, we give a semantic measure of execution time: we prove that we can compute the number of cut-elimination steps leading to a cut free normal form of the net obtained by connecting two cut free nets by means of a cut link, from the interpretations of the two cut free nets. These results are inspired by similar ones obtained by the first author for the (untyped) lambda-calculus.
Document type :
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, February 4, 2008 - 5:58:31 PM
Last modification on : Friday, February 4, 2022 - 3:25:23 AM
Long-term archiving on: : Friday, September 24, 2010 - 11:07:46 AM


Files produced by the author(s)


  • HAL Id : inria-00206099, version 4


Daniel de Carvalho, Michele Pagani, Lorenzo Tortora de Falco. A semantic measure of the execution time in Linear Logic. [Research Report] RR-6441, INRIA. 2008, pp.48. ⟨inria-00206099v4⟩



Record views


Files downloads