See Contextual Embeddings: Implementing Bound Variables through Instance Resolution by Samantha Frohlich, Jessica Foster, G. A. Kavvos and Meng Wang. I don't know if this is really Jessica Foster , internal evidence suggests the speaker is Samantha Frohlich. See About Logic - Dependent Types . Subscribe to ACM SIGPLAN .