Contextual Embeddings: Implementing Bound Variables through Instance Resolution
This program is tentative and subject to change.
Representing bound variables in embedded languages is a challenging problem, often requiring painful trade-offs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read and write. On the other hand, higher-order representations can piggy-back on the host language's binders to offer a more ergonomic interface, at a variety of costs depending on the technique. The current state-of-the-art is unembedding, i.e. a translation from the higher-order representation to the first-order and back again to get the best of both worlds. Unfortunately, the fact that this translation is type-safe relies on external metatheoretic arguments, holding unembedding back from its true potential. We solve this problem with a new embedding technique that uses instance resolution to define a context-directed isomorphism between an ergonomic higher-order interface and a first-order representation. Unlike previous techniques, this also applies to embedded languages with modal and substructural (e.g. linear) type systems, making unembedding relevant for modern languages.
This program is tentative and subject to change.
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:40 | |||
11:00 20mTalk | Decoupling Data Layouts from Bounding Volume Hierarchies PLDI Research Papers Christophe Gyurgyik Stanford University, Alexander J Root Stanford University, Fredrik Kjolstad Stanford University DOI Pre-print | ||
11:20 20mTalk | Contextual Embeddings: Implementing Bound Variables through Instance Resolution PLDI Research Papers Samantha Frohlich University of Bristol, Jessica Foster University of Bristol, Alex Kavvos University of Bristol, Meng Wang University of Bristol DOI Pre-print | ||
11:40 20mTalk | CoTenN: Constrained Optimization with Tensor Networks PLDI Research Papers Ritvik Sharma Stanford University, Cheng Peng Stanford Institute for Materials and Energy Sciences, SLAC National Accelerator Laboratory, Siddharth Dangwal University of Chicago, Sara Achour Stanford University DOI | ||
12:00 20mTalk | Diagramming Program Values by Spatial Refinement PLDI Research Papers Siddhartha Prasad Brown University, Michael Tu Brown University, Karan Kashyap Brown University, Tim Nelson Brown University, Shriram Krishnamurthi Brown University DOI | ||
12:20 20mTalk | Persistent Iterators with Value Semantics PLDI Research Papers DOI | ||