The
pioneering work of Ranta (1994) on using Type Theory for NL
semantics has initiated a strong interest in the use of Type
Theories for representing formal semantics. And even though
Type Theory was initially mainly concerned
with compositional and formal semantics, a number of
linguists, logicians and computer scientists noticed the
relevance of type theory for lexical semantics as
well. Around 2000 the paper “the metaphysics of words in
context” by Asher & Pustejovsky (2001) initiated Type
Theoretic approaches to lexical coercions and meaning
transfers by investigating extension and refinement of the type
system used by Montague. Accounts for this type of phenomena
need to capture ordinary selectional restriction phenomena
(e.g. a “chair” may not “bark”, in an ordinary context), while
at the some time they have to ensure some flexibility for
adapting meanings to contexts in case of meaning transfers,
co-predication etc. The study of this kind of phenomena is of
course not new. Their study goes back at least till the 80’s
(Bierwisch, Nunberg, Cruse among others). What is
relatively new is the study of these phenomena from the
perspective of Type Theory and this approach is by now quite
successful as valuable type theoretical contributions on
incorporating lexical considerations into compositional
semantics show (Asher, Bassac, Chatzikyriakidis, Cooper, Luo,
Melloni, Mery, Moot, Prévot, Pustejovsky, Ranta, Real, Retoré)

Authors
are invited to submit 4-page abstracts before March 31 on any
subject related to the workshop, including:

- Linguistically
motivated variants of type theories (subtyping)
- Lexical
semantics in type theory (compositionality and the lexicon)
- Interaction
between lexical semantics and type theoretical semantics
- Classical
semantic questions in richly typed frameworks (plurals,
quantification, generics)
- Modelling
specific questions in type theory (nouns, deverbals, events,
adjectives, adverbs, ontological aspects,)
- Computational aspects
and implementation of type theoretical semantics (natural
language inference, proof assistants,…)

- submission
of 4-page abstract (PDF) before March 31

please use https://easychair.org/conferences/?conf=tytles-2015 - notification
of acceptance: April 30
- revised
4 page abstracts due: May 15
- conference date and location: Barcelona August 3-7 2015 see ESSLLI 2015

Papers
on this page should be referred to as follows: Author, Title in
ESSLLI proceedings of the TYTLES workshop on Type Theory and
Lexical Semantics (Cooper, Retoré, eds) ESSLLI 2015,
Barcelona.

**Monday14:00-15:30**

**14:00 Christian
Retoré (and Robin Cooper), Introduction **

**14:30 Justyna Grudzinska and
Marek Zawadowski. A Puzzle about Long-distance Indefinites
and Dependent Type Semantics**

Dependently Typed Semantics with Generalized Quantifiers (DTSGQ)
combines two semantic approaches to account for natural language
quantification: Generalized Quantifier Theory familiar from
Montague-style semantics (Mostowski, A. 1957, Lindstrˆm, P.
1966, Barwise, J., Cooper, R. 1981) and type-theoretic approach
(Martin-Löf, P. 1972, Ranta, A. 1994, Makkai, M. 1995, Luo, Z.
2012). Like in the classical Montague-style analysis, DTSGQ
makes essential use of generalized quantifiers (GQs). But in the
spirit of the type-theoretic framework we adopt a many-typed
analysis (in place of a standard single-sorted analysis). Like
in the standard type-theoretic approaches, we have type
dependency in our system. But our semantics is
model-theoretic (with truth and reference being basic concepts),
and not proof-theoretic (where proof is a central semantic
concept). Combining GQs with dependent types allows us to
handle in a uniform manner a number of semantic puzzles
concerning natural language quantifiers. In our previous work we
have defined a new interpretational algorithm to account for a
wide range of anaphoric (dynamic) effects associated with
natural language quantification (Grudzinska, J., Zawadowski, M.
2014). In this paper we will tackle the phenomenon of
exceptional scopes of one class of quantifiers (indefinites) and
the so-called puzzle about long-distance indefinites that seems
to be unsettled in the literature (see Chierchia, G. 2001,
Schwarz, B. 2001, Szabolcsi, A. 2010). Our solution to the
puzzle about long-distance indefinites makes crucial use of
dependent types, i.e. we propose to credit the problematic
long-distance readings to the presence of possibly hidden)
dependencies.

