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.

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)

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.

We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set (...) of strongly normalizing terms of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms. (shrink)

We solve a question of McLaughlin by showing that if A is a regressive co-simple isol, there is a co-simple regressive isol B such that the intersection type of A and B is trivial. The proof is a nonuniform 0 priority argument that can be viewed as the execution of a single strategy from a 0-argument. We establish some limit on the properties of such pairs by showing that if AxB has low degree, then the intersection type of (...) A and B cannot be trivial. (shrink)

A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems.

We propose related algorithms for unification and constraint simplification in }F’&, a refinement of the simply-typed A-calculus with subtypes and bounded intersection types. }F""’ is intended as the basis of a logical framework in order to achieve more succinct and declarative axiomatiza-.

In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...) (based on weak head reduction and normal $beta$-reduction) we obtain the same interpretation for types. Since the presence of $omega$ prevents typability and realisability from coinciding and creates extra difficulties in characterizing the interpretation of a type, we define a class ${mathbb U}^+$ of the so-called positive types (where $omega$ can only occur at specific positions). We show that if a term inhabits a positive type, then this term is $beta$-normalisable and reduces to a closed term. In other words, positive types can be used to represent abstract data types. The completeness theorem for ${mathbb U}^+$ becomes interesting indeed since it establishes a perfect equivalence between typable terms and terms that inhabit a type. In other words, typability and realisability coincide on ${mathbb U}^+$. We give a number of examples to explain the intuition behind the definition of ${mathbb U}^+$ and to show that this class cannot be extended while keeping its desired properties. (shrink)

Positive public perceptions of academic quality and professional ethics are critical to the long-term legitimacy of American colleges and universities. Faculty codes of conduct are one mechanism whereby the professoriate can define acceptable practice, exercise social control, and maintain public confidence in higher education, yet the drivers of their adoption are not well understood. Building upon previous research into such organizational behavior by institutional type, this study examined the prevalence and content of publicly posted faculty codes of conduct within an (...) organizational field of institutions that share a common religious identity but differ in their institutional types and employment structures. Faculty handbooks from American member institutions of the Council for Christian Colleges & Universities, an international association of faith-based institutions, were gathered and analyzed. Although only 27% of CCCU member institutions in the U.S. publicly posted faculty codes of conduct, the average number of tenets present in each code was higher than suggested by previous research. Study findings also revealed that membership category, institutional type, and employment structures influence the content of faculty codes of conduct, indicating that isomorphic pressures operate within this particular organizational field. The piece concludes by commending publicly posted codes of conduct as an affirmation of the personal responsibility, fairness, and care exercised by ethical professionals in the academy. (shrink)

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)

This paper studies intersection and union type assignment for the calculus , a proof-term syntax for Gentzen’s classical sequent calculus, with the aim of defining a type-based semantics, via setting up a system that is closed under conversion. We will start by investigating what the minimal requirements are for a system, for to be complete ; this coincides with System , the notion defined in Dougherty et al. [18]; however, we show that this system is not sound , so (...) our goal cannot be achieved. We will then show that System is also not complete, but can recover from this by presenting System as an extension of and showing that it satisfies completeness; it still lacks soundness. We show how to restrict so that it satisfies soundness as well by limiting the applicability of certain type assignment rules, but only when limiting reduction to call-by-name or call-by-value reduction; in restricting the system this way, we sacrifice completeness. These results when combined show that, with respect to full reduction, it is not possible to define a sound and complete intersection and union type assignment system for. (shrink)

This paper develops an account of intersectional feminist theory by critically examining the notion of identity implicitly assumed in major critiques of intersectionality. Critics take intersectionality to fragment women along the lines of identity categories such as race, class, and sexuality. Underlying this interpretation, I argue, is the metaphysical assumption that identity is a fixed entity. This is a misunderstanding of identity that neglects how identity is actually lived. By exploring how Asian American women experience their “Asian” identity in their (...) everyday lives (e.g., the “Asian-as-patriarchal vs. White-as-gender-progressive” stereotype, growing anti-Asian racism amid COVID-19, and Asian-Black feminist solidarities), I demonstrate that Asian identity is not fixed but changing according to how it is related to power. I identify and discuss three characteristic types of the identity-power relationship: manifestation of power-as-oppression through the construction of identity, reproduction of power-as- oppression, and creation of new forms of power, namely resistance and solidarity, through the reconstruction of identity. The lives of multiply-oppressed women (e.g., Asian women) can be understood as the locus at which the identity-power relationship is worked out, that is, the power dynamics of oppression are manifested, reproduced, and resisted through the (re)construction of identity. Building on this analysis and engaging discussions on non-ideal theory in social/political philosophy, I argue that intersectional feminist theory can be best explained as a non-ideal theory in a strong sense: a theory that, by focusing on the lives of the multiply oppressed, presents the intersecting dynamics of oppression as central and theory-guiding. (shrink)

In transfinite arithmetic 2n is defined as the cardinality of the family of all subsets of some set v with cardinality n. However, in the arithmetic of recursive equivalence types 2N is defined as the RET of the family of all finite subsets of some set v of nonnegative integers with RET N. Suppose v is a nonempty set. S is a class over v, if S consists of finite subsets of v and has v as its union. Such (...) a class is an intersecting class over v, if every two members of S have a nonempty intersection. An IC over v is called a maximal IC , if it is not properly included in any IC over v. It is known and readily proved that every MIC over a finite set v of cardinality n ≥ 1 has cardinality 2n-1. In order to generalize this result we introduce the notion of an ω-MIC over v. This is an effective analogue ot the notion of an MIC over v such that a class over a finite set v is an ω-MIC iff it is an MIC. We then prove that every ω-MIC over an isolated set v of RET N ≥ 1 has RET 2N-1. This is a generalization, for while there only are χ0 finite sets, there are ϰ isolated sets, where c denotes the cardinality of the continuum, namely all the finite sets and the c immune sets. MSC: 03D50. (shrink)

The transitions between turns at talk in conversation tend to occur quickly, with only a slight gap of approximately 100 to 300 ms between them. This estimate of central tendency, however, hides a wealth of complex variation, as a number of factors, such as the type of turns involved, have been shown to influence the timing of turn transitions. This article considers one specific type of turn that does not conform to the statistical trend, namely turns that deal with troubles (...) of speaking, hearing, and understanding, known as other-initiations of repair. The results of a quantitative analysis of 169 other-initiations of repair in face-to-face conversation reveal that the most frequent cases occur after gaps of approximately 700 ms. Furthermore, other-initiations of repair that locate a source of trouble in a prior turn specifically tend to occur after shorter gaps than those that do not, and those that correct errors in a prior turn, while rare, tend to occur without delay. An analysis of the transitions before other-initiations of repair, using methods of conversation analysis, suggests that speakers use the extra time (i) to search for a late recognition of the problematic turn, (ii) to provide an opportunity for the speaker of the problematic turn to resolve the trouble independently, (iii) and to produce visual signals, such as facial gestures. In light of these results, it is argued that other-initiations of repair take priority over other turns at talk in conversation and therefore are not subject to the same rules and constraints that motivate fast turn transitions in general. (shrink)

A poset is well‐partially ordered (WPO) if all its linear extensions are well orders; the supremum of ordered types of these linear extensions is the length, of p. We prove that if the vertex set X is infinite, of cardinality κ, and the ordering ⩽ is the intersection of finitely many well partial orderings of X,, then, letting, with, denote the euclidian division by κ (seen as an initial ordinal) of the length of each corresponding poset: where denotes (...) the least initial ordinal greater than the ordinal. This inequality is optimal. This result answers questions of Forster. (shrink)

At the intersection of taxonomy and nomenclature lies the scientific practice of typification. This practice occurs in biology with the use of holotypes (type specimens), in geology with the use of stratotypes, and in metrology with the use of measurement prototypes. In this paper I develop the first general definition of a scientific type and outline a new philosophical theory of types inspired by Pierre Duhem. I use this general framework to resolve the necessity-contingency debate about type specimens (...) in philosophy of biology, to advance the debate over the myth of the absolute accuracy of standards in metrology, and to address the definition-correlation debate in geology. I conclude that just as there has been a productive synergy between philosophical accounts of natural kinds and scientific taxonomic practices, so too there is much to be gained from developing a deeper understanding of the practices and philosophy of scientific types. (shrink)

