The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionistic logic. Moreover, typable terms are translated in a typed version, so that --typed (...) combinatory logic terms are proved to completely codify the associated logical proofs. (shrink)

We present a type inference system for pure λ-calculus which includes, in addition to arrow types, also universal and existential type quantifiers, intersection and union types, and type recursion. The interest of this system lies in the fact that it offers a possibility to study in a unified framework a wide range of type constructors. We investigate the main syntactical properties of the system, including an analysis of the preservation of types under parallel reduction strategies, leading to a form of (...) the subject-reduction property. We describe a model for this system where types are special subsets of a D∞ model for λ-calculus, without imposing any formal contractiveness constraint on types of the kind considered for a closely related system by MacQueen, Plotkin and Sethi. (shrink)

This paper discusses the relation between the minimal positive relevant logic B and intersection and union type theories. There is a marvelous coincidence between these very differently motivated research areas. First, we show a perfect fit between the Intersection Type Discipline ITD and the tweaking BT of B, which saves implication and conjunction but drops disjunction . The filter models of the -calculus (and its intimate partner Combinatory Logic CL) of the first author and her coauthors then become theory models (...) of these calculi. (The logician's "theory" is the algebraist's "filter".) The coincidence extends to a dual interpretation of key particles—the subtype translates to provable , type intersection to conjunction , function space to implication, and whole domain to the (trivially added but trivial) truth T. This satisfying ointment contains a fly. For it is right, proper, and to be expected that type union should correspond to the logical disjunction of B. But the simulation of functional application by a fusion (or modus ponens product) operation on theories leaves the key Bubbling lemma of work on ITD unprovable for the -prime theories now appropriate for the modeling. The focus of the present paper lies in an appeal to Harrop theories which are (a) prime and (b) closed under fusion. A version of the Bubbling lemma is then proved for Harrop theories, which accordingly furnish a model of and CL. (shrink)

This research aims to examine access to medical treatment during the COVID-19 pandemic for people living with disabilities. During the COVID-19 pandemic, the practical and ethical problems of allocating limited medical resources such as intensive care unit beds and ventilators became critical. Although different countries have proposed different guidelines to manage this emergency, these proposed criteria do not sufficiently consider people living with disabilities. People living with disabilities are therefore at a higher risk of exclusion from medical treatments as physicians (...) tend to assume they have poor quality of life, whereas access to medical treatment should be based on several parameters, including clinical data and prognosis. However, the COVID-19 pandemic shifts the medical paradigm from person-centred medicine to community-centred medicine, challenging the main ethical theories. We reviewed the main guidelines and recommendations for resources allocation and examined their position toward persons with disabilities. Based on our findings, we propose criteria for not discriminating against people with disabilities in allocating resources. The shift from person-centred to community-centred medicine offers opportunities but also risks sacrificing the most vulnerable people. The principle of reasonable accommodation must always be considered to guarantee the rights of persons with disabilities. (shrink)

Recent research showed the potential benefits of robot-assisted therapy in treating children with Autism Spectrum Disorder. These children often have some form of Intellectual Disability too, but this has mainly been neglected by previous robotics research. This article presents an empirical evaluation of robot-assisted imitation training, where the child imitated the robot, integrated into the Treatment and Education of Autistic and related Communication handicapped Children program. The sample included six hospitalized children with different levels of ID, from mild to profound. (...) We applied mixed methods to assess their progress, during treatment and three months later. Results show increased Gross Motor Imitation skills in the children, except for those with profound ID and the therapists’ positive attitude towards the humanoid robot. Furthermore, the therapists suggest how a robot could be used to autonomously collect and analyze the information obtained in the rehabilitation training for a continuous evaluation of the participants. (shrink)

It was observed by Curry that when λ-terms can be assigned types, for example, simple types, these terms have nice properties . Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems and Ω. (...) The proofs use variants of the method of reducibility. In this paper, we present a uniform approach for proving several meta-theorems relating properties of λ-terms and their typability in the systems and Ω. Our proofs use a new and more modular version of the reducibility method. As an application of our metatheorems, we show how the characterizations obtained by Coppo, Dezani, Veneri, and Pottinger, can be easily rederived. We also characterize the terms that have weak head-normal forms, which appears to be new. We conclude by stating a number of challenging open problems regarding possible generalizations of the realizability method. (shrink)

We study the intersection type assignment system as defined by Barendregt, Coppo and Dezani. For the four essential variants of the system (with and without a universal type and with and without subtyping) we show that the emptiness (inhabitation) problem is recursively unsolvable. That is, there is no effective algorithm to decide if there is a closed term of a given type. It follows that provability in the logic of "strong conjunction" of Mints and Lopez-Escobar is also undecidable.

In [gallier], general results (due to Coppo, Dezani and Veneri) relating properties of pure lambda terms and their typability in some systems with conjunctive types are proved in a uniform way by using the reducibility method.This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.

In his Lives, Giorgio Vasari mentions many artists who were talented at music when they were young, prominently Giorgione and Sebastiano del Piombo. Benvenuto Cellini resisted his father's pressure to choose music. Why? How rewarding was a musical profession in Renaissance Italy? It could be very lucrative, both for town musicians such as Cellini's father and for castratos. Moonlighting for banquets, dances, even spying, could bring in additional income. For gentlemen, music was a necessary social grace; they had private tutors, (...) such as Silvestro Ganassi dal Fontego, who was himself a painter as well as a printer. Amateurs could learn from cathedral choirmasters, who were often music theorists, the pinnacle of the profession. The theorist Pietro Aaron, choirmaster at Imola Cathedral, then tutor to the sons of Sebastian Michiel, Grand Prior of the Knights of St John of Jerusalem in Venice, had a wide acquaintance among humanists, noblemen and other musicians, and his letters open a window on the life of a musician. Among his many professions, the writer Antonfrancesco Doni counted music; a madrigal he wrote in 1560 is included in an appendix. The ability to improvise verses and music was much prized, ranging from star performers such as Serafino Aquilano to amateurs such as Niccolò Machiavelli. Portraits of musicians are discussed; they offer important evidence but are difficult to interpret. The theorist Lodovico Zacconi concluded in 1592 that being a musician was not only an honourable and lucrative profession but an enjoyable one. (shrink)

The first system of intersection types, Coppo and Dezani [3], extended simple types to include intersections and added intersection introduction and elimination rules (( $\wedge$ I) and ( $\wedge$ E)) to the type assignment system. The major advantage of these new types was that they were invariant under β-equality, later work by Barendregt, Coppo and Dezani [1], extended this to include an (η) rule which gave types invariant under βη-reduction. Urzyczyn proved in [6] that for both these systems (...) it is undecidable whether a given intersection type is empty. Kurata and Takahashi however have shown in [5] that this emptiness problem is decidable for the sytem including (η), but without ( $\wedge$ I). The aim of this paper is to classify intersection type systems lacking some of ( $\wedge$ I), ( $\wedge$ E) and (η), into equivalence classes according to their strength in typing λ-terms and also according to their strength in possessing inhabitants. This classification is used in a later paper to extend the above (un)decidability results to two of the five inhabitation-equivalence classes. This later paper also shows that the systems in two more of these classes have decidable inhabitation problems and develops algorithms to find such inhabitants. (shrink)