[Iris-Club] Acryonym: what does the CMRA stand for?
dreyer at mpi-sws.org
Thu Aug 4 10:50:54 CEST 2016
Hehe...I was wondering when someone would ask that question! We never
said what it stands for because no one was quite sure about the
answer. :-) There are several plausible answers, but they are all
kind of strange:
1. CMRA stands for "complete metric resource algebra" (or something
like that: we could never find a very suitable acronym).
2. CMRA stands for "camera", i.e. "camera" is not a pronunciation of
CMRA -- rather, the term "camera" came first and CMRA is an
abbreviation of "camera", which makes it look like some kind of
resource algebra. Cameras allow you to zoom in and out, which is kind
of like a "view shift".
3. The meaningless of the acronym "CMRA" mirrors the meaninglessness
of the name "Iris" itself.
Speaking of which, what does "Iris" stand for? We never said what
Iris stands for because no one was quite sure about the answer. :-)
There are several plausible answers, but they are all kind of strange:
1. Iris stands for "impredicativity, resources, invariants, and
separation" or some such nonsense.
2. The logic was originally called ROSE (standing for "resources,
ownership, separation, and I don't know what the E stood for") but
then I decided it was better not to name a logic after my wife. (What
if it turned out to be unsound? She would never forgive me.) Anyway,
I liked ROSE, and Iris is another flower with a nice short name that
could plausibly be an acronym for something.
3. Iris was developed around the same time as Dave Swasey was working
on compositional verification of SSH, and for some reason he was
calling his system "Bickle" (after Travis Bickle, the protagonist of
the movie Taxi Driver played by Robert De Niro). I still have no idea
why he was calling his system Bickle. I convinced him instead to call
it "Travis" -- that way, if we had a typed version of his system, we
could call it "TravisT" (for "Travis Typed") and pronounce it
"travesty" (hoho). Since it seemed like Iris could provide a more
general framework for encoding Travis, we somehow thought it would be
a good idea to name the logic after the underage prostitute character
Iris in Taxi Driver (played by Jodie Foster) whom Travis takes it upon
himself to protect. (OK, there's a pun connecting Iris and Travis
that makes this story slightly less ridiculous, but it's NSFW. Ask me
over beer.) Incidentally, the Iris character in Taxi Driver is of
historical importance: John Hinckley was so obsessed with Jodie
Foster's performance as Iris in Taxi Driver that he shot Ronald Reagan
in order to impress her.
In short, the meaninglessness of the acronym "Iris" (and the utter
obscurity of its provenance) mirrors the meaninglessness of the movie
"Taxi Driver" itself.
Speaking of which, what is "Taxi Driver" all about anyway? Beats me,
but it's a great movie, just like Iris is a great logic!
On Thu, Aug 4, 2016 at 9:54 AM, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr> wrote:
> Dear Iris Club,
> This is not a technical question, but :-)
> I couldn't find what CMRA stands for in the paper and the appendix.. May I
> ask what does it stand for?
> Thank you,
> Jeehoon Kang (Ph.D. student)
> Software Foundations Laboratory
> Seoul National University
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
More information about the Iris-Club