Ethical challenges that arise within healthcare delivery institutions are currently categorized as either clinical or organizational, based on the type of issue. Despite this common binary issue-based methodology, empirical study and increasing academic dialogue indicate that a clear line cannot easily be drawn between organizational and clinical ethics. Disagreement around end-of-life treatments, for example, often spawn value differences amongst parties at both organizational and clinical levels and requires a resolution to address both the case at hand and large-scale underlying system-level (...) confounders. I refer to issues that contain elements of both clinical and organizational issues as hybrids and propose a new taxonomy to characterize hybrid cases. I contend that salient contextual features of an ethical issue, such as where it is identified, who it impacts and where it is ideally resolved in relation to its scope of impact, should inform procedure. Implementation of a Hybrid taxonomy viewing ethical issues as existing on a continuum furthers that end. The primary goals are to 1) systematize thinking about ethical issues that arise within healthcare delivery institutions and 2) allow the content of the ethical challenge to drive the process, rather than continuing to rely on the traditional binary issue-based choice. Failure to capture the complexity of hybrid situations perpetuates incomplete information and ultimately an inchoate resolution that creates more questions than answers. (shrink)

In this paper, we shall present a generalization of phrase structure grammar, in which all functional categories have type restrictions, that is, their argument types are specific domains. In ordinary phrase structure grammar, there is just one universal domain of individuals. The grammar does not make a distinction between verbs and adjectives in terms of domains of applicability. Consequently, it fails to distinguish between sentences like every line intersects every line, which is well typed, and every line intersects every (...) point, which is ill typed.Our generalization relates to ordinary phrase structure grammar in the same way as the higherlevel constructive type theory of Martin-Löf relates to the simple type theory of Church . Simple type theory has been used in linguistics and related with phrase structure grammar, especially in the tradition based on the work of Montague .Our definition of the grammar will be more formal than Montague's in the sense that we shall use a formal metalanguage, that of constructive type theory, for defining both the object language and its interpretation. The grammar, both syntax and semantics, is thus readily implementable in the type-theoretical proof system ALF . Inside type theory, a distinction can be made between the object language and the model, in other words, between syntactic and semantic types. It will turn out that the object language cannot be defined independently of the model, as in ordinary Tarski semantics. This is a direct consequence of introducing the typing restrictions.The grammar presented here can be seen as a formal linguistic elaboration of the work presented in Ranta 1991 and 1994. The organization of generative grammar as categorial grammar followed by sugaring should now look more familiar to the linguist, as the grammatical formalism on which sugaring operates is no longer full type theory but a set of phrase structure trees. (shrink)

Speakers of jokes are aware of the human cognitively rooted relevance-seeking inferential procedure and predict the interlocutor’s steps leading to a valid interpretation of the utterance in the joke. Specifically, speakers can predict the accessibility to certain information which builds up a proper scenario for understanding the joke, the inferential steps taken to turn the words uttered into contextualized meaningful propositions, and the awareness of cultural stereotypes regarding professions, nationalities, connoted places, sex roles, etc.. This inferred information is exploited to (...) generate humorous effects. In previous research, the Intersecting Circles Model was proposed. It comprises seven types of jokes depending on whether the joke only relies on one of or on combinations of them, which entails analyzing the extent to which play or do not play a role in the generation of humorous effects. In this paper, 1000 jokes are analyzed and fitted into a type or combinations of. Several interesting humor-generating patterns are also isolated inside the seven preliminary joke types covered by the Model. (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)

