Brainscape's Knowledge GenomeTM


Top Flashcards (Certified)
All Flashcards

Types > L10 > Flashcards

L10 Flashcards

1
Q

Proof and refutation terms syntax: propositions, true contexts, false contexts, values, continuations, contradictions

A

259

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

Expressions proof terms

A

260

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

refutation terms

A

261

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

Continuations

A

262

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

Op sem of CL+STLC

A

263

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

Preservation for contradictions

A

264

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

Type preservation for STLC+CL

A

265

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

Problematic definition of progress

A

266

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

how to make progress less vacuous

A

267-268

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

Why adding a halt config makes CL inconsistent

A

269

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

Why embed CL into IPL

A

270

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

Double Negation Translation

A

271

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

Triple negation elimination

A

272

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
14
Q

IPL DNE

A

273

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
15
Q

Dne for _

A

274

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
16
Q

Theorem : classical terms embed into intuitionistic terms

17
Q

CL->IPL translation of contexts

18
Q

CL->IPL translation of contraictions

19
Q

CL->IPL translation of most expressions

20
Q

CL->IPL translation of most continuations

21
Q

Translation of proof by contradiction

22
Q

Translation of refutation by contradiction

23
Q

Consequences of encoding CL into IPL

24
Q

Key property that must hold for any embedding

25
Godel Gentzen Translation
284
26
Kolmogorov translation
285
27
Point of implementing classical logic with implicit continuations
286
28
TLC with continuations
287
29
TLC+cont typing rules
288-291
30
DNE in TLC+Cont
292
31
EM in TLC+cont
292
32
CPS translation of types and contexts
293
33
CPS translation theorem
294
34
CPS translation
294-296

Types (6 decks)

Brainscape helps you reach your goals faster, through stronger study habits.
© 2025 Bold Learning Solutions. Terms and Conditions