**15:00 Stergios
Chatzikyriakidis, Mathieu Lafourcade, Lionel Ramadier and
Manel Zarrouk. Type Theories and Lexical Networks: Using
Serious Games as the Basis for Multi-Sorted Typed Systems**

In this paper, we show how a rich lexico-semantic network which
has been built using serious games, JeuxDeMots, can help us in
grounding our semantic ontologies as well as different sorts of
information in doing formal semantics using modern type theories
(type theories within the tradition of Martin L¨of). We discuss
the domain of base types, adjectival and verbal types,
hyperonymy/hyponymy relations as well as more advanced issues
like homophony and polysemy.

**Tuesday 14:00 - 15:30**

**14:00 Staffan Larsson.
Perceptual Meaning in TTR Judgement-based Semantics and
Conceptual Spaces**

We are developing a type-theoretical judgement-based semantics
where notions such as perception, classification, judgement,
learning and dialogue coordination play a central role. By
bringing perception and semantic coordination into formal
semantics, this theory can be seen as an attempt at unifying
cognitive and formal approaches to meaning. The purpouse of this
paper is to briefly compare judgement-based semantics to the
theory of conceptual spaces. We conclude that there are
important similarities but also some differences. One aim of
judgement-based semantics is to formalise semantic
classification and learning in detail, to enable
integration of these aspects of meaning with those traditionally
studied in formal semantics, and to enable computational
modeling and implementation of these aspects of meaning. By
using statistical classifiers, we connect to machine learning
theory, giving access to a host of classification methods and
associated learning algorithms.

**14:30 Simon Dobnik.
Interfacing Language, Spatial Perception and Cognition in
Type Theory with Records**

In the proposed presentation we overview and connect two lines
of our work related to Type Theory with Records (TTR): modelling
of spatial language and cognition and modelling of
attention-driven judgement. We argue that computational
modelling of perception, action, language, and cognition
introduces several requirements on a formal semantic theory and
its practical implementations: (i) interfacing discrete
conceptual knowledge and continuous real-valued sensory
readings; (ii) information fusion of knowledge from several
modalities; (iii) dynamic adaptation of semantic
representations/knowledge as agents experience new situations
through linguistic interaction and perception. Using examples of
semantic representations of spatial descriptions we show how
Type Theory with Records satisfies these requirements. The
advantage of truth being based on agent-relative judgements in
TTR is crucial in this but practically it comes with a
computational cost. However, this challenge is not unique to
TTR. An agent would have to check whether a situation s is of
every type in its inventory. In the second part of the talk we
argue that the number of type judgements an agent has to make
can be minimised by incorporating a cognitive notion of
judgement that is driven by perceptual attention.

**15:00 Peter Sutton and Hana
Filip. Probabilistic Mereological TTR and the Mass/Count
Distinction**

The goals of this paper are threefold. (1) We argue that four
semantic classes can be used to predict cross and
intralinguistic variation in whether nouns are encoded as count
or mass. These semantic classes are defined in terms of two
kinds of sources: vagueness (Chierchia 2010) and (non-)overlap
of individuated entities (Landman 2011). (2) We enrich prob-TTR
(Cooper et al. 2014, a probabilistic variant of TTR, Cooper
2012) with mereological relations to give probM-TTR. We adopt
prob-TTR since its probabilistic basis is perfectly suited to
the representation of vagueness. We enrich it with mereology so
as to be able to express when two (mereological) entities
overlap. (3) We derive our four classes by defining vagueness
and non-overlap in probabilistic terms, and showing how
vagueness and (non-)overlap interact. The presence of neither
vagueness nor overlap is characteristic of prototypical count
nouns (cat, book). The presence of vagueness and overlap is
characteristic of “substance” mass nouns (mud, blood). Both
these noun classes display little or no cross and
intralinguistic variation in MASS/COUNT encoding. “Aggregate”
nouns (furniture, kitchenware) are not vague, but do overlap (a
pestle and mortar can count as both one and two items of
kitchenware). “Granular” nouns (lentils, rice) are vague (it is
vague how much rice counts as enough rice for dinner). Both of
these noun classes display cross- and intralinguistic
variation in MASS/COUNT encoding. Countability requires
determining a clear counting base of discrete entities.
Vagueness or overlap can interfere with counting, vagueness and
overlap always do.