Despite the demonstrated utility of intersectionality, research on men allied with women’s rights movements has largely focused on white, heterosexual, middle-class, young men. This study illustrates the importance of attending to men’s intersecting identities by evaluating the applicability of existing knowledge about men’s engagement pathways to the predominantly African American members of a Muslim men’s anti–domestic violence group and a gay/queer men’s gender justice group. Findings from a year-long qualitative study highlight how these men’s experiences differ from those in the (...) literature. While the Muslim men’s experiences add dimension to the existing knowledge—especially regarding age and parenthood, online interactions, and formal learning opportunities—the gay/queer men’s experiences are not accurately represented within it. Their pathways begin earlier, do not rely on women’s input, do not create a shift in gendered worldview, and lack a pathway narrative because they connect to gender justice through their own intersecting identities and experiences. This suggests that a marginalized identity is not in itself sufficient to alter engagement pathways; the particular type of marginalization matters. (shrink)

The attempt to find usable diagrams fornterms of the sort devised by John Venn seems to have originated with Venn himself, who published diagrams for up to five classes (the fifth class, however, was shaped like a doughnut, and contained an area outside itself — like the hole in the doughnut). Venn then suggested that “if we wanted to use a diagram forsixterms (x, y, z, w, v, u) the best plan would probably be to taketwofive-term figures, one for theupart (...) and one for the non-upart of all the other combinations …” Such a method would, as Venn admits, be somewhat confusing to the eye, and thus fail to fulfil one of the major purposes of the diagram; nevertheless, it is a method which could be extended to covernclasses.Venn also suggests (but without illustration) another method for drawing diagrams fornterms: “… the rule of formation would be very simple. We should merely have to begin by drawing any closed figure, and then proceed to draw others subject to the one condition that each intersect once, and once only, all the existing subdivisions produced by those which had gone before.” Then, in a rather surprising footnote, he adds: “It will be found that when we adhere to continuous figures, instead of the discontinuous five-term figure given above, there is a tendency for the resultant outlines thus successively drawn to assume a comb-like shape after the first four or five. If we begin by circles or other rounded figures the teeth are curved, if by parallelograms then they are straight. (shrink)

With age might come a decline in crucial driving skills. The effect of a collision warning system on older drivers' head movements behavior at intersections was examined.Methods: Twenty-six old-adults, between 55 and 64 years of age, and 16 Older drivers between 65 and 83 years of age, participated in the study. A CWS and a front-back in-vehicle camera were installed in each of the participants' own vehicles for 6 months. The CWS was utilized to identify unsafe events during naturalistic driving (...) situations, and the IVC was used to capture head direction at intersections. The experimental design was conducted in three phases, 2 months each. Unsafe events were recorded by the CWS during all phases of the study. In the second phase, the CWS feedback was activated to examine its effect on drivers' head movement' behavior at intersections.Results: Older drivers drove significantly more hours in total during the intervention phase than the baseline phase and the carryover phase. The study revealed no significant differences between the head movements of older and old-adult drivers at intersections. For intersection on the left direction, a significant improvement in drivers' head movements' behavior was found at T-junctions, turns and four-way intersections from phase 1 to phase 3, however, two intersection types presented a decrease along the study phases. The head movements' behavior at roundabouts and merges was better at phase 1 compared to phase 3. There was no significant reduction of the mean number of CWS unsafe events across the study phases.Conclusions: The immediate feedback provided by the CWS was effective in terms of participants' head movements at certain intersections but was harmful in others. However, older drivers drove many more hours during the active feedback phase, implying that they trusted the system. Therefore, in the light of this complex picture, using the technological feedback with older drivers should be followed with an additional mediation or follow-up to ensure safety. (shrink)

Reciprocal interactions between the host circadian clock and the microbiota are evidenced by recent literature. Interestingly, dysregulation of either the circadian clock or microbiota is associated with common human pathologies such as obesity, type 2 diabetes, or neurological disorders. However, it is unclear to what extent a perturbation of pathways regulated by both the circadian clock and microbiota is involved in the development of these disorders. It is speculated that these perturbations are associated with impaired growth hormone (GH) secretion and (...) sexual development. The GH axis is a broadly neglected pathway and could be the main converging point for the interaction of both circadian clock and microbiota. Here, the links between the circadian clock and microbiota are reviewed. Finally, the effects of chronodisruption and dysbiosis on physiology and pathology are discussed and it is speculated whether a common deregulation of the GH pathway could mediates those effects. (shrink)

