arXiv subjects

Elaine Pimentel

Publications and source records attributed to Elaine Pimentel.

26 records · Page 2Linked to original sources

arXiv2019

The ILLTP Library for Intuitionistic Linear Logic

Benchmarking automated theorem proving (ATP) systems using standardized problem sets is a well-established method for measuring their performance. However, the availability of such libraries for non-classical logics is very limited. In this work we propose a library for benchmarking Girard's (propositional) intuitionistic linear logic. For a quick bootstrapping of the collection of problems, and for discussing the selection of relevant problems and understanding their meaning as linear logic theorems, we use translations of the collection of Kleene's intuitionistic theorems in the traditional monograph "Introduction to Metamathematics". We analyze four different translations of intuitionistic logic into linear logic and compare their proofs using a linear logic based prover with focusing. In order to enhance the set of problems in our library, we apply the three provability-preserving translations to the propositional benchmarks in the ILTP Library. Finally, we generate a comprehensive set of reachability problems for Petri nets and encode such problems as linear logic sequents, thus enlarging our collection of problems.

cs.LO↗

arXiv2018

Proof systems: from nestings to sequents and back

In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a general algorithm for transforming a class of nested systems into sequent calculus systems, passing through linear nested systems. Moreover, we show a semantical characterisation of intuitionistic, multi-modal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.

cs.LO↗

arXiv2018

A Concurrent Constraint Programming Interpretation of Access Permissions

A recent trend in object oriented (OO) programming languages is the use of Access Permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as Linear Concurrent Constraint Programs (lcc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in lcc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of lcc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the lcc model, observing the flow of APs and quickly finding inconsistencies of the APs vis-a-vis the implementation. The latter is an automatic theorem prover based on ILL. This paper is under consideration for publication in Theory and Practice of Logic Programming (TPLP).

cs.LO↗

arXiv2017

Modularisation of Sequent Calculi for Normal and Non-normal Modalities

In this work we explore the connections between (linear) nested sequent calculi and ordinary sequent calculi for normal and non-normal modal logics. By proposing local versions to ordinary sequent rules we obtain linear nested sequent calculi for a number of logics, including to our knowledge the first nested sequent calculi for a large class of simply dependent multimodal logics, and for many standard non-normal modal logics. The resulting systems are modular and have separate left and right introduction rules for the modalities, which makes them amenable to specification as bipole clauses. While this granulation of the sequent rules introduces more choices for proof search, we show how linear nested sequent calculi can be restricted to blocked derivations, which directly correspond to ordinary sequent derivations.

cs.LO↗

arXiv2016

Hybrid and Subexponential Linear Logics Technical Report

HyLL (Hybrid Linear Logic) and SELL (Subexponential Linear Logic) are logical frameworks that have been extensively used for specifying systems that exhibit modalities such as temporal or spatial ones. Both frameworks have linear logic (LL) as a common ground and they admit (cut-free) complete focused proof systems. The difference between the two logics relies on the way modalities are handled. In HyLL, truth judgments are labelled by worlds and hybrid connectives relate worlds with formulas. In SELL, the linear logic exponentials (!, ?) are decorated with labels representing locations, and an ordering on such labels defines the provability relation among resources in those locations. It is well known that SELL, as a logical framework, is strictly more expressive than LL. However, so far, it was not clear whether HyLL is more expressive than LL and/or SELL. In this paper, we show an encoding of the HyLL's logical rules into LL with the highest level of adequacy, hence showing that HyLL is as expressive as LL. We also propose an encoding of HyLL into SELL $\doublecup$ (SELL plus quantification over locations) that gives better insights about the meaning of worlds in HyLL. We conclude our expressiveness study by showing that previous attempts of encoding Computational Tree Logic (CTL) operators into HyLL cannot be extended to consider the whole set of temporal connectives. We show that a system of LL with fixed points is indeed needed to faithfully encode the behavior of such temporal operators.

cs.LO↗

arXiv2014

A Proof Theoretic Study of Soft Concurrent Constraint Programming

Concurrent Constraint Programming (CCP) is a simple and powerful model for concurrency where agents interact by telling and asking constraints. Since their inception, CCP-languages have been designed for having a strong connection to logic. In fact, the underlying constraint system can be built from a suitable fragment of intuitionistic (linear) logic --ILL-- and processes can be interpreted as formulas in ILL. Constraints as ILL formulas fail to represent accurately situations where "preferences" (called soft constraints) such as probabilities, uncertainty or fuzziness are present. In order to circumvent this problem, c-semirings have been proposed as algebraic structures for defining constraint systems where agents are allowed to tell and ask soft constraints. Nevertheless, in this case, the tight connection to logic and proof theory is lost. In this work, we give a proof theoretical interpretation to soft constraints: they can be defined as formulas in a suitable fragment of ILL with subexponentials (SELL) where subexponentials, ordered in a c-semiring structure, are interpreted as preferences. We hence achieve two goals: (1) obtain a CCP language where agents can tell and ask soft constraints and (2) prove that the language in (1) has a strong connection with logic. Hence we keep a declarative reading of processes as formulas while providing a logical framework for soft-CCP based systems. An interesting side effect of (1) is that one is also able to handle probabilities (and other modalities) in SELL, by restricting the use of the promotion rule for non-idempotent c-semirings.This finer way of controlling subexponentials allows for considering more interesting spaces and restrictions, and it opens the possibility of specifying more challenging computational systems.

cs.LO↗

arXiv2012

Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications

This volume contains the proceedings of the Sixth Workshop on Logical and Semantic Frameworks with Applications (LSFA 2011). The workshop will be hold in Belo Horizonte, on August 27th 2011. Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for formal specification of systems and programming languages, supporting tool development and reasoning. The objective of this one-day workshop is to put together theoreticians and practitioners to promote new techniques and results, from the theoretical side, and feedback on the implementation and the use of such techniques and results, from the practical side.

cs.LO↗

arXiv2011

Proceedings Fifth Workshop on Intersection Types and Related Systems

This volume contains the proceedings of the Fifth International Workshop on Intersection Types and Related Systems (ITRS 2010). The workshop was held in Edinburgh, Scotland, on July 9th 2010, as part of FLoC 2010 and affiliated with LICS 2010. The ITRS workshop series aim at bringing together researchers working on both the theory and practical applications of systems based on intersection types and related approaches (e.g., union types, refinement types, behavioral types).

cs.LO↗