Wednesday14:00 - 15:30

**14:00 Ellen Breitholtz.
Are Widows Always Wicked? Learning concepts through
enthymematic reasoning**

In this paper we suggest that enthymematic reasoning may play a
role in the acquisition of new concepts by a language learner.
On our account, a learner, for example a young child, forms
hypotheses about acceptable ways of reasoning – so called topoi
– based on observations and interaction with dialogue partners.
These topoi are then used to underpin the child’s reasoning in
other situations. To illustrate this point we analyse an example
of natural dialogue using an information state update approach
cast in Type Theory with Records. This approach allows us to
represent misunderstanding and misinterpretation of meaning,
since it is based on the conceptualisation of entities in
individuals rather than on a God's eye view of meaning. Also,
the record types of TTR offer a convenient way to represent
subtype relations, which seems to be an important aspect of our
evaluation of in which situations specific topoi are applicable
Our account fits well with an approach to word meaning where
speakers are constantly adjusting meanings on the basis of
experience, and where meaning may be negotiated in
interaction. Also, our account of word acquisition relates to
Pustejovsky’s (1998) suggestion that enthymemes, or enthymematic
reasoning, may be a means for lexical interpretation.

**14:30 **** Bruno
Mery. The Relative Complexity of Constraints in
Co-Predicative Utterances
**In
examining “The Relative Complexity of Constraints in
Co-Predicative Utterances”, we want to explore one among many
phenomena of lexical semantics that are at once hard to
characterise and prone to many exceptions and idiosyncrasies,
and nevertheless can be formally treated in compositional
semantics, thus illustrating the expressive power of
adaptative logical frameworks for semantics and the specific
challenges in gathering adequate data to evaluate their
validity. We detail the particular variations of semantic
felicity in co-predicative utterances the constraints on the
combination of facets of polysemous words, and the possible
adaptations that can be proposed to existing formal frameworks
that support lexical semantics. As the linguistic data is
incomplete and disputed, we also include a proposal for a
linguistic survey aimed at clearing up many outstanding
issues.This communication is intended as a discussion
material, detailing a specific issue in order to foster
collaborations around the subject. Having been prepared by the
author in his spare time, it is, by necessity, incomplete. The
work presented here is closely related to /\TYn, a formal
framework for lexical semantics developed since 2006 with
Christian Bassac, Richard Moot, Christian Retoré and many
other researchers at LaBRI and LIRMM. We will also present a
recently developed extension of that framework in Linear
Intuitionistic Logic that can be used to integrate many of the
discussed phenomena.

Dependent type semantics (DTS) is a proof-theoretic, compositional framework of discourse semantics based on dependent type theory, extended with underspecified terms. In DTS, anaphora and presupposition triggers are represented by using underspecified terms, which are to be replaced by proof terms inhabiting the same type. This process corresponds to anaphora resolution and presupposition binding, and it has been predicted in previous literature that the type of each underspecified term can be calculated via type inference/checking of dependent type theory, which amounts to the calculation of presupposition projection. However, the formulation of type inference/checking for DTS has been left as an open issue, which is not an obvious task, since type inference/checking in dependent type theory is known to be undecidable. In this paper, we formalized a set of rules for a type inference/checking algorithm for a decidable fragment of dependent type theory, which is an extension of the type inference/checking algorithm for Agda by Loh et al. We claim that this fragment is sufficient for representing (proof-theoretic) meaning of a broad range of natural language sentences. Moreover, we have implemented the proposed algorithm in Haskell programming language and demonstrate that it correctly calculates the projective contents of sentences involving presupposition filtering and global/local accommodations.

