Conversation

I have a few times not written up "Here is how <thing> is done in Idris" because I expect to be told it's been done before. I should do it anyway, but it would essentially be done as a really nerdy hobby and I already have plenty of them...

Quote Tweet

Chris Martin

@chris__martin

· Feb 14, 2019

Replying to @KirinDave

Academic culture should encourage a lot more rewritings of research IMO, originality is overrated

Miëtek Bak

@mietek

Feb 15, 2019

Please, write down the stuff that does not get published because ‘everybody knows it’; the stuff that only propagates via physical proximity; the stuff that makes type theory an oral tradition. Please.

Brendan Zabarauskas

@brendanzab

Feb 15, 2019

Yes! This! I only know about 'semantic type checking' thanks to

@jonsterling

telling me and

@dannygratzer

's repository: github.com/jozefg/nbe-for - these kinds of ideas are super valuable for those of us interested in language development outside of academia! :)

github.com

GitHub - jozefg/nbe-for-mltt: Normalization by Evaluation for Martin-Löf Type Theory

Normalization by Evaluation for Martin-Löf Type Theory - GitHub - jozefg/nbe-for-mltt: Normalization by Evaluation for Martin-Löf Type Theory

Brendan Zabarauskas

@brendanzab

Feb 15, 2019

I wasted many months on locally nameless representations and binding libraries like github.com/brendanzab/mon. I guess it was good learning anyway, but I was attracted to it because it had such a nice paper introducing it: chargueraud.org/research/2009/