Conversation

Normalisation, how to do it fast for the untyped lambda-calculus by means of evaluation, and why we care (together with some of the required type theory/PLT background): first of a series, hopefully. Feel free to yell at me in replies about mistakes etc! colimit.net/posts/normalis

Brendan Zabarauskas

@brendanzab

Feb 3, 2020

Thanks for pointing to Andreas Abel's thesis! I've not seen that one before. The levels/indices thing is weird but handy, but I've struggled to find where this idea emerged from. It's super interesting that Abel makes the connection between it an locally nameless!

Replying to

and

I've kind of struggled to find where the `n-(i+1)` weirdness comes from, so I'm happy to actually see an attempt to explain it here! Will be curious to look at the references to see if there is any earlier stuff on this!

9:00 PM · Feb 3, 2020Twitter Web App

Replying to

and

I thought Jon Sterling and

@dannygratzer

were calling it 'Semantic Type Checking' and attributing it to Coqand - but I'm not sure if that was the level/index representation+NbE or something else…