[1] 
Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze.
A realizability interpretation for intersection and union types.
In Programming Languages and Systems  14th Asian Symposium,
APLAS 2016, pages 187205, October 2016.
[ bib 
DOI 
http 
.pdf ]
Prooffunctional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of firstclass objects. This is in contrast to classical truthfunctional connectives where the meaning of a compound formula is dependent only on the truth value of its subformulas. In this paper we present a typed lambda calculus, enriched with products, coproducts, and a related prooffunctional logic. This calculus, directly derived from a typed calculus previously defined by two of the current authors, has been proved isomorphic to the wellknown BarbaneraDezaniCiancaglinide'Liguoro type assignment system. We present a logic L featuring two prooffunctional connectives, namely strong conjunction and strong disjunction. We prove the typed calculus to be isomorphic to the logic L and we give a realizability semantics using Mints' realizers and a completeness theorem. A prototype implementation is also described.

[2] 
Luigi Liquori and Claude Stolze.
A Decidable Subtyping Logic for Intersection and Union Types (full
version).
Research report, Inria, March 2017.
[ bib 
http 
.pdf ]
Prooffunctional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of firstclass objects. This is in contrast to classical truthfunctional connectives where the meaning of a compound formula is dependent only on the truth value of its subformulas. We present a prooffunctional logic and we give a semantics using Mints' realizers accounting for intersection types, union types, and subtyping. The semantics interprets the type ω as the set universe, the > type as a function space, the /\ and V types as set intersection and set union, respectively, and the subtype relation as a subset operator. Using the proofastypes and termsaspropositions paradigms, we extend the typed calculus previously defined by the authors with a decidable subtyping relation and we show this calculus to be isomorphic to the BarbaneraDezaniCiancaglinide'Liguoro type assignment system. A subtyping algorithm is presented and proved to be sound and complete. Hindley gave a subtyping algorithm for intersection types but, as far as we know, there is no system in the literature also including union types.

[3] 
Luigi Liquori and Claude Stolze.
A Decidable Subtyping Logic for Intersection and Union Types.
In 2nd International Conference on Topics in Theoretical
Computer Science, TTCS 2017, pages 7490, September 2017.
[ bib 
DOI 
http 
.pdf ]
Using CurryHoward isomorphism, we extend the typed lambdacalculus with intersection and union types, and its corresponding prooffunctional logic, previously defined by the authors, with subtyping and explicit coercions.We show the extension of the lambdacalculus to be isomorphic to the BarbaneraDezanide'Liguoro type assignment system and we provide a sound interpretation of the prooffunctional logic with the NJ(β) logic, using Mints' realizers.We finally present a sound and complete algorithm for subtyping in presence of intersection and union types. The algorithm is conceived to work for the (sub)type theory Ξ.

[4] 
Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto.
Towards a Logical Framework with Intersection and Union Types.
In 11th International Workshop on Logical Frameworks and
Metalanguages, LFMTP 2017, pages 1  9, September 2017.
[ bib 
http 
.pdf ]
We present an ongoing implementation of a dependenttype theory (Δframework) based on the Edinburgh Logical Framework LF, extended with Prooffunctional logical connectives such as intersection , union, and strong (or minimal relevant) implication. Prooffunctional connectives take into account the shape of logical proofs, thus allowing to reflect polymorphic features of proofs in formulae. This is in contrast to classical Truthfunctional connectives where the meaning of a compound formula is only dependent on the truth value of its subformulas. Both Logical Frameworks and proof functional logics consider proofs as first class citizens. But they do it differently namely, explicitly in the former while implicitly in the latter. Their combination opens up new possibilites of formal reasoning on prooftheoretic semantics. We provide some examples in the extended type theory and we outline a type checker. The theory of the system is under investigation. Once validated in vitro, the prooffunctional type theory can be successfully plugged in existing truthfunctional proof assistants.

[5] 
Furio Honsell, Luigi Liquori, Ivan Scagnetto, and Claude Stolze.
The Δframework.
working paper or preprint, February 2018.
[ bib 
http 
.pdf ]
We introduce a dependenttype theory Δframework, LFΔ , based on the Edinburgh Logical Framework LF, extended with the strong prooffunctional connectives intersection, union, and relevant implication. Prooffunctional connectives take into account the shape of logical proofs, thus allowing the user to reflect polymorphic features of proofs in formulae. This is in contrast to classical and intuitionistic connectives where the meaning of a compound formula is dependent only on the truth value or the provability of its subformulae. Both Logical Frameworks and Proof Functional Logics consider proofs as first class citizens albeit differently. The former mention proofs explicitly, while the latter mention proofs implicitly. Their combination therefore opens up new possibilites of formal reasoning on prooftheoretic semantics. We study the metatheory of LFΔ and provide various examples of applications. Moreover, we discuss a prototype implementation of a type checker and a refiner allowing the user to accelerate and possibly automate, the proof development process. This prooffunctional type theory can be plugged in existing common proof assistants.

[6] 
Luigi Liquori and Claude Stolze.
The Deltacalculus: syntax and types.
working paper or preprint, March 2018.
[ bib 
http 
.pdf ]
We present the Deltacalculus, an explicitly typed lambdacalculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the CoppoDezani, the CoppoDezaniSallé, the CoppoDezaniVenneri and the BarendregtCoppoDezani ones, producing a family of Deltacalculi with related intersection type systems. We prove the main properties like ChurchRosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection type systems à la Church by means of an essence function translating an explicitly typed Deltaterm into a pure lambdaterm one. We finally translate a Deltaterm with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Deltacalculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.

This file was generated by bibtex2html 1.97.