Bidirectional Type Checking

  Рет қаралды 6,361

Compose Conference

Compose Conference

Күн бұрын

Пікірлер: 5
@anchpop
@anchpop 5 жыл бұрын
The slide at 28:55 is incorrect. The code sample should read: check G other t2 = let t1 = synth G other in isSubtype t1 t2
@asitisj
@asitisj 2 жыл бұрын
Nat
@slowpnir
@slowpnir 3 жыл бұрын
What font does he use?
@GurwinderSingh-mk8db
@GurwinderSingh-mk8db 2 жыл бұрын
Iosevka
@Lircking
@Lircking 7 ай бұрын
nice
Type Driven Secure Enclave Development using Idris
26:48
Type Driven Secure Enclave Development using Idris
Compose Conference
Рет қаралды 448
The Best Refactoring You’ve Never Heard Of
32:33
The Best Refactoring You’ve Never Heard Of
Compose Conference
Рет қаралды 15 М.
伪装成一棵树整蛊妹妹，结果妹妹当场怀疑人生竟要揍我？【两只马儿-恶搞姐妹】
00:57
伪装成一棵树整蛊妹妹，结果妹妹当场怀疑人生竟要揍我？【两只马儿-恶搞姐妹】
两只马儿—恶搞姐妹
Рет қаралды 44 МЛН
So Cute 🥰 who is better?
00:15
So Cute 🥰 who is better?
dednahype
Рет қаралды 19 МЛН
Support each other🤝
00:31
Support each other🤝
ISSEI / いっせい
Рет қаралды 81 МЛН
Каха и дочка
00:28
Каха и дочка
К-Media
Рет қаралды 3,4 МЛН
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with [...]
22:57
Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with [...]
POPL 2019
Рет қаралды 1,8 М.
Building a Typechecker from scratch [1/20] Introduction to Type theory and checking
19:39
Building a Typechecker from scratch [1/20] Introduction to Type theory and checking
Dmitry Soshnikov
Рет қаралды 10 М.
George Wilson - An Intuition for Propagators - Compose Melbourne 2019
31:23
George Wilson - An Intuition for Propagators - Compose Melbourne 2019
Compose Conference
Рет қаралды 7 М.
Propositions as Types (7)
28:50
Propositions as Types (7)
Theo Reto
Рет қаралды 1,4 М.
Fast Inverse Square Root - A Quake III Algorithm
20:08
Fast Inverse Square Root - A Quake III Algorithm
Nemean
Рет қаралды 5 МЛН
Inside the V3 Nazi Super Gun
19:52
Inside the V3 Nazi Super Gun
Blue Paw Print
Рет қаралды 2,4 МЛН
How To Think Like A Programmer
1:00:07
How To Think Like A Programmer
Coding Tech
Рет қаралды 2,1 МЛН
Visualizing transformers and attention | Talk for TNG Big Tech Day '24
57:45
Visualizing transformers and attention | Talk for TNG Big Tech Day '24
Grant Sanderson
Рет қаралды 328 М.
"A Little Taste of Dependent Types" by David Christiansen
38:36
"A Little Taste of Dependent Types" by David Christiansen
Strange Loop Conference
Рет қаралды 40 М.
A Tase Of ATS
37:27
A Tase Of ATS
Compose Conference
Рет қаралды 3,8 М.
伪装成一棵树整蛊妹妹，结果妹妹当场怀疑人生竟要揍我？【两只马儿-恶搞姐妹】
00:57
伪装成一棵树整蛊妹妹，结果妹妹当场怀疑人生竟要揍我？【两只马儿-恶搞姐妹】
两只马儿—恶搞姐妹
Рет қаралды 44 МЛН