This chapter contains sections titled: Introduction: Major Problems with Trait Ascriptions The Logic of Intellectual Trait Ascription and the Generality Problem The Logic of Moral Trait Ascription and the Global Trait Problem The Common Structure of the Two Problems Acknowledgments References.

Body part terms (BPTs) are used extensively in Mesoamerican languages to name object parts. The process through which BPTs might be extended to refer to a part of an object and further serve as a relator in describing the relation between objects in space has often been attributed to metaphorical processes. This study proposes an alternative analysis following a Structure–Mapping Theory approach (Gentner, 1983, inter alia), based on data from Diidxazá (Isthmus Zapotec, Otomanguean) obtained through elicitation and experimental tasks. The (...) data show that structure mapping does not depend on a 1:1 match of attributes; frequency of use shed light on principles that constrain the semantic extension of most BPTs; a core set of six BPTs are extended by abstraction of the set of intersecting axes of the body. The detailed nature of this study enables an analysis of the mental representations underlying the semantic extension of BPTs. This in turn elucidates on aspects of the relation between spatial language and spatial cognition. In addition, this study allows us to address questions about the categorial status of BPTs in Diidxazá and their lexicographic representation. (shrink)

This article introduces the concept of epistemic positioning to theorize the relationship between identity-based epistemic judgements and the reproduction of social inequalities, including those of gender and ethnicity/race, in the academia. Acts of epistemic positioning entail the evaluation of knowledge claims based on the speaker’s stated or inferred identity. These judgements serve to limit the scope of the knowledge claim, making it more likely speakers will be denied recognition or credit. The four types of epistemic positioning – bounding (reducing (...) a knowledge claim to elements of personal identity), domaining (reducing a knowledge claim to discipline or field associated with identity), non-attribution (using the claim without recognizing the author) and appropriation (presenting the claim as one’s own) – are mutually reinforcing. Given the growing importance of visibility and recognition in the context of increasing competition and insecurity in academic employment, these practices play a role in the ability of underrepresented groups to remain in the academic profession. (shrink)

The implementation of transnational standards — in codes of conduct, certification, and monitoring initiatives — necessarily intertwines with domestic law and other types of rules. Yet much of the existing literature overlooks or obscures this fundamental point. Indeed, scholars often err either by treating private regulatory standards as transcendent or by viewing implementation as fundamentally a technical problem. This Article argues that understanding the operation of transnational private regulation requires attention to the layering of multiple rules in a given (...) location. It develops a framework for examining this layering and illustrates it by briefly looking at two major issues—community rights in sustainable forestry standards and freedom of association in fair labor standards — and their implementation in Indonesia. In various ways, these domains illustrate how conflict and complementarity between public and private standards structure the practice of private regulation. (shrink)

This research investigates the development of transferable - "adaptive" expertise. The study contrasts problem-solving performance of two kinds of experts (business consultants and restaurant managers) on novel problems at the intersection of their two domains, as well as a group of novices (non-business undergraduates). Despite a lack of restaurant experience, consultants performed better than restaurant managers and undergraduates, even though the problems concerned a restaurant. Process measures suggest this was due to the use of more theoretical reasoning. Analyses show (...) this resulted from differences in work experience and not other factors (e.g., education). We discuss aspects of experience that might be responsible for development of theoretical understanding and, thus, expertise that transfers to novel problems. One possible explanation, consistent with existing research from multiple approaches, is that to transfer to novel problems, experience must include substantive variability. The social context of learning may also play a role. (shrink)