We present an approach that aims at integrating logical operators into semantic frames by employing hybrid logic. Frames have been developed as a format for the representation of conceptual and lexical knowledge. They are commonly presented as graphs, where nodes correspond to entities (individuals, events, etc.) and edges represent (functional or non-functional) relations between these entities. Semantic structures of this type allow one to capture lexical meaning in a fine-grained way but lack a natural way to integrate logical operators such as quantifiers. Our approach starts from the observation that modal logic is a powerful tool for describing relational structures and is hence suitable for characterizing frames. We use a hybrid logic extension of modal logic. In particular, we make use of the following elements that can occur in logical formulas: nominals, which allow the reference to specific nodes of the frame, and state variables with their associated quantifiers, which can express general properties of the models. Lexical items are then provided with logical expressions which specify the semantic properties that should hold for the corresponding frames. This grounds our approach to quantification in frame semantics. Finally, we devise a compositional syntax-semantics interface in a type-theoretic setting and give an illustration of how classical examples of quantifier scope can interact with path equalities introduced by the lexical frames.

We discuss nominalizations in Portuguese formed by the suffix -ura, as pintura (painting), magistratura (magistracy) and gordura (fat). We have done a corpus-based description of the behavior of these nominal forms and proposed a type ontology to categorize them. We have parted from all the nouns formed by -ura which are present in OpenWordNet-PT and checked them in three famous Portuguese dictionaries (Porto Dictionary, Caldas Aulete Dictionary and Houaiss Dictionary). Then we analyzed their use in context in Corpus Brasileiro, a corpus which has more than 1 billion words extracted from various textual genders. In order to offer a rich description, we also tested all words formed by -ura in co-predication contexts with at least three native speakers of Brazilian Portuguese with no knowledge of linguistic study theories to check if their types could be co-predicated. Although our main goal was to produce a corpus-based description on those nouns, we have found few possible generalizations considering the type-structure of -ura forms. More than that, our tests on co-predication show that may be the frequency of use of a given word has a special role on the acceptability of co-predication between different senses of a nominalization.

