Disjunctive discourse referents in French Sign Language

Disjoined noun phrases, like indefinites, may introduce indeterminate discourse referents. Disjunction provides more flexibility in some respects than indefinites, though, as the two disjuncts may bear different morphological features, and a disjunctive discourse referent may have a split antecedent. Sign language, too, has been shown to bear on arguments pertaining to discourse anaphora. Notably, discourse referents may be established at locations in the signing space (loci), closely paralleling the use of variables in dynamic semantics. Here, we compare several theories of disjunctive anaphora and of space in sign language with new data from French Sign Language (LSF). We argue that loci must be mediated by a featural layer that iconically preserves mereological properties.

Towards an Extrinsic Formalization of Featherweight Java in Agda

Featherweight Java is one of the most popular calculi which specify object-oriented programming features. It has been used as the basis for investigating novel language functionalities, as well as to specify and understand the formal properties of existing features for languages in this paradigm. However, when considering mechanized formalization, it is hard to find an implementation for languages with complex structures and binding mechanisms as Featherweight Java. In this paper we formalize Featherweight Java, implementing the static and dynamic semantics in Agda, and proving the main safety properties for this calculus.

In search of the narrator

The chapter proposes a semantic analysis of narrators in fiction, addressing three main issues: (a) in fiction, we cannot rely on reality to determine the identity of the narrator, (b) there are linguistic items beyond pronouns to introduce a narrator, and (c) narrators can be unreliable. It shows how narrators in fiction can be modeled by discourse referents (drefs) in dynamic semantics. At the core of the analysis is the assumption that hearers derive subjective meanings by taking into account all contexts c that could be the context they are in. Combined with dynamic semantics, this captures the intuition that a narrator can be both unique and indefinite. Different types of narrator introduction are surveyed: apart from first-person pronouns, speaker-oriented items like exclamatives, questions, and evidentials trigger the accommodation of a narrator dref. Other items, like predicates of personal taste, can but need not refer to the narrator dref. The analysis is extended to unreliable narrators and narrations about humanless worlds.

A dynamic semantics of single-wh and multiple-wh questions

We develop a uniform analysis of single-wh and multiple-wh questions couched in dynamic inquisitive semantics. The analysis captures the effects of number marking on which-phrases, and derives both mention-some and mention-all readings as well as an often neglected partial mention-some reading in multiple-wh questions.

An Alleged Ambiguity and the Dynamics of Context-Change

The observation that demonstrative expressions allow for both bound and referential readings, and can be bound across sentence boundaries, provides independent motivation for a shifty account of context. Dynamic semantics offers an elegant model of shiftiness, in treating the context as a running record of potential interpretive dependencies, and utterances as instructions to update and possibly change extant dependencies. Such an account advances over the static Kaplanean model insofar as it allows for the interpretation to be dynamically affected by the linguistic elements in the preceding discourse. However, due to the way it represents linguistic dependencies, and due to its reliance on both linguistic and non-linguistic effects of context to determine interpretation, the account still makes demonstrative pronouns indefinitely ambiguous at the level of logical form, thus inheriting some of the theoretical problems of the static account.

Taming the Merge Operator

Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition, and simple solutions to hard modularity problems. Unfortunately, recent calculi with disjoint intersection types and the merge operator lack a (direct) operational semantics with expected properties such as determinism and subject reduction, and only account for terminating programs. This paper proposes a type-directed operational semantics (TDOS) for calculi with intersection types and a merge operator. We study two variants of calculi in the literature. The first calculus, called λ i , is a variant of a calculus presented by Oliveira et al. (2016) and closely related to another calculus by Dunfield (2014). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject reduction. Using our TDOS, we obtain a direct semantics for λ i that has both properties. The second calculus, called λ i + , employs the well-known subtyping relation of Barendregt, Coppo and Dezani-Ciancaglini (BCD). Therefore, λ i + extends the more basic subtyping relation of λ i , and also adds support for record types and nested composition (which enables recursive composition of merged components). To fully obtain determinism, both λ i and λ i + employ a disjointness restriction proposed in the original λ i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike previous calculi with disjoint intersection types where recursion is problematic. We relate the static and dynamic semantics of λ i to the original version of the calculus and the calculus by Dunfield. Furthermore, for λ i + , we show a novel formulation of BCD subtyping, which is algorithmic, has a very simple proof of transitivity and allows for the modular addition of distributivity rules (i.e. without affecting other rules of subtyping). All results have been fully formalized in the Coq theorem prover.

A Computational Treatment of Anaphora and Its Algorithmic Implementation

In this paper, we propose a framework capable of dealing with anaphora and ellipsis which is both general and algorithmic. This generality is ensured by the compination of two general ideas. First, we use a dynamic semantics which reperent effects using a monad structure. Second we treat scopes flexibly, extending them as needed. We additionally implement this framework as an algorithm which translates abstract syntax to logical formulas. We argue that this framework can provide a unified account of a large number of anaphoric phenomena. Specifically, we show its effectiveness in dealing with pronominal and VP-anaphora, strict and lazy pronouns, lazy identity, bound variable anaphora, e-type pronouns, and cataphora. This means that in particular we can handle complex cases like Bach–Peters sentences, which require an account dealing simultaneously with several phenomena. We use Haskell as a meta-language to present the theory, which also consitutes an implementation of all the phenomena discussed in the paper. To demonstrate coverage, we propose a test suite that can be used to evaluate computational approaches to anaphora.

A focused solution to the avoidance problem

In ML-style module type theory, sealing often leads to situations in which type variables must leave scope, and this creates a need for signatures that avoid such variables. Unfortunately, in general, there is no best signature that avoids a variable, so modules do not always enjoy principal signatures. This observation is called the avoidance problem. In the past, the problem has been circumvented using a variety of devices for moving variables so they can remain in scope. These devices work, but have heretofore lacked a logical foundation. They have also lacked a presentation in which the dynamic semantics is given on the same phrases as the static semantics, which limits their applications. We can provide a best supersignature avoiding a variable by fiat, by adding an existential signature that is the least upper bound of its instances. This idea is old, but a workable metatheory has not previously been worked out. This work resolves the metatheoretic issues using ideas borrowed from focused logic. We show that the new theory results in a type discipline very similar to the aforementioned devices used in prior work. In passing, this gives a type-theoretic justification for the generative stamps used in the early days of the static semantics of ML modules. All the proofs are formalized in Coq.