We address three fundamental questions: What does it mean for an entity to be living? What is the role of inter-organismic collaboration in evolution? What is a biological individual? Our central argument is that life arises when lineage-forming entities collaborate in metabolism. By conceiving of metabolism as a collaborative process performed by functional wholes, which are associations of a variety of lineage-forming entities, we avoid the standard tension between reproduction and metabolism in discussions of life – a tension particularly evident (...) in discussions of whether viruses are alive. Our perspective assumes no sharp distinction between life and non-life, and does not equate life exclusively with cellular or organismal status. We reach this conclusion through an analysis of the capabilities of a spectrum of biological entities, in which we include the pivotal case of viruses as well as prions, plasmids, organelles, intracellular and extracellular symbionts, unicellular and multicellular life-forms. The usual criterion for classifying many of the entities of our continuum as non-living is autonomy. This emphasis on autonomy is problematic, however, because even paradigmatic biological individuals, such as large animals, are dependent on symbiotic associations with many other organisms. These composite individuals constitute the metabolic wholes on which selection acts. Finally, our account treats cooperation and competition not as polar opposites but as points on a continuum of collaboration. We suggest that competitive relations are a transitional state, with multi-lineage metabolic wholes eventually outcompeting selfish competitors, and that this process sometimes leads to the emergence of new types or levels of wholes. Our view of life as a continuum of variably structured collaborative systems leaves open the possibility that a variety of forms of organized matter – from chemical systems to ecosystems – might be usefully understood as living entities. (shrink)

The postsecular turn within feminist theory refers to a renewed attention to religion within feminist scholarship. However, rather than conceptualizing the postsecular as a new moment within feminist theorizing that breaks with a previous trend of secular feminism, this article stresses that it is important to recognize the long history of coexistence and contestations between religious and secular feminist approaches. In this article, the different reception histories of the story of Sojourner Truth are examined to elucidate and reflect on the (...) complicated relationship of the religious and the secular within feminist scholarship. Three different types of feminist theoretical engagement with the story of Sojourner Truth are examined and contrasted: the implicitly secular use of the story of Sojourner Truth in black feminist scholarship and theorizing of intersectionality, the explicitly religious interpretations found in the work of feminist and womanist theologians, and the deconstructive reading by Donna Haraway. In discussing and comparing these different engagements with the story of Sojourner Truth, it is stressed that the boundaries between the religious and the secular are perhaps less clear-cut than initially imagined, and that a dialogue between secular and religious feminist approaches is very fruitful. The article closes by examining how the complex intersections of gender, religion and race in the story of Sojourner Truth can be connected to the contemporary theorizing on the racialization of religion within critical race scholarship. (shrink)

In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky’s univalent interpretation of it. This interpretation has given rise to the univalent foundations program, which is the topic of the current special year at the Institute for Advanced Study.

Nanometre-sized ! '-martensites , a few nanometres in cross-sectional diameter, formed at intersections of deformation twins, have been found in a heavily deformed 316-type austenitic stainless steel and examined by high-resolution transmission electron microscopy . An orientation relationship was found to be close to the Kurdjumov-Sachs relationship, that is , . HRTEM observations were conducted with a beam direction parallel to . The observed nanometre-sized ! '-martensites exhibited a habit plane and the cross-section of the nanometre-sized ! '-martensites were elongated (...) along [545] % . It has been revealed that the nanometre-sized ! '-martensites of a few nanometres diameter formed at the intersections of deformation twins have a typical habit plane of , which is identical with that reported for a fully grown plate such as ! '-martensite. The origin of the observed habit plane is discussed on the basis of the d 112 ¢ {111} ! shear displacements assisting the % M ! ' transformation. (shrink)

This paper recognizes a specific correspondence between biological evolution and technological development and on this basis tries to set up a semioticapproach to the evolutionary phenomenon of exaptation. To do this, the existence of a historical-structural and pragmatic analogy between organs and tools is shown, which in turn implies on a communicative ground the dissolution of some of their traditional distinctive att ributes. Finally, a philosophical-analytical approach to natural and cultural functions is applied to define three types of exaptations.

Academic productivity is realized through resources obtained from professional networks in which scientists are embedded. Using a national survey of academic faculty in Science, Technology, Engineering, and Mathematics fields across multiple institution types, we examine how the structure of professional networks affects scholarly productivity and how those effects may differ by race, ethnicity, and gender. We find that network size masks important differences in composition. Using negative binomial regression, we find that both the size and composition of professional networks (...) affect scientific productivity, but bigger is not always better. We find that instrumental networks increase scholarly productivity, while advice networks reduce it. There are important interactive effects that are masked by modeling only direct effects. We find that white men are especially advantaged by instrumental networks, and women are especially advantaged by advice networks. (shrink)

In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.

