Search

It is proved that the standard sequent calculus proof system of linear logic is equivalent to a natural deduction style proof system. The natural deduction system is used to investigate the pragmatic problems of type inference and type safety for a linear lambda calculus. Although terms do not have a single most-general type (for either the standard sequent presentation or the natural deduction formulation), there is a set of most-general types that may be computed using unification. The natural deduction system also facilitates the proof that the type of an expression is preserved by any evaluation step. An execution model and implementation is described, using a variant of the three-instruction machine. A novel feature of the implementation is that garbage-collected nonlinear memory is distinguished from linear memory, which does not require garbage collection and for which it is possible to do secure update in place. >

We propose a new practical technique for the distributed execution-driven simulation of parallel computers. Our simulation methodology allows complete verbalization of the design at all levels and achieves good performance by preserving and exploiting the parallelism of the parallel program being simulated. With our technique it is possible to decouple the simulation of the execution of a parallel application from the estimation of the virtual execution time in which such execution is carried out. Our technique uses minimal overhead to maintain coherent distributed event causality relations by making it possible for the simulated executions to reflect the intrinsic uncertainties of parallel applications being simulated. We include a detailed description of our methodology, explain how to apply our ideas to parallelize an existing execution-driven sequential simulator under quite general assumptions, discuss the trade-offs of our methodology, and give preliminary performance measurements of a distributed simulator that uses our technique.

We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first-order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability. >