Author name cluster

Andrea Masini

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.

6 papers

2 author rows

TCS Journal 2010 Journal Article

Quantum implicit computational complexity

Ugo Dal Lago
Andrea Masini
Margherita Zorzi

We introduce a quantum lambda calculus inspired by Lafont’s Soft Linear Logic and capturing the polynomial quantum complexity classes EQP, BQP and ZQP. The calculus is based on the “classical control and quantum data” paradigm. This is the first example of a formal system capturing quantum complexity classes in the spirit of implicit computational complexity — it is machine-free and no explicit bound (e. g. , polynomials) appears in its syntax.

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

Parsing MELL proof nets

Stefano Guerrini
Andrea Masini

We propose a rewriting system for parsing full multiplicative and exponential proof structures. The recognizing grammar defined by such a rewriting system (confluent and strongly normalizing) gives a correctness criterion that we show equivalent to the Danos–Regnier one.

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

CSL Conference 1989 Conference Paper

A temporal Logic Approach to Specify and to Prove Properties of Finite State Concurrent Systems

Marco Danelutto
Andrea Masini

Abstract We present a formalism to handle finite state concurrent systems in a mechanical way. In such a formalism we can axiomatically define concurrent systems by means of a branching time language. We show that, starting from the axiomatic description of a concurrent system, we can obtain automatically a finite Kripke model H such that theorem proving is reduced to model checking with respect to H. By means of such a formal procedure, we can model a large class of concurrent systems including Petri nets, CSP, Interaction Systems and so on. A tool has been implemented to produce a Kripke model from an axiomatical description of a concurrent system and to perform model checking on it.

Details