In this paper we present a study of adjectival/adverbial modification using modern type theories, i.e. type theories within the tradition of Martin-Löf. We present an account of various issues concerning adjectival/adverbial modification and argue that MTTs can be used as an adequate language for interpreting NL semantics. MTTs are not only expressive enough to deal with a range of modification phenomena, but are furthermore well-suited to perform reasoning tasks that can be easily implemented given their proof-theoretic nature. In MTT-semantics, common (...) nouns are interpreted as types rather than predicates. Therefore, in order to capture the semantics of adjectives adequately, one needs to meet the challenge of modeling CNs modified by adjectives as types. To explicate that this can be done successfully, we first look at the mainstream classification of adjectives, i.e. intersective, subsective and non-subsective adjectives. There, we show that the rich type structure available in MTTs, along with a suitable subtyping framework, offers an adequate mechanism to model these cases. In particular, this modelling naturally takes care of the characterising inferences associated with each class of adjectives. Then, more advanced issues on adjectival modification are discussed: degree adjectives, comparatives and multidimensional adjectives. There, it is shown that the use of indexed types can be usefully applied in order to deal with these cases. In the same vein, the issue of adverbial modification is discussed. We study two general typings for sentence and VP adverbs respectively. It is shown that the rich type structure in MTTs further provides useful organisational mechanisms in giving formal semantics for adverbs. In particular, we discuss the use of \-types to capture the veridicality/non-veridicality distinction and further discuss cases of intensional adverbs using the type theoretic notion of context. We also look at manner, subject and speech act adverbials and propose solutions using MTTs. Finally, we show that the current proof technology can help mechanically check the associated inferences. A number of our proposals concerning adjectival and adverbial modification have been formalised in the proof assistant Coq and many of the associated inference patterns are checked to be correctly captured. (shrink)

Health innovation is mainly envisioned in direct connection to medical research institutions or pharmaceutical and technology companies. Yet, these types of innovation often do not meet the needs and expectations of individuals affected by health conditions. With the emergence of digital health technologies and social media, we can observe a shift, which involves people living with illness modifying and improving medical and health devices outside of the formal research and development sector, figuring both as users and innovators. This patient‐led (...) innovation has been celebrated in innovation studies and economics as a “bottom‐up” type of innovation. In this article, we take a closer look at open‐source patient‐led innovation in the context of type 1 diabetes care. In our inquiry, we pay particular attention to the social and ethical dimensions of this innovation, building on empirical material. Upon exploring the notion of patient‐led innovation and its socio‐political context through the lens of intersectional and global health justice, we argue that a proactive strategy is needed to ensure that open‐source patient‐led innovation will be more globally accessible, center the health needs of the most underserved populations, as well as facilitate equitable and just health benefits. To support this aim, we provide a range of examples of different initiatives addressing the persistent inequalities that have so far inhibited patient‐led innovation from more fully materializing its innovative potential. (shrink)

This essay looks at the economic and theological intersections of definitions of usury in the economic system of capitalism. It challenges seminarians and the church to examine their roles in addressing the problem of usury.

If we already had a periodic table of mental illness in hand, there would be less need for a book of this type. Although some psychiatrists do think of themselves as chemists, the analogy is without warrant. Not only does psychiatry lack an analogue of the periodic table, its principal tool -- the Diagnostic and Statistical Manual of Mental Disorders (DSM) -- is a contentious document. Even subsequent to the publication of DSM-III in 1980, which was intended to serve as (...) an operational guideline for clinical practice, it and its heirs (DSM-V was published in 2013) have often fueled rather than quelled controversy. Although beginning with that third major revision of DSM a concerted effort has been made to ensure greater consistency in diagnoses, psychiatry remains beset by concerns that it is insufficiently scientific, unduly influenced by the pharmaceutical industry, indecisive as to whether it should focus on the mind or the brain, incapable of distinguishing among types of diseases, inclined to expand illness criteria without adequate justification, overly reliant on subjective judgments, wont to conflate clinical and ethical judgments, and engaged in indiscriminate use of psychoactive drugs. These worries concerning its scientific and ethical status are among the reasons that psychiatry attracts the attention of philosophers. (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)