Conversation

finally grok CBPV and let me tell you, this is a thing of beauty

Oct 21, 2020

next up is focusing. 🎩 Gabriel Scherer who caught my attention in 3s at the end of a talk at ICFP 2015 with something like “check out focusing, it’s like bidirectional typechecking, but better,” which I think about frequently

-_-

@boarders__

Oct 21, 2020

Its important in the Dunfield, Krishnaswami GADT paper too! Something I would love to understand.

This Tweet is from a suspended account. Learn more

Brendan Zabarauskas

@brendanzab

Oct 21, 2020

Is that Lecture 4 of "Proof theory foundations"? cs.uoregon.edu/research/summe

This Tweet is from a suspended account. Learn more

Replying to

and

Yeah, just getting to grips with bidirectional type checking - TIL about focusing! 😅

10:58 PM · Oct 21, 2020Twitter Web App

Replying to

and

bidi typechecking is a good time :)