From Dependent Types to Natural Language Semantics

In this talk, I will provide a comprehensive overview of Dependent Type Semantics (DTS), a proof-theoretic approach to natural language semantics based on dependent type theory. DTS marks a departure from the traditional model-theoretic semantic frameworks that have long been the standard, such as Montagovian intensional logic, discourse representation theory, and dynamic semantics.

The key distinguishing feature of DTS is its ability to unify analyses of linguistic phenomena such as anaphora and presupposition through the process of type checking and proof search. This is consistent with the “presupposition is anaphora” paradigm that is widely discussed and analyzed in semantic studies.

DTS computes the meaning of a given sentence through the principle of compositionality, coupled with the mechanism called “unspecified types,” which correspond to open proofs in proof assistants. This establishes a new correspondence between the meaning of natural language and type theory, shedding new light on both fields.

I will also reflect on the extensive research and developments over the past decade. This will shed light on the future prospects of DTS and provide insights into its potential applications in computational linguistics.

1. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
From Dependent Types
to Natural Language Semantics
Daisuke Bekki
Ochanomizu University
Faculty of Core Research
https://daisukebekki.github.io/
A plenary talk at Logic Colloquim 2024
25 June (Tue)
1 / 96

2. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Dependent Type Semantics (DTS) (Bekki 2014;
Bekki and Mineshima 2017; Bekki 2021)
IA framework of natural language semantics
IUnied approach to (general) inferences and
anaphora/presupposition resolution in terms oftype checking
andproof search
Main features:
1.Proof-theoretic semantics:
From model theory (denotations and models) to proof theory
(proofs and contexts)
2.Anaphora/Presuppositions: A proof-theoretic alternative to
Dynamic Semantics (DRT, DPL, etc.)
3.Compositionality: Syntax-semantics interface via categorial
grammars (e.g. CCG, TLG, ACG, etc)
4.Implementation: Applications to Natural Language
Processing.
https://github.com/DaisukeBekki/lightblue/
2 / 96

3. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Dependent Types
3 / 96

4. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Per Martin-Lof
Martin-Lof (1984) \Intuitionistic type theory"
4 / 96

5. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
What are-types
-type is a type ofbredfunctions.
Simple function space Fibredfunction space
5 / 96

6. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
What are-types
-type is a type ofbredproducts.
Simple product space Fibredproduct space
6 / 96

7. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Notations
DTS notation Standard notationx62fv(B)x2fv(B)
(x:A)!B(x:A)B A !B (8x:A)B(x:A)B
or

x:A
B
(x:A)B A ^B (9x:A)B
Scope of the variable in-types:(x:A)!
B
Scope of the variable in-types:

x:A
B

7 / 96

8. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
-type F/I/E rules
A:s1
x:A
i
.
.
.
.
B:s2
(x:A)!B:s2
(F);i
where(s1;s2)2
8
<
:
(type;type);
(type;kind);
(kind;kind)
9
=
;
:
A:type
x:A
i
.
.
.
.
M:B
x:M:x:A)!B
(I);i
M:x:A)!B :A
MN:B[N=x]
(E)
8 / 96

9. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
-type F/I/E rules
A:type
x:A
i
.
.
.
.
B:type
(x:A)B:type
(F);i
M:A :B[M=x]
(M; N) : x:A)B
(I)
M:x:A)B
1(M) :A
(E)
M:x:A)B
2(M) :B[1(M)=x]
(E)
9 / 96

10. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Rules of DTS
Rules from Martin-Lof Type Theory
IAxioms and Structural rules
I-type (Dependent function type)
I-type (Dependent product type)
IIntensional equality type
IDisjoint union type
IEnumeration type
INatural number type
New rule in DTS
I@ (the `asperand' operator)
IAnaphora and presupposition triggers
(linguistically speaking)
IOpen proofs (logically speaking)
10 / 96

11. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Conjunction, Implication, and Negation
Denition

A
B

def
(x:A)B where x =2fv(B):
A!B
def
(x:A)!B where x =2fv(B):
:A
def
(x:A)! ?
11 / 96

12. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Anaphora in Natural Language
12 / 96

13. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
A theory of anaphora
IAnaphora representable by a constant symbol:
IDeictic use:
(1)(Pointing at John)
He
was born in Detroit.
bornIn(
j;d)
ICoreference:
(2)
John
loves a girl who hates
him
.
9x(girl(x)^love(
j; x)^hate(x;j))
IAnaphora representable by a variable
IBound variable anaphora:
(3)
Every boy
loves
his
father.
8x
(boy(x)!love(x;fatherOf(
x)))
13 / 96

14. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
A theory of anaphora
IAnaphora not representable by FoL:
IE-type anaphora:
(4)
A man
entered into the park.
He
whistled.
IDonkey anaphora:
(5)
a donkeybeatsit
.
(6)
a donkey
, he beats
it
.
IAnaphora not representable by FoL nor dynamic semantics:
ISyllogistic anaphora:
(7)
a present. Some girl openedit
.
IDisjunctive antecedent:
(8)
a horse or a pony
, she waves to
it
.
14 / 96

15. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Geach (1962)
For the donkey sentences (9), a rst-order formula (10), whose
truth condition is the same as those of (9), is a candidate of its
semantic representation (SR).(We only discuss itsstrong readinghere. See Tanaka (2021)
for itsweak reading.)
(9)
[a donkey]
1
beats it1.
b.
1
owns
[a donkey]
2
, he1beats it2.
(10)8x(farmer(x)!
8y(donkey(y)^own(x; y)!
beat(x; y)))
But the translation from the sentence (9) to (10) is not
straightforward since i) the indenite noun phrasea donkeyis
translated into a universal quantier in (10) instead of an
existential quantier, and ii) the syntactic structure of (10) does
not corresponds to that of (9).
15 / 96

16. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Geach (1962)
(9)
1
beats
it1.
b.
1
owns [a donkey]
2
, he1beats
it2.
The syntactic parallel of (9) is, rather, the SR (11), in which the
indenite noun phrase is translated into an existential
quantication.
(11)8x(farmer(x)^ 9y(donkey(y)^own(x; y))!
beat(x;
y))
However, (11) does not represent the truth condition of (9)
correctly since the variableyinbeat(x; y)fails to be bound by9.
Therefore, neither (10) nor (11) qualies as the SR of (9).
16 / 96

17. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Various approaches in discourse semantics
Dynamic Semantics
IDiscourse Representation Theory (DRT): Kamp (1981),
Kamp and Reyle (1993)
IDynamic Predicate Logic (DPL): Groenendijk and Stokhof
(1991)
IDynamic Plural Predicate Logic (DPPL): van den Berg
(1996), Sudo (2012)
Type-theoretical Semantics
IAnalysis of donkey anaphora: Sundholm (1986))
IType Theoretical Grammar (TTG): Ranta (1994)
IType Theory with Record (TTR): Cooper (2005)
IModern Type Theory: Luo (1997, 1999, 2010, 2012), Asher
and Luo (2012), Chatzikyriakidis (2014)
IDependent Type Semantics (DTS): Bekki (2014), Bekki and
Mineshima (2017)
17 / 96

18. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Sundholm (1986)
(9a) beats
it
.
0
B
B
B
B
B
@
u:
2
6
6
6
6
6
4
x:entity
2
6
6
6
4
farmer(x)
2
6
4
v:
"
y:entitydonkey(y)
#
own(x; 1v)
3
7
5
3
7
7
7
5
3
7
7
7
7
7
5
1
C
C
C
C
C
A
!
beat(1u;1122u)
Note:(x:A)!Bis a type for functions fromAtoB[x].
18 / 96

19. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
From TTG to DTS: Compositionality
Q:
representations from arbitrary sentences?
A:
Q:
words like pronouns?
0
B
B
B
B
B
@
u:
2
6
6
6
6
6
4
x:entity
2
6
6
6
4
farmer(x)
2
6
4
v:
"
y:entity
donkey(y)
#
own(x; 1v)
3
7
5
3
7
7
7
5
3
7
7
7
7
7
5
1
C
C
C
C
C
A
!
beat(1u;1122u)
19 / 96

20. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
From TTG to DTS: Compositionality
Q:
representations from arbitrary sentences?
A:
Q:
words like pronouns?
A: underspecied types.
Q:
type?
A: type checking.
20 / 96

21. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Dependent Type Semantics (DTS)
21 / 96

22. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Underspecied types
DTS
= DTT +
underspecied types
Denition (@-rule)
A:typeM:A [M=x] :type

x@A
B

:type
(@)
I@-rule states that the well-formedness of(x@A)B
requires:
IAis a well-formed type
Ithe inhabitance of a proof (let it beM) ofA, checking of
which launches a proof search
IB[M=x]is a well-formed type
This means that the truth ofAispresupposed.
22 / 96

23. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
A model of natural language understanding via CCG
and DTS
A sentence
. . .
A sentence
+ +
CCG Parsing . . . CCG Parsing
+ +
An underspecied SRsinDTS
. . .
An underspecied SRsinDTS
+ +
Discoruse Parsing
+
An underspecied discourse SRs
in
DTS
+
Type checking+Proof search
+
A proof diagram of the well-formedness of an SRsin DTT
+
Inference in DTT
23 / 96

24. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Lexical items in CCG style
Surface form Syntactic category Semantic representation
every
(
T =(TnNP)=N
Tn(T =NP)=N
n:p:~x:

u:

x:entity
n(x)

!p(1u)~x
a;some
(
T =(TnNP)=N
Tn(T =NP)=N
n:p:~x:
2
4
u:

x:entity
n(x)

p(1u)~x
3
5
if
(
S=S=S
SnS=S
p:q:(u:p)!q
who/whom
(
NnN=(SnNP)
NnN=(S=NP)
p:n:x:

nx
px

farmer N farmer
donkey N donkey
owns SnNP=NP own
beats SnNP=NP beat
he/him
(
T =(TnNP)nom
Tn(T =NP)acc
p:~x:
2
4
u@

x:entity
male(x)

p(1u)~x
3
5
it
(
T =(TnNP)nom
Tn(T =NP)acc
p:~x:
2
4
u@

x:entity
:human(x)

p(1u)~x
3
5
the
(
T =(TnNP)=Nnom
T =(TnNP)=Nacc
n:p:~x:
2
4
u@

x:entity
n(x)

p(1u)~x
3
5
24 / 96

25. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Syntactic Structure
Every
T =(TnNP)=N
farmer
N
who
NnN=(SnNP)
owns
SnNP=NP
a
Tn(T =NP)=N
donkey
N
Tn(T =NP)
SnNPn(SnNP=NP)
8E
SnNP
<
NnN
>
N
<
T =(TnNP)
>
S=(SnNP)
8E
beat
SnNP=NP
it
Tn(T =NP)
SnNPn(SnNP=NP)
8E
SnNP
>
S
>
S
CC
25 / 96

26. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Semantic Composition (1/2)
farmer
farmer
who
p:n:x:

n(x)
p(x)

owns
y:x:
own(x; y)
a
n:p:
2
4
v:

y:entity
n(y)

p(1v)
3
5
donkey
donkey
p:
2
4
v:

y:entity
donkey(y)

p(1v)
3
5
>
x:
2
4
v:

y:entity
donkey(y)

own(x; 1v)
3
5
<
n:x:
2
6
6
4
n(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
5
>
x:
2
6
6
4
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
5
<
26 / 96

27. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Semantic Composition (2/2)
Every
n:p:

u:

x:entity
n(x)

!p(1u)
farmer who owns a donkey
x:
2
6
6
4
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
5
p:
0
B
B
B
B
@
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
C
C
C
C
A
!p(1u)
>
beat
y:x:
beat(x; y)
it
p:x:
2
6
4
w@

z:entity
:human(z)

p(1w)x
3
7
5
x:
2
6
4
w@

z:entity
:human(z)

beat(x; 1w)
3
7
5
>
0
B
B
B
B
@
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
C
C
C
C
A
!
2
6
4
w@

z:entity
:human(z)

beat(1u; 1w)
3
7
5
>
27 / 96

28. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Semantic Felicity Condition
(=Type Checking)
.
.
.
.
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
:type
.
.
.
.

z:entity
:human(z)

:type
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
.
.
.
.
? :

z:entity
:human(z)

.
.
.
.
(beat(1u; 1w))[?=w] :type
2
6
4
w@

z:entity
:human(z)

beat(1u; 1w)
3
7
5:type
(@)
0
B
B
B
B
@
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
C
C
C
C
A
!
2
6
4
w@

z:entity
:human(z)

beat(1u; 1w)
3
7
5:type
(I);1
28 / 96

29. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Anaphora Resolusion (=Proof
Search)
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
2u:
2
6
6
4
farmer(x)
v:

y:entity
donkey(y)

own(1u; 1v)
3
7
7
5
(E)
22u:
2
4
v:

y:entity
donkey(y)

own(1u; 1v)
3
5
(E)
122u:

y:entity
donkey(y)
(E)
1122u:entity
(E)
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
2u:
2
6
6
4
farmer(x)
v:

y:entity
donkey(y)

own(1u; 1v)
3
7
7
5
(E)
22u:
2
4
v:

y:entity
donkey(y)

own(1u; 1v)
3
5
(E)
122u:

y:entity
donkey(y)
(E)
d:

u:

x:entity
donkey(x)

! :human(1u)
(CON)
d(122u) ::human(1122u)
(E)
(1122u; d(122u)):

z:entity
:human(z)
(I)
29 / 96

30. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Donkey anaphora: Semantic Felicity Condition
(=Type Checking) continued
.
.
.
.
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
:type
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
.
.
.
.
beat(1u; 1122u) :type
0
B
B
B
B
@
u:
2
6
6
6
6
4
x:entity
farmer(x)
v:

y:entity
donkey(y)

own(x; 1v)
3
7
7
7
7
5
1
C
C
C
C
A
!beat(1u; 1122u) :type
(beat(1u; 1w))[
(1122u; d(122u))=w] :type
beat(1u; 1122u)
(I);1
30 / 96

31. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Notes on donkey anaphora
IThe same analysis applies to theimplicationaldonkey
sentence:
(12)
1
owns [a donkey]
2
, he1beats it2.
IThis analysis only predicts thestrong readingfor donkey
sentences. For deriving both the strong readings and theweak
readings, we need to rene the semantic representations for
quanticational expressions: See Tanaka (2021).
IThe rened analysis also explains why the anaphoric link to
theparametrized sum individual(Krifka, 1996) is allowed
(Tanaka, 2021).
(13)
1
who owns [a donkey]
2
loves its2tail.
But they1beat it2.
31 / 96

32. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
PresuppositionJoint work with Koji Mineshima
32 / 96

33. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
What is Presupposition? | Background content
(14)
Presupposition:Someone broke my iPhone.
Ithe background content
Iits truth is usually taken for granted
Assertion:John was the one who did it.
Ithe foreground content
Ithe main point of an utterance
33 / 96

34. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Two puzzules of Presupposition { (i) Projection
(14)
(15) presupposes(15))
(15) projects out of all the embedded contexts in (16a{e).
(16) negation
b. modal
c.
it. the antecedent of a conditional
d. question
e.
hypothetical assumption
34 / 96

35. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
The Case of Entailment
(17)
(18) entails(18))
(18) does not survive in the contexts (19a{e).
(19) negation
b. modal
c.
the antecedent of a conditional
d. question
e.
hypothetical assumption
35 / 96

36. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
The Case of Entailment
(17)
american(john)^pianist(john)
(19)
:(american(j)^pianist(j))
b.
3(american(j)^pianist(j))
c.
american(j)^pianist(j)!skillful(j)
Standard semantics correctly predicts these patterns:
I(17)`american(john)
I(19a)6`american(john)
I(19b)6`american(john)
I(19c)6`american(john)
36 / 96

37. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
The Case of Presupposition
(14) SR1
(16) :SR1
b. 3SR1
c.
SR1!
What SR accounts for the following inference patterns?
ISR19x(broke(x;myiphone))
I:SR19x(broke(x;myiphone))
I3SR19x(broke(x;myiphone))
ISR1!A9x(broke(x;myiphone))
Q: Can \" be dened as a standard consequence relation "`"?
A: No. If that were the case, then9x(broke(x;myiphone))was
a tautology (under the classical setting).
37 / 96

38. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Two puzzules of Presupposition { (ii) Filteration
(20) presupposes that someone broke the window, but the
conditional in (21) does not inherit this presupposition.
(20)
(
Someone broke the window
(21)
6
(
Someone broke the window
Similarly for (22) and (23).
(22)
(
France has a king.
(23)
6
(
France has a king.
A presupposition islteredwhen it occurs in certain contexts.
38 / 96

39. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Presupposition triggers
(24) The elevatorin this building is clean.Description
b.
(25) John's sisteris happy. Possessive
b.
(26) regretsthat he lied to Mary. Factive
b.
(27) stoppedbeating his wife. Aspectual
b.
(28) managedto nd the book. Implicative
b.
39 / 96

40. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Presupposition triggers
(29) againtoday. Iterative
b.
(30) It wasSamwhobroke the window. Cleft
b.
(31) WhatJohn brokewashis typewriter.Pseudo-cleft
b.
(32) Fis leaving,too. (Focus onPat) Additive
b.
For classical examples of presupposition triggers, see Levinson
(1983), Soames (1989), Geurts (1999), and Beaver (2001), among
others.
40 / 96

41. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
\Presupposition Is Anaphora"
hypothesis
41 / 96

42. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
\Presupposition Is Anaphora" hypothesis
There are striking parallels between anaphoric expressions and
presupposition triggers. (van der Sandt, 1992; Geurts, 1999)
Presupposition ltering:
(33) John's childrenare wise.
b. John's childrenare wise.
(34) it wasJohnwhobroke it.
b. it wasJohnwhobroke it.
Compare (33) and (34) with the paradigm examples of anaphora
resolution.
Anaphora resolution:
(35) it.
b. it.
42 / 96

43. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
DTS on Projection
IThe projection inferences of presupposition can be naturally
accounted for using the framework of DTS.
INote that negation is dened to be an implication of the form
:AA! ?.the formation rule for negation can be
derived as on the right:
IAccording to the formation rule(:F)for negation, the
propositionAand its negation:Ahave the same
presupposition.
Example:
It is not the case that the king of France is bald.
SR :
2
6
4
u@

x:entity
king(x;fr)

bold(1u)
3
7
5
43 / 96

44. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Projection: Syntax
It is not
the case that
S=S
the
S=(SnNP)=N
king
N=PPof
of
PPof=NP
France
NP
PPof
>
N
<
S=(SnNP)
>
is
SnNP=(SnNP)
bald
SnNP
SnNP
>
S
>
S
>
44 / 96

45. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Projection: Semantic Composition
It is not
the case that
p::p
the
n:p:
2
6
4
u@

x:entity
n(x)

p(1u)
3
7
5
king
z:x:
kingOf(x; z)
of
id
France
fr
fr
>
x:kingOf(x;fr)
<
p:
2
6
4
u@

x:entity
kingOf(x;fr)

p(1u)
3
7
5
>
is
id
bald
bald
bald
>
2
6
4
u@

x:entity
kingOf(x;fr)

bald(1u)
3
7
5
>
:
2
6
4
u@

x:entity
kingOf(x;fr)

bald(1u)
3
7
5
>
45 / 96

46. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Projection: Type checking
.
.
.
.

x:entity
kingOf(x;fr)

?
:

x:entity
kingOf(x;fr)

:bald(1u)[?
=u] :type
2
6
4
u@

x:entity
kingOf(x;fr)

:bald(1u)
3
7
5:type
(@)
?:type
(fgF)
:
2
6
4
u@

x:entity
kingOf(x;fr)

:bald(1u)
3
7
5:type
(F)
IIn order for the sentence \The king of France is bald" to be
well-formed, the contextmust be such that the following
type inhabits a proof (namely, there exists a king of France).
`? :

x:entity
kingOf(x;fr)

46 / 96

47. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
DTS on Projection
IThe same inference is triggered for the antecedent of a
conditional sentence like (36):
(36)
.
.
.
.
2
6
4
u:

x:entity
kingOf(x;fr)

wise(1u)
3
7
5:type
.
.
.
.
happy(people) :type
2
6
4
u:

x:entity
kingOf(x;fr)

wise(1u)
3
7
5!happy(people) :type
(F)
47 / 96

48. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
DTS on Filtering
IThe present account can explain the ltering inference
without further stipulation.
ITake a look at the case of a conditional sentence:
(37) the king of Franceis wise.
SR

u:

x:entity
kingOf(x;fr)

!
2
6
4
v@

x:entity
kingOf(x;fr)

wise(1v)
3
7
5
48 / 96

49. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Filtering: Type checking
.
.
.
.

x:entity
kingOf(x;fr)

:type
.
.
.
.

x:entity
kingOf(x;fr)

:type
u:

x:entity
kingOf(x;fr)
1
.
.
.
.
?
:

x:entity
kingOf(x;fr)

.
.
.
.
wise(1v)[?
=v]
2
6
4
v@

x:entity
kingOf(x;fr)

wise(1v)
3
7
5
(@)

u:

x:entity
kingOf(x;fr)

!
2
6
4
v@

x:entity
kingOf(x;fr)

wise(1v)
3
7
5:type
(F);1
49 / 96

50. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
DTS on Filtering
.
.
.
.

x:entity
kingOf(x;fr)

:type
wise:entity!type
(CON)
u:

x:entity
kingOf(x;fr)
1
1u:entity
(E)
wise(1u) :type
(E)

u:

x:entity
kingOf(x;fr)

!wise(1u) :type
(F);1
IType checking algorithm returns a fully-specied semantic
representation.
IPresupposition ltering is performed via exactly the same
process as anaphora resolution.
50 / 96

51. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Summary and History
51 / 96

52. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
A Unied, Compositional Theory of Projective
Meaning
IDTS provides a unied analysis for (general) inferences and
anaphora resolusion mechanisms (at least) for:
IDeictic use and coreference
IBound variable anaphora (BVA)
IE-type anaphora
IDonkey anaphora
IBridging anaphora
ISyllogistic anaphora
IDisjunctive antecedents
52 / 96

53. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
A Unied, Compositional Theory of Projective
Meaning
IThe background theory for DTS is an extention of DTT with
underspecied typesandthe@-rule
.
ILexical items of anaphoric expressions and presupposition
triggers are represented by using underspecied types.
IContext retrieval in DTS reduces to
type checking
.
IAnaphora resolution and presupposition binding in DTS
reduces to
proof search
.
I
Type checker
translates a proof diagram of DTS into a proof
diagram of DTT, by which an SR in DTT is obtained with all
anaphora resolved.
53 / 96

54. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Natural language semantics via dependent types:
Early works
IDonkey anaphora: Sundholm (1986)
ITranslation from DRS to dependent type representations: Ahn
and Kolb (1990)
ISummation: Fox (1994a,b)
IRanta's TTG (Relative and Implicational Donkey Sentences,
Branching Quantiers, Intensionality, Tense): Ranta (1994)
ITranslation from Montague Grammar to dependent type
representations: Davila-Perez (1995)
IPresupposition Binding and Accommodation, Bridging:
Krahmer and Piwek (1999), Piwek and Krahmer (2000)
54 / 96

55. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Natural language semantics via dependent types:
The second generation
IType Theory with Record (TTR): Cooper (2005)
IModern Type Theory: Luo (1997, 1999, 2010, 2012), Asher
and Luo (2012), Chatzikyriakidis (2014)
ISemantics with Dependent Types: Grudzinska and
Zawadowski (2014; 2017)
IDynamic Categorial Grammar: Martin and Pollard (2014)
IDependent Type Semantics (DTS): Bekki (2014), Bekki
and Mineshima (2017)
55 / 96

56. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Semantic Analyses by DTS
IGeneralized Quantiers: Tanaka (2014)
IHonorication: Watanabe et al. (2014)
IConventional Implicature: Bekki and McCready (2015),
Matsuoka et al. (2023)
IFactive Presuppositions: Tanaka et al. (2015)
IDependent Plural Anaphora: Tanaka et al. (2017)
IPaycheck sentences: Tanaka et al. (2018)
ICoercion and Metaphor: Kinoshita et al. (2017, 2018)
IQuestions: Watanabe et al. (2019), Funakura (2022)
IComparision with DRT: Yana et al. (2019)
IThe proviso problem: Yana et al. (2021)
IWeak Crossover: Bekki (2023)
56 / 96

57. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Computational Aspects of DTS
IType Checker for (the fragment of) DTS: Bekki and Sato
(2015)
IDevelopment of an automated theorem prover (for the
fragment of) DTS: Daido and Bekki (2020)
IIntegrating Deep Neural Network with DTS: Bekki et al.
(2023, 2022)
57 / 96

58. Dependent TypesAnaphoraDTS on AnaphoraPresuppositionDTS on Presupp.Summary
Thank you!
58 / 96

59. Type SystemType Check/Inference Algorithm
Appendix I: Type System in DTS
59 / 96

60. Type SystemType Check/Inference Algorithm
Axioms and Structural Rules
x:A
(VAR)
c:A
(CON)
where(c:A)2:
type:kind
(typeF)
M:A :B
M:A
(WK)
M:A
M:B
(CONV)
where A=B:
60 / 96

61. Type SystemType Check/Inference Algorithm
-type F/I/E rules
A:s1
x:A
i
.
.
.
.
B:s2
(x:A)!B:s2
(F);i
where(s1;s2)2
8
<
:
(type;type);
(type;kind);
(kind;kind)
9
=
;
:
A:type
x:A
i
.
.
.
.
M:B
x:M:x:A)!B
(I);i
M:x:A)!B :A
MN:B[N=x]
(E)
61 / 96

62. Type SystemType Check/Inference Algorithm
-type F/I/E rules
A:type
x:A
i
.
.
.
.
B:type
(x:A)B:type
(F);i
M:A :B[M=x]
(M; N) : x:A)B
(I)
M:x:A)B
1(M) :A
(E)
M:x:A)B
2(M) :B[1(M)=x]
(E)
62 / 96

63. Type SystemType Check/Inference Algorithm
Disjoint Union Type F/I/E rules
A:typeB:type
A+B:type
(+F)
M:A
1(M) :A+B
(+I)
N:B
2(N) :A+B
(+I)
M:A+B :A+B)!typeN1:x:A)!P(1(x))N2:x:B)!P(2(x))
unpack
P
M
(N1; N2) :P(M)
(+E);i
63 / 96

64. Type SystemType Check/Inference Algorithm
Natural Number Type F/I/E rules
N:type
(NF)
0:N
(NI)
n:N
s(n) :N
(NI)
n:NP:N!typee:P(0)f:k:N)!P(k)!P(s(k))
natrec
P
n
(e; f) :P(n)
(NE)
64 / 96

65. Type SystemType Check/Inference Algorithm
Enumeration Type F/I/E rules
fa1; : : : ; ang:type
(fgF)
ai:fa1; : : : ; ang
(fgI)
M:fa1; : : : ; angP:fa1; : : : ; ang !typeN1:P(a1): : : n:P(an)
case
P
M
(N1; : : : ; Nn) :P(M)
(fgE)
65 / 96

66. Type SystemType Check/Inference Algorithm
Intensional Equality Type F/I/E rules
A:typeM:A :A
M=AN:type
(=F)
M:A
reA(M) :M=AM
(=I)
E:M=AN :x:A)!(y:A)!(x=Ay)!typeR:x:A)!P xx(reA(x))
idpeel
P
E
(R) :P MNE
(=E)
66 / 96

67. Type SystemType Check/Inference Algorithm
@-rule
A:typeM:A [M=x] :type

x@A
B

:type
(@)
67 / 96

68. Type SystemType Check/Inference Algorithm
Appendix II: Type Check/Inference
Algorithm
68 / 96

69. Type SystemType Check/Inference Algorithm
Inferable terms (1/2)
The collection ofinferable terms(notationM") and the
collection ofcheckable terms(notationM#) are simultaneously
dened by the following BNF notations, wherev; v
0
are values.
M"::=x variable
jc constant symbol
jtype the type of types
j(x:M#)!M# dependent functional type
jM"M# functional application
j(x:M#)M# dependent sum type
ji(M") projections
jM#+M# disjoint union types
junpack
M#
M"
(M#; M#)unpack
69 / 96

70. Type SystemType Check/Inference Algorithm
Inferable terms (2/2)
j ? bottom type
j > top type
j() unit
jM#=M#
M# Intensional Equality types
jreM#
(M#) reexive
jidpeel
M#
M"
(M#) idpeel
jN natural number types
j0 zero
js(M#) successor
jnatrec
M#
M"
(M#; M#)mathematical induction
jM#:M# annotated term
j

x@M#
M#

underspecied type
70 / 96

71. Type SystemType Check/Inference Algorithm
Checkable terms
M#::=M" inferable terms
jx:M# lambda abstraction
j(M#; M#)pair
ji(M#) injections
71 / 96

72. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Type inference of a UDTT is a transformation of a UDTT
judgment to a set of DTT proof diagrams, recursively dened by
the following set of rules.
Denition (Inferable Terms: Structural Rules)
J; x:A;`x: ?K=
(
x:A
0
.
.
.
.
A
0
:type
2J`A:typeK
)
J`c: ?K=

c:A
(CON)
`c:A

J`type: ?K=

`type:kind
(typeF)

72 / 96

73. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (-types)
J`(x:A)!B: ?K=
8
>
>
>
<
>
>
>
:

DA
A
0
:type
; x:A
0
DB
B
0
:type
(x:A
0
)!B
0
:type
(F)
DA2J`A:typeK
DB2J; x:A
0
`B:typeK
9
>
>
>
=
>
>
>
;
J`x:M: (x:A)!BK=
8
>
>
>
<
>
>
>
:

DA
A
0
:type
; x:A
0
DM
M
0
:B
0
x:M
0
: (x:A
0
)!B
0
(I)
DA2J`A:typeK
DM2J; x:A
0
`M:BK
9
>
>
>
=
>
>
>
;
J`MN: ?K=
8
>
>
>
>
>
<
>
>
>
>
>
:

DM
M
0
: (x:A)!B

DN
N
0
:A
M
0
N
0
:B[N
0
=x]
(E)
M
0
N
0
:B
0
(CONV)
DM2J`M: ?K
DN2J`N:AK
B[N
0
=x]B
0
9
>
>
>
>
>
=
>
>
>
>
>
;
73 / 96

74. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (-types)
s
`

x:A
B

: ?
{
=
8
>
>
>
>
<
>
>
>
>
:

DA
A
0
:type
; x:A
0
DB
B
0
:type

x:A
0
B
0

:type
(F)
DA2J`A:typeK
DB2J; x:A
0
`B:typeK
9
>
>
>
>
=
>
>
>
>
;
s
`(M; N) :

x:A
B
{
=
8
>
>
>
<
>
>
>
:

DM
M
0
:A
0

DN
N
0
:B
0
(M
0
; N
0
) :

x:A
0
B
0
(I)
DM2J`M:AK
B[M
0
=x]B
0
DN2J`N:B
0
K
9
>
>
>
=
>
>
>
;
J`1(M) : ?K=
8
>
>
>
>
>
<
>
>
>
>
>
:

DM
M
0
:

x:A
B

1(M
0
) :A
(E)
DM2J`M: ?K
9
>
>
>
>
>
=
>
>
>
>
>
;
J`2(M) : ?K=
8
>
>
>
>
>
>
>
<
>
>
>
>
>
>
>
:

DM
M
0
:

x:A
B

2(M
0
) :B[1M
0
=x]
(E)
2(M
0
) :B
0
(CONV)
DM2J`M: ?K
B[1M
0
=x]B
0
9
>
>
>
>
>
>
>
=
>
>
>
>
>
>
>
;
74 / 96

75. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Disjoint Union types)
J`A+B: ?K=
8
>
>
<
>
>
:

DA
A
0
:type

DB
B
0
:type
A
0
+B
0
:type
(+F)
DA2J`A:typeK
DB2J`B:typeK
9
>
>
=
>
>
;
J`1(M) :A+BK=
8
>
>
<
>
>
:

DM
M
0
:A
0
1(M
0
) :A
0
+B
(+I)
DM2J`M:AK
9
>
>
=
>
>
;
J`2(N) :A+BK=
8
>
>
<
>
>
:

DN
N
0
:B
0
2(N
0
) :A+B
0
(+I)
DN2J`N:BK
9
>
>
=
>
>
;
q
`unpack
P
L
(M; N) : ?
y
=
8
>
>
>
>
>
<
>
>
>
>
>
:

DL
L
0
:A+B

DP
P
0
:A+B)!type

DM
M
0
:x:A)!P
0
(1(x))

DN
N
0
:x:B)!P
0
(2(x))
unpack
P
L
0(M
0
; N
0
) :P
0
(L
0
)
(+E);i
unpack
P B
L
0(M
0
; N
0
) :PL
(CONV)














DL2J`L: ?K
DP2J`P: (A+B)!typeK
P
0
(L
0
)PL
P
0
(1(x))PM
P
0
(2(x))PN
DM2J`M: (x:A)!PMK
DN2J`N: (x:B)!PNK
9
>
>
>
>
>
>
>
>
=
>
>
>
>
>
>
>
>
;
75 / 96

76. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Enumeration types)
J` fa1; : : : ; ang: ?K=

fa1; : : : ; ang:type
(fgF)

J`ai: ?K=

ai:fa1; : : : ; ang
(fgI)

q
`case
P
M
(N1; : : : ; Nn) : ?
y
=
8
>
>
>
>
>
<
>
>
>
>
>
:

DM
M:fa1; : : : ; ang

DP
P:fa1; : : : ; ang !type

DP1
N1:P1
N1:P(a1)
(CONV)
: : :

DPn
Nn:Pn
Nn:P(an)
(CONV)
case
P
M
(N1; : : : ; Nn) :P(M)
(fgE)
case
P
M
(N1; : : : ; Nn) :PM
(CONV)













DM2J`M: ?K
DP2J`P:fa1; : : : ; ang !typeK
P(a1)P1
DP12J`N1:P1K
: : :
P(an)Pn
DPn2J`Nn:PnK
P(M)PM
9
>
>
>
>
>
>
>
=
>
>
>
>
>
>
>
;
76 / 96

77. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Intensional Equality types)
J`M=AN: ?K=
8
>
>
<
>
>
:

DA
A
0
:type

DM
M
0
:A
0

DN
N
0
:A
0
M
0
=A
0N
0
:type
(=F)
DA2J`A:typeK
DM2J`M:A
0
K
DN2J`N:A
0
K
9
>
>
=
>
>
;
J`reA(M) : ?K=
8
>
>
<
>
>
:

DA
A
0
:type

DM
M
0
:A
0
reA
0(M
0
) :M
0
=A
0M
0
(=I)
DA2J`A:typeK
DM2J`M:A
0
K
9
>
>
=
>
>
;
q
`idpeel
P
E
(R) : ?
y
=
8
>
>
>
<
>
>
>
:

DE
E
0
:M=AN

DP
P
0
:x:A)!(y:A)!(x=Ay)!type

DR
R
0
:x:A)!P
0
xx(reA(x))
idpeel
P
0
E
0(R
0
) :P
0
MNE
0
(=E)
idpeel
P
0
E
0(R
0
) :P
00
(CONV)








DE2J`E:K
DP2J`P:x:A)!(y:A)!(x=Ay)!typeK
DR2J`R:x:A)!P
0
xx(reA(x))K
P MNEP
00
9
>
>
=
>
>
;
77 / 96

78. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Natural Number types)
J`N: ?K=

N:type
(NF)

J`0:K=

0:N
(NI)

J`s(n) :K=
8
>
>
<
>
>
:

Dn
n:N
s(n) :N
(NI)
Dn2J`n:NK
9
>
>
=
>
>
;
q
`natrec
P
n
(e; f) :
y
=
8
>
>
>
>
>
<
>
>
>
>
>
:

Dn
n
0
:NP:N!typee:P(0)f:k:N)!P(k)!P(s(k))
natrec
P
n
(e; f) :P(n)
(NE)
natrec
P
n
(e; f) :Pn
(CONV)




Dn2J`n:NK
P(n)Pn

78 / 96

79. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Underspecied types)
s
`

x@A
B

: ?
{
=
8
>
>
>
>
>
>
>
>
>
<
>
>
>
>
>
>
>
>
>
:

DB
B
00
:type
.
.
.
.
A
0
:type
2J`A:typeK
.
.
.
.
M:A
0
2J`? :A
0
K
B[M=x]B
0
DB2J`B
0
:typeK
9
>
>
>
>
>
>
>
>
>
=
>
>
>
>
>
>
>
>
>
;
79 / 96

