24 citations · 52 across the 9 of their papers we have counts for
9 papers
From 2-sequents and Linear Nested Sequents to Natural Deduction for Normal Modal Logics
Simone Martini, Andrea Masini, Margherita Zorzi
We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal syst…
Several types of types in programming languages
Simone Martini
Types are an important part of any modern programming language, but we often forget that the concept of type we understand nowadays is not the same it was perceived in the sixties.…
Towards A Theory Of Quantum Computability
Stefano Guerrini, Simone Martini, Andrea Masini
We propose a definition of quantum computable functions as mappings between superpositions of natural numbers to probability distributions of natural numbers. Each function is obta…
On Constructor Rewrite Systems and the Lambda Calculus
Ugo Dal Lago, Simone Martini
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduct…
Light Logics and Higher-Order Processes
Ugo Dal Lago, Simone Martini, Davide Sangiorgi
We show that the techniques for resource control that have been developed in the so-called "light logics" can be fruitfully applied also to process algebras. In particular, we pres…
General Ramified Recurrence is Sound for Polynomial Time
Ugo Dal Lago, Simone Martini, Margherita Zorzi
Leivant's ramified recurrence is one of the earliest examples of an implicit characterization of the polytime functions as a subalgebra of the primitive recursive functions. Leivan…
On Constructor Rewrite Systems and the Lambda-Calculus (Long Version)
Ugo Dal Lago, Simone Martini
We prove that orthogonal constructor term rewrite systems and lambda-calculus with weak (i.e., no reduction is allowed under the scope of a lambda-abstraction) call-by-value reduct…
An Invariant Cost Model for the Lambda Calculus
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 lam…
Optimizing Optimal Reduction: A Type Inference Algorithm for Elementary Affine Logic
Paolo Coppola, Simone Martini
We present a type inference algorithm for lambda-terms in Elementary Affine Logic using linear constraints. We prove that the algorithm is correct and complete.