The troublesome reflection rule (TYPES 2015 slides)

Here are the slides of my TYPES 2015 talk “The troublesome reflection rule” with fairly detailed presenter notes. The meeting is  taking place in Tallinn, Estonia – a very cool country in many senses (it’s not quite spring yet even though we’re in the second half of May, and it’s the country that gave us Skype).

Download slides: The troublesome reflection rule (TYPES 2015) [PDF].

2 thoughts on “The troublesome reflection rule (TYPES 2015 slides)

  1. Nice! A few comments/questions:

    1. Some of the notes on the RHS of the slides are cut off at the end.
    2. Doesn’t the eta-rule together with the reflection rule give you function extensionality?
    3. Are you saying that the reflection rule is never applied (and, thus, an Eq-term in the context is never used) unless a hint explicitly instructs us to?

Leave a Reply to Andrej Bauer Cancel reply

Your email address will not be published. Required fields are marked *

*