80. Type SystemType Check/Inference Algorithm
Type Checking/Inference Algorithm
Denition (Checkable Terms)
J`M:AK=
8
<
:

DM
M:A
0
DM2J`M: ?K
A=A
0
9
=
;
where Minferable:
80 / 96

81. Type SystemType Check/Inference Algorithm
-reduction Rules
Mx:v v[N=x]v
0
MNv
0
()
M(v1; v2)
iMvi
()
xx
(VAR=)
cc
(CON=)
typetype
(type=)
kindkind
(kind=)
81 / 96

82. Type SystemType Check/Inference Algorithm
-reduction Rules
Mv Nv
0
(x:M)!N(x:v)!v
0
(=)
Mv
x:Mx:v
(=)
Mn Nv
MNnv
(APP=)
Mv Nv
0

x:M
N



x:v
v
0
(=) Mv Nv
0
(M; N)(v; v
0
)
(PAIR=)
Mn
iMin
(PROJ=)
()()
(()=)
>>
(>=)
??
(?=)
82 / 96

83. Type SystemType Check/Inference Algorithm
Reference
Ahn, R. and H.-P. Kolb. (1990) \Discourse Representation meets
Constructive Mathematics", In: L. Kalman and L. Polos (eds.):
Papers from the Second Symposium on Logic and Language.
Akademiai Kiado.
Asher, N. and Z. Luo. (2012) \Formalisation of coercions in lexical
semantics", In the Proceedings ofSinn und Bedeutung 17.
pp.63{80.
Beaver, D. I. (2001)Presupposition and Assertion in Dynamic
Semantics, Studies in Logic, Language and Information. CSLI
Publications & FoLLI.
83 / 96

84. Type SystemType Check/Inference Algorithm
Reference
Bekki, D. (2014) \Representing Anaphora with Dependent Types",
In the Proceedings of N. Asher and S. V. Soloviev (eds.):
Logical Aspects of Computational Linguistics (8th international
conference, LACL2014, Toulouse, France, June 2014
Proceedings), LNCS 8535. pp.14{29, Springer, Heiderburg.
Bekki, D. (2023) \A Proof-theoretic Analysis of Weak Crossover",
In:New Frontiers in Articial Intelligence (JSAI-isAI 2021
Workshops, JURISIN, LENLS18, SCIDOCA, Kansei-AI, AI-BIZ,
Yokohama, Japan, November 13-15, 2021, Revised Selected
Papers), LNAI 13856. Springer, pp.228{241.
84 / 96

85. Type SystemType Check/Inference Algorithm
Reference
Bekki, D. and E. McCready. (2015) \CI via DTS", In:New
Frontiers in Articial Intelligence (JSAI-isAI 2014 Workshops,
LENLS, JURISIN, and GABA, Yokohama, Japan, November
23-24, 2014, Revised Selected Papers), Vol. LNAI 9067.
Springer.
Bekki, D. and K. Mineshima. (2017) \Context-Passing and
Underspecication in Dependent Type Semantics", In: S.
Chatzikyriakidis and Z. Luo (eds.):Modern Perspectives in
Type-Theoretical Semantics, Studies of Linguistics and
Philosophy. Springer, pp.11{41.
Bekki, D. and M. Sato. (2015) \Calculating Projections via Type
Checking", In the Proceedings ofTYpe Theory and LExical
Semantics (TYTLES), ESSLLI2015 workshop.
85 / 96

86. Type SystemType Check/Inference Algorithm
Reference
Bekki, D., R. Tanaka, and Y. Takahashi. (2022) \Learning
Knowledge with Neural DTS", In the Proceedings ofthe 3rd
Natural Logic Meets Machine Learning (NALOMA III).
pp.17{25, Association of Computational Linguistics.
Bekki, D., R. Tanaka, and Y. Takahashi. (2023) \Integrating Deep
Neural Network with Dependent Type Semantics", In: R.
Loukanova, P. L. Lumsdaine, and R. Muskens (eds.):Logic and
Algorithms in Computational Linguistics 2021
(LACompLing2021), Studies in Computational Intelligence 1081.
Springer.
86 / 96

87. Type SystemType Check/Inference Algorithm
Reference
Chatzikyriakidis, S. (2014) \Adverbs in a Modern Type Theory",
In: N. Asher and S. V. Soloviev (eds.):Logical Aspect of
Computational Linguistics, 8th International Conference,
LACL2014, Toulouse, France, June 18-20, 2014 Proceedings.
Springer.
Cooper, R. (2005) \Records and Record Types in Semantic
Theory",Journal of Logic and Computation15(2), pp.99{112.
Daido, H. and D. Bekki. (2020) \Development of an automated
theorem prover for the fragment of DTS", In the Proceedings of
the 17th International Workshop on Logic and Engineering of
Natural Language Semantics (LENLS17).
Davila-Perez, R. (1995) \Semantics and Parsing in Intuitionistic
Categorial Grammar", Thesis, University of Essex. Ph.D. thesis.
87 / 96

88. Type SystemType Check/Inference Algorithm
Reference
Fox, C. (1994a) \Discourse Representation, Type Theory and
Property Theory", In the Proceedings of H. Bunt, R. Muskens,
and G. Rentier (eds.):the International Workshop on
Computational Semantics. pp.71{80.
Fox, C. (1994b) \Existence Presuppositions and Category
Mistakes",Acta Linguistica Hungarica42(3/4), pp.325{339.
Funakura, H. (2022) \Answers, Exhaustivity, and Presupposition of
wh-questions in Dependent Type Semantics", In the Proceedings
ofLogic and Engineering of Natural Language Semantics 20
(LENLS20). pp.72{76.
Geach, P. (1962)Reference and Generality: An Examination of
Some Medieval and Modern Theories. Ithaca, New York, Cornell
University Press.
Geurts, B. (1999)Presuppositions and pronouns. Elsevier, Oxford.
88 / 96

89. Type SystemType Check/Inference Algorithm
Reference
Groenendijk, J. and M. Stokhof. (1991) \Dynamic Predicate
Logic",Linguistics and Philosophy14, pp.39{100.
Kamp, H. (1981) \A Theory of Truth and Semantic
Representation", In: J. Groenendijk, T. M. Janssen, and M.
Stokhof (eds.):Formal Methods in the Study of Language.
Amsterdam, Mathematical Centre Tract 135.
Kamp, H. and U. Reyle. (1993)From Discourse to Logic. Kluwer
Academic Publishers.
Kinoshita, E., K. Mineshima, and D. Bekki. (2017) \An Analysis of
Selectional Restrictions with Dependent Type Semantics", In: S.
Kurahashi, Y. Ohta, S. Arai, K. Satoh, and D. Bekki (eds.):
New Frontiers in Articial Intelligence. JSAI-isAI 2016, Lecture
Notes in Computer Science, vol 10247. Springer, pp.19{32.
89 / 96

90. Type SystemType Check/Inference Algorithm
Reference
Kinoshita, E., K. Mineshima, and D. Bekki. (2018) \Coercion as
Proof Search in Dependent Type Semantics", In: C.
Fabricius-Hansen, B. Behrens, A. Pitz, and H. Petter Helland
(eds.):Possessives in L2 and translation: basic principles and
empirical ndings, Oslo Studies in Language 10, No 2. pp.1{20.
Krahmer, E. and P. Piwek. (1999) \Presupposition Projection as
Proof Construction", In: H. Bunt and R. Muskens (eds.):
Computing Meanings: Current Issues in Computational
Semantics, Studies in Linguistics Philosophy Series. Dordrecht,
Kluwer Academic Publishers.
Krifka, M. (1996) \Parametrized Sum Individuals for Plural
Anaphora",Linguistics and Philosophy19, pp.555{598.
Levinson, S. (1983)Pragmatics. Cambridge, Cambridge University
Press.
90 / 96

91. Type SystemType Check/Inference Algorithm
Reference
Luo, Z. (1997) \Coercive subtyping in type theory", In: D. van
Dalen and M. Bezem (eds.):CSL 1996. LNCS, vol. 1258.
Heidelberg, Springer.
Luo, Z. (1999) \Coercive subtyping",Journal of Logic and
Computation9(1), pp.105{130.
Luo, Z. (2010) \Type-theoretical semantics with coercive
subtyping", In the Proceedings ofSemantics and Linguistic
Theory 20 (SALT 20).
Luo, Z. (2012) \Formal Semantics in Modern Type Theories with
Coercive Subtyping",Linguistics and Philosophy35(6).
Martin, S. and C. J. Pollard. (2014) \A dynamic categorial
grammar", In the Proceedings ofFormal Grammar 19, LNCS
8612.
91 / 96

92. Type SystemType Check/Inference Algorithm
Reference
Matsuoka, D., D. Bekki, and H. Yanaka. (2023) \Appositive
Projection as Implicit Context Extension in Dependent Type
Semantics", In the Proceedings ofthe 20th International
Workshop on Logic and Engineering of Natural Language
Semantics (LENLS20). pp.82{87.
Piwek, P. and E. Krahmer. (2000) \Presuppositions in Context:
Constructing Bridges", In: P. Bonzon, M. Cavalcanti, and R.
Nossum (eds.):Formal Aspects of Context, Applied Logic
Series. Dordrecht, Kluwer Academic Publishers.
Ranta, A. (1994)Type-Theoretical Grammar. Oxford University
Press.
Soames, S. (1989) \Presupposition", In: D. Gabbay and F.
Guenthner (eds.):Handbook of Philosophical Logic, Vol. 4.
Dordrecht, Reidel, pp.553{616.
92 / 96

93. Type SystemType Check/Inference Algorithm
Reference
Sudo, Y. (2012) \On the Semantics of Phi Features on Pronouns",
Thesis, MIT. Doctoral dissertation.
Sundholm, G. (1986) \Proof theory and meaning", In: D. Gabbay
and F. Guenthner (eds.):Handbook of Philosophical Logic, Vol.
III. Reidel, Kluwer, pp.471{506.
Tanaka, R. (2014) \A Proof-Theoretic Approach to Generalized
Quantiers in Dependent Type Semantics", In the Proceedings
of R. de Haan (ed.):the ESSLLI 2014 Student Session, 26th
European Summer School in Logic, Language and Information.
pp.140{151.
Tanaka, R. (2021) \Natural Language Quantication and
Dependent Types", Thesis, Ochanomizu University. Doctoral
Dissertation.
93 / 96

94. Type SystemType Check/Inference Algorithm
Reference
Tanaka, R., K. Mineshima, and D. Bekki. (2015) \Factivity and
Presupposition in Dependent Type Semantics", In the
Proceedings ofTYpe Theory and LExical Semantics (TYTLES),
ESSLLI2015 workshop.
Tanaka, R., K. Mineshima, and D. Bekki. (2017) \On the
Interpretation of Dependent Plural Anaphora in a
Dependently-Typed Setting", In: S. Kurahashi, Y. Ohta, S. Arai,
K. Satoh, and D. Bekki (eds.):New Frontiers in Articial
Intelligence. JSAI-isAI 2016, Lecture Notes in Computer Science,
vol 10247. Springer, pp.123{137.
Tanaka, R., K. Mineshima, and D. Bekki. (2018) \Paychecks,
presupposition, and dependent types", In the Proceedings ofthe
Fifth Workshop on Natural Language and Computer Science
(NLCS2018), Preprint no.215. Oxford University.
94 / 96

95. Type SystemType Check/Inference Algorithm
Reference
van den Berg, M. (1996) \Some aspects of the internal structure
of discourse { the dynamics of nominal anaphora {", Thesis,
University of Amsterdam.
van der Sandt, R. (1992) \Presupposition projection as anaphora
resolution",Journal of Semantics9, pp.333{377.
Watanabe, K., K. Mineshima, and D. Bekki. (2019) \Questions in
Dependent Type Semantics", In the Proceedings ofProceedings
of the Sixth Workshop on Natural Language and Computer
Science (NLCS'19). pp.23{33.
Watanabe, N., E. McCready, and D. Bekki. (2014) \Japanese
Honorication: Compositionality and Expressivity", In the
Proceedings of S. Kawahara and M. Igarashi (eds.):FAJL 7:
Formal Approaches to Japanese Linguistics, the MIT Working
Papers in Linguistics 73. pp.265{276.
95 / 96

96. Type SystemType Check/Inference Algorithm
Reference
Yana, Y., D. Bekki, and K. Mineshima. (2019) \Variable Handling
and Compositionality: Comparing DRT and DTS",Journal of
Logic, Language and Information28(2), pp.261{285.
Yana, Y., K. Mineshima, and D. Bekki. (2021) \The proviso
problem from a proof-theoretic perspective", In the Proceedings
ofLogical Aspects of Computational Linguistics (LACL) 2021.
pp.159{176.
96 / 96