Author name cluster

Simone Martini

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

TCS Journal 2008 Journal Article

The weak lambda calculus as a reasonable machine

Ugo Dal Lago
Simone Martini

We define a new cost model for the call-by-value lambda-calculus satisfying the invariance thesis. That is, under the proposed cost model, Turing machines and the call-by-value lambda-calculus can simulate each other within a polynomial time overhead. The model only relies on combinatorial properties of the usual beta-reduction, without any reference to a specific machine or evaluator. In particular, the cost of a single beta reduction is proportional to the difference between the size of the redex and the size of the reduct. In this way, the total cost of normalizing a lambda term will take into account the size of all intermediate results (as well as the number of steps to normal form).

Details DOI

I&C Journal 2004 Journal Article

(Optimal) duplication is not elementary recursive

Andrea Asperti
Paolo Coppola
Simone Martini

In 1998 Asperti and Mairson proved that the cost of reducing a lambda-term using an optimal lambda-reducer (a la Lévy) cannot be bound by any elementary function in the number of shared-beta steps. We prove in this paper that an analogous result holds for Lamping’s abstract algorithm. That is, there is no elementary function in the number of shared beta steps bounding the number of duplication steps of the optimal reducer. This theorem vindicates the oracle of Lamping’s algorithm as the culprit for the negative result of Asperti and Mairson. The result is obtained using as a technical tool Elementary Affine Logic.

Details DOI

TCS Journal 2004 Journal Article

Phase semantics and decidability of elementary affine logic

Ugo Dal Lago
Simone Martini

Light, elementary and soft linear logics are formal systems derived from Linear Logic, enjoying remarkable normalization properties. In this paper, we prove decidability of Elementary Affine Logic, EAL. The result is obtained by semantical means, first defining a class of phase models for EAL and then proving soundness and (strong) completeness, following Okada's technique. Phase models for Light Affine Logic and Soft Linear Logic are also defined and shown complete.

Details DOI

TCS Journal 2003 Journal Article

Coherence for sharing proof-nets

Stefano Guerrini
Simone Martini
Andrea Masini

Sharing graphs are an implementation of linear logic proof-nets in which a redex is never duplicated. In their usual formulation, sharing graphs present a problem of coherence: if the proof-net N reduces by standard cut-elimination to N′, then, by reducing the sharing graph of N we do not obtain the sharing graph of N′. We solve this problem by changing the way the information is coded into sharing graphs and introducing a new reduction rule (absorption). The rewriting system is confluent and terminating. The proof exploits an algebraic semantics for sharing graphs.

Details DOI

TCS Journal 2001 Journal Article

Proof nets, garbage, and computations

Stefano Guerrini
Simone Martini
Andrea Masini

We study the problem of local and asynchronous computation in the context of multiplicative exponential linear logic (MELL) proof nets. The main novelty is in a complete set of rewriting rules for cut-elimination in presence of weakening (which requires garbage collection). The proposed reduction system is strongly normalizing and confluent. The proofs are based on pure syntactical reasonings.

Details DOI

TCS Journal 1997 Journal Article

Experiments in linear natural deduction

Simone Martini
Andrea Masini

We investigate several fragments of multiplicative linear logic, in a natural deduction setting and with the aim of a better understanding of the par connective. We study, first, a pre-tensorial calculus, which is strengthened then in the standard tensorial fragment. The addition of a further pre-tensorial connective yields (a natural deduction version of) Full Intuitionistic Linear Logic. A further strengthening of the rules leads to the full classical multiplicative logic. Some proof-theoretical properties of the systems are investigated.

Details DOI

I&C Journal 1992 Journal Article

Categorical models of polymorphism

Andrea Asperti
Simone Martini

We present and discuss the relations between two classes of categorical models of the second order (or polymorphic) lambda-calculus, namely those based on internal categories (internal models) and those based on indexed categories (external models). We start, in Part I, with a detailed introduction to internal categories and their relations to indexed categories; the presentation is by means of equations between arrows in an ambient category with finite limits. In Part II we recall the definition of the two classes of models and we present the “externalization process” that given an internal model yields an external model. We show how one can go back in a straightforward way, and that, by making a full round trip (from an internal model to an internal model via an external one, or vice-versa), one does obtain equivalent models. Part III discusses three major examples of models (provable retractions inside a PER model, PER inside ω-Set, PL-categories inside their Grothendieck completions). The appendix contains an account of internal adjunctions and internal CCCs.

Details DOI