influential dtt papers

Stream: general

[Andrew Ashworth]

is there a list out there of really important papers in dtt? i recently read "Elimination with a Motive" that was linked in this chat and finally understood how cases works

[Mario Carneiro]

link?

[Mario Carneiro]

I'm still in the paper gathering stage, so I don't think I can help you that much, although I have been able to find good papers (maybe influential, maybe not) on specific topics

[Andrew Ashworth]

Elimination With a Motive

[Mario Carneiro]

Conor McBride is generally known for writing a number of DTT papers, so you could look there

[Andrew Ashworth]

yeah, he seems to have a lot of proof pearls

[Andrew Ashworth]

i like how even in the abstract he says : "I adopt a technique standard in `folklore', generalizing the ~x and expressing the restriction by equation...". Where do I learn this fabled folklore?!

[Andrew Ashworth]

maybe by reading all his papers :|

[Mario Carneiro]

Of course, that's code for "not written down yet", and is the bane of new researchers :)

[Simon Hudon]

That's the fun of literature review. What a fun summer that was ... reaches for bottle of whiskey

[Simon Hudon]

If that's helpful, I treat gathering a literature review like browsing wikipedia. There's a section at the end with their references and you just download all the papers with the interesting titles, read their intro and conclusion and start over with their reference section

[Andrew Ashworth]

that paper also explains where "no confusion" comes from

[Andrew Ashworth]

when I read about no_confusion in TPIL i was anything but not confused

[Simon Hudon]

when I read about no_confusion in TPIL i was anything but not confused

But it's supposed to be precluded by no_confusion!!!

[Kevin Buzzard]

when I read about no_confusion in TPIL i was anything but not confused

I was just the same. I'd never heard of the concept before and IIRC it's dropped in without any explanation right in the middle of the preliminary discussion on type classes when, rather than talking about things like Haskell type classes (which I kind of understood) they start going on about making a canonical nat and then randomly dropping a proof that 1 isn't 2 using no_confusion. That was a part of TPIL that I had to read again and again before it made sense. I flagged this up to Jeremy who I think might have done some rearranging as a consequence...