Jason (jcreed) wrote,

Whoa! This paper from like six years ago already suggests (at the end of Section 2.1) exactly the "swap" primitive I was vaguely thinking of as appropriate for how ref cells would interact with the differential privacy stuff. Always nice to be corroborated by history.

Looks like a neat paper anyway. The abstract is:

We explore foundational typing support for strong updates — updating a memory cell to hold values of unrelated types at different points in time. We present a simple, but expressive type system based upon standard linear logic, one that also enjoys a simple semantic interpretation for types that is closely related to models for spatial logics. The typing interpretation is strong enough that, in spite of the fact thato ur core calculus supports shared, mutable references and cyclic graphs, every well-typed program terminates. We then consider extensions needed to make our calculus expressive enough to serve as a model for languages with ML-style references, where the capability to access a reference cell is unrestricted, but strong updates are disallowed. Our extensions include a thaw primitive for temporarily re-gaining the capability to perform strong updates on unrestricted references.


Man if someone could scan in a copy of page 168 of Theoretical Computer Science volume 59 ("The Linear Abstract Machine", Yves Lafont, from 1988), I would be super grateful; The Penn library doesn't seem to have a paper copy, and refers me to ScienceDirect, whcih has the article but accidentally included page 193 where 168 should be, and page 168 unfortunately, I believe, contains only the most important definition of the entire paper in Table 1. I think it also has Tables 2 and 3, since alls I see is Tables 4 and onward.
Tags: papers, privacy, work

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded