Kimball Germane

@Ngnghm This essay sounds very interesting. Is any draft available publicly?

I'm wondering whether to butcher my "Lambda The Ultimate Object" essay to submit pieces at ECOOP or other conferences, or to keep it in once piece and try to submit to a Journal, or what.

@AndrewCMyers Is the careful thinking devising an abstraction that the memory actually implements and developing a threat model based on it? If so, one reason there may be another attack lurking: the devised abstraction will certainly be oblivious to some classes of behavior.

based on that abstraction. Again, we needed more careful thinking about the threat model and what hardware/software mechanisms justified it. 6/7

Many people are skeptical of the formal approach to computer security because "there will always be more unexpected attacks". This criticism misunderstands how the formal approach represents real adversaries with abstract threat models. There are two parts to the answer. 1/7

Put it it

@kmett @MarisaVeryMoe @codydroux @ezyang @mattmight @andrasKovacs6 Abstract GC can be used in definitional interpreters too and big step enables a much more effective mode of it. (I have a recent ESOP paper about it.) Higher precision and (not published) incredible performance gains.

@MarisaVeryMoe @codydroux @ezyang @mattmight Exactly. I keep exploring CEK-like machines rather than big step semantics because it opens the possibility of abstract GC to tighten analyses or any analysis at all.. but @andrasKovacs6-style NbE is just so damn fast I cry whenever I have to run anything in a small-step setting.

Apparently it's way easier to write a staged interpreter than it is to write a compiler pass; functional IRs get their revenge!!!

@GuannanWei @ilyasergey @samth @krismicinski @mattmight @lambda_calculus @JanMidtgaard I have a draft paper connecting AAM, ADI, and PoPA constraint-based via a unifying monad exactly as Guannan suggests: monadic computations encode constraints, running it intertwines discovery and resolution. I’m happy to share to any interested.

@ilyasergey @samth @krismicinski @mattmight @lambda_calculus @JanMidtgaard Hmm, solving could be just running the monad. Also, I recalled that Nada Amin has some experiments of doing ADI in miniKanren github.com/namin/clpsmt-m…, but I'm not sure its current status.

Looking for a paper that makes an explicit connection between Abstract Abstract Machines and constraint-based CFA (a la PopA textbook). The closest work I know of is Midtgaard's ICFP'09 paper, but that precedes AAM. Any pointers? @JanMidtgaard @lambda_calculus @krismicinski

@glaebhoerl @GuannanWei This is how CFA2 does it. I have a blog post draft that does what I describe that I’d be happy to share. Now I’m wondering if you can analyze CPS code using ADI by inserting a continuation monad in the monad stack.

@glaebhoerl If your CPS transformation distinguishes the continuation terms it introduced, you can use the @GuannanWei’s technique (related to ADI) to get precise call-return matching for the calls that existed pre-CPS. You can often recover the distinction directly from the IR too.

Via @importantshock and @rob_rix, this is really rad: david.darais.com/assets/papers/… (Abstracting Definitional Interpreters, Darais + Labich + Nguyen + Van Horn, 2017)

@jeapostrophe You can prevent that by planting your finger while it fetches the new tweets (i.e. immediately). But, yeah, lame change.

This #OpenBordersDay, we publish the #OpenBordersManifesto: openborders.info/open-borders-m… Spread it far and wide!

When one lacks understanding, he can struggle for it or create a blind spot itself to which he becomes blind.