arXiv subjects

Luigi Liquori

Publications and source records attributed to Luigi Liquori.

7 recordsLinked to original sources

arXiv2026

Determinacy with Priorities up to Clocks

In Milner's seminal book on communication and concurrency introducing CCS, a process algebra inherently non-deterministic, chapter 11 was completely devoted to introduce the notion of determinacy and confluence in order to identify a subcalculus of CCS in which all definable agents are confluent. At the same time, or shortly later, determinate semantics were given for programming languages that reconcile concurrency and determinacy, such as Esterel by Berry and Gonthier, or SL by Boussinot and de Simone. These dedicated semantics do not easily map to Milner's confluence theory for CCS, which is unable to express causality and shared memory multi-threading with reaction to absence in a compositional way. We present an extension of CCS with priority-guarded actions and clocks, and we exploit the added expressiveness to enrich Milner's original notion of confluence by the new concept of coherence which permits us to encode, in a compositional fashion, synchronous programming languages such as Esterel.

cs.PL↗

arXiv2025

Strong Priority and Determinacy in Timed CCS

Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of "coherent" processes a confluence property for constructive reductions. We show that under some restrictions, called "pivotability", coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.

cs.PL↗

arXiv2020

A Type Checker for a Logical Framework with Union and Intersection Types

We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Xi of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi's Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow the user to write Delta-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard's parametric one.

cs.LO↗

arXiv2019

The Delta-calculus: syntax and types

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Salle', the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection type systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems a` la Curry and the corresponding intersection type systems a` la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.

cs.LO↗

arXiv2018

The Delta-framework

We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF-Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF-Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.

cs.LO↗

arXiv2017

$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,σ}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,σ}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,σ}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $λ$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.

cs.LO↗

arXiv2015

Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks

We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for gluing together diverse Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.

cs.LO↗