This is a talk about the proof assistant Agda. More specifically, about using Agda to prove things and all the advantages of doing so. Those advantages, as we shall explain, are that you: a) have a machine-checked implementation of your theory; b) can compute with your proofs; and c) can typeset Agda proofs so that the proofs you write are the proofs you publish. The first half of this talk is going to be spent introducing the Agda language, programming in Agda and writing papers in literate Agda. The second half is going to be spend giving an example of this process, by formalising the Lambek-Grishin calculus (LG) in Agda, discussing a proof for cut-elimination in LG, and outlining a CPS translation from LG into Agda. We will finish up by providing several example analyses of sentences. [

Dependent Type Semantics (DTS) is a framework of natural language semantics based on dependent type theory. In contrast to traditional model-theoretic semantics, DTS is a proof-theoretic semantics where entailment relations are characterized as provability relations between semantic representations. Two distinctive features of DTS, as compared to other type-theoretical frameworks, are that (i) it is augmented with underspecified terms so as to provide a unified analysis of entailment, anaphora and presupposition from an inferential/computational perspective; and (ii) it gives a fully compositional account of inferences involving anaphora. In this paper, we present an analysis of entailment and presupposition associated with factive verbs within the framework of DTS. Factive attitude verbs such as "know" are distinguished from non-factive attitude verbs such as "believe" in that they introduce presuppositional inferences. We propose different forms of semantic representations for factive verbs and non-factive verbs: we analyze factive verbs as predicates taking a proof term as argument, and non-factive verbs as predicates taking a proposition in the sense of dependent type theory. Our theory also accounts for inferential properties of factive and non-factive verbs taking NP-complements: for example, "S believes the hypothesis that P" implies "S believes that P", whereas "S knows the hypothesis that P" does not imply "S knows that P".

Robin
Cooper (University of Gothenburg, CoChair),

Christian
Retoré (Université de Montpellier, &
LIRMM CoChair)

Alexandra
Arapinis (CNR, Trento)

Nicholas
Asher (CNRS, Toulouse)

Christian
Bassac (Université Lyon II)

Stergios
Chatzikyriakidis (CNRS et LRIMM,
Montpellier)

Shalom
Lappin (King’s College, London)

Zhaohui
Luo (Royal Holloway, University of London)

Chiara Melloni
(CNR, Verona)

Bruno
Mery (Université de Bordeaux)

Richard
Moot (CNRS, Bordeaux)

Glyn
Morrill (Universitat Polytècnica de
Catalunya, Barcelona)

Larry
Moss (Indiana University, Bloomington)

Reinhard
Muskens (Universiteit Tilburg)

Livy Real (IBM
Research, Saõ Paolo)

- Asher, N. (2011), Lexical Meaning in Context: A Web of Words, Cambridge University Press.
- Asher, N. & Luo, Z. (2012), Formalisation of coercions in lexical semantics, in 'Sinn und Bedeutung 17'.
- Asher, N. & Pustejovsky, J. (2005), 'Word Meaning and Commonsense Metaphysics', in course materials for Type Selection and the Semantics of Local Context, ESSLLI 2005.
- Bassac, C.; Mery, B. & Retoré, C. (2010), 'Towards a type-theoretical account of lexical semantics', Journal of Logic, Language and Information 19(2), 229--245.
- Chatzikyriakidis, S. & Luo, Z. (2013), Adjectives in a Modern Type-Theoretical Setting In Morrill, G. & Nederhof, M.-J. Formal Grammar, LNCS 8036 pp. 159-174.
- Chatzikyriakidis, S. & Luo Z. (2014). Natural Language Reasoning Using Proof Technology: Rich Typing and Beyond. Proceedings of EACL2014
- Cooper, R. (2011), Copredication, Quantfication and Frames, in S. Pogodalla & J.-Ph. Prost, ed., 'Logical Aspects of Computational Linguistics: 6th International Conference, LACL 2011', Springer, pp. 64--79.
- Cooper, R.; Dobnik S.; Lappin, S.; Larsson, S. (2014) A Probabilistic Rich Type Theory for Semantic Interpretation. ACL Workshop on Type Theory and Natural Language Semantics, Göteborg, 2014.
- Cooper, R. (2010), Type Theory and Semantics in Flux, In Kempson, R.; Asher, N. & Fernando, T. Handbook of Philosophy of linguistics. pp. 271-323.
- Jezek, E. & Melloni, Ch. (2011) Nominals, polysemy and copredication, Journal of cognitive sciences 12 pp. 1-31.
- Moot, R.; Prévot, L. & Retoré, C. (2011) A discursive analysis of itineraries in an historical and regional corpus of travels: syntax, semantics, and pragmatics in a unified type theoretical framework In Contraints in Discourse
- Ranta, A. (1994), Type-Theoretical Grammar, Clarendon Press, Oxford.
- Real L. & Retoré, C. (2013), Deverbal semantics and the Montagovian generative lexicon. Journal of Logic Language and Information. 2014 DOI: 10.1007/s10849-014-9187-y
- Retoré,
C. The Montagovian Generative Lexicon ΛTyn: a
Type Theoretical Framework for Natural Language
Semantics in Ralph Matthes and Aleksy
Schubert (eds) 19th International Conference on
Types for Proofs and Programs (TYPES 2013)
LIPICS vol 26 pp. 202--229. Freely
available here.