[PRL] Practice Talk for HOPE on Sept 20th 14:00, WVH 366

[Phillip Mates]

Hello, I'm presenting at HOPE next Saturday. Please come critique my talk
tomorrow at 2:00pm in WVH 366.
Thanks, Phillip.


Speaker: Phillip Mates
Talk venue: HOPE workshop

Title: A Kripke Logical Relation for Linear Functions: The Story of a Free
Theorem in the Presence of Non-termination

Abstract:
In the course of extending Ahmed and Blume's recent work on fully abstract
CPS translation to a language with non-termination, we have encountered the
need for a free theorem that cannot be proved using existing logical
relations. The free theorem involves a mix of linear functions and
linearly-treated intuitionistic functions. To reason about the latter, we
have had to develop a step-indexed Kripke logical relation that allows us
to reason about how a linearly treated function may have been used.
-------------- next part --------------
HTML attachment scrubbed and removed