Fwd: OOPSLA 2013 Paper Notification [116]

[Joe Gibbs Politz]

Congratulations everyone! LambdaPy will appear at OOPSLA this fall!
Great work all around, I'm super excited :-D

I'll follow up soon with a plan for how we should prepare our code for
evaluation. That is due sooner than I thought --- next Saturday, June
1 --- so I'll summarize what I think we need for packaging and
clean-up before then.

Good job, team!



---------- Forwarded message ----------
From: Cristina V. Lopes <oop...@splashcon.org>
Date: Fri, May 24, 2013 at 6:31 PM
Subject: OOPSLA 2013 Paper Notification [116]
To: j...@cs.brown.edu, amtri...@gmail.com, mat...@cs.brown.edu,
jswa...@cs.brown.edu, dbpa...@cs.brown.edu, ljs.da...@gmail.com,
anand...@gmail.com, s...@cs.brown.edu
Cc: oop...@splashcon.org, oopsla2013-pa...@borbala.com


Dear Joe, Alejandro, Matthew, Sumner, Daniel, Junsong, Anand and Shriram,

Congratulations! Your paper

"Python: The Full Monty; A Tested Semantics for the Python
Programming Language"

has been selected to advance to the 2nd phase of OOPSLA 2013! Please
see the main editorial feedback as well as the individual reviews
enclosed in this email.

I look forward to receiving the improved version of your paper!

Crista Lopes
OOPSLA 2013 PC Chair

-----------------------------------------------------------------

PLEASE PAY CLOSE ATTENTION TO ALL PARTS OF THIS EMAIL, AS IT CONTAINS
IMPORTANT INFORMATION THAT YOU NEED IN ORDER TO REVISE AND RESUBMIT
YOUR PAPER.

*** OOPSLA Artifacts ***

I would like to strongly encourage you to formally submit supporting
materials to the Artifact Evaluation (AE) process. The deadline is
June 1, 2013. For more information, please see
http://splashcon.org/2013/cfp/due-june-01-2013/665-oopsla-artifacts

Submission to the AE is not mandatory, and your decision to submit
your artifacts, or not, will not influence the outcome of your
paper. Nevertheless, the readers of your paper will likely benefit
from having access to those artifacts, and the attention that your
work will get may likely increase if you make those artifacts publicly
available.

Papers whose artifacts are endorsed by the AE committee will be given
a stamp on the final camera-ready version attesting that endorsement.

For further questions regarding the AE process, please contact the AE
committee chairs Matthias Hauswirth and Steve Blackburn, at
arti...@splashcon.org

*** Resubmission of the paper ***

* You must submit your revised paper on or before July 20, 2013. The
resubmission can be done at any time between now and then. If you
resubmit early, please send me an email notifying me of your final
submission, and I will try to inform you of the final decision early,
too. Otherwise, the official final notification date is July 29, 2013.

* Your revised paper should be no longer than 20 pages, including
everything -- appendices, bibliography, etc.

* Your paper must be revised and improved according to the feedback in
this email. In order for reviewers to make a speedy assessment of
your improvements to the paper, you must submit a "cover letter" along
with your paper detailing how you reacted to the revision requests and
the reviewers' comments. If you have never written one of these cover
letters before, you can find an example here:

http://www.ics.uci.edu/~lopes/documents/cover_letter_example.pdf

You can find many additional resources for writing responses to
reviewers if you search the Web for "response to reviewers".

The goal of the cover letter is to speed up the reviewers'
reassessment of your work. Please do not engage in long explanations
in the cover letter; the best reactions to revision requests are those
made in the paper itself. The reviewers simply need to know where to
look.

Unless your paper has been considered acceptable as-is, THE ABSENCE OF
THE COVER LETTER IS GROUNDS FOR THE PAPER'S REJECTION.

* The resubmission must consist of one single ZIP file containing
both the paper and the cover letter, both in PDF. The resubmission
can be done with your usual credentials:

Resubmission link: http://cyberchair.acm.org/oopslapapers/submit/
Username: j...@cs.brown.edu
Password: SPL-136396836718687

(It is ok to override what is currently in Cyberchair, even though
that wouldn't happen normally, because you will now be submitting a
ZIP file instead of a single PDF file)

* Optionally, additionally to the paper itself and the cover letter,
you can also include another PDF file that highlights the differences
between your original submission and the revised submission. (If you
are using latex, you can use latexdiff). This is optional.

*** Main editorial feedback ***

What follows is a summary of the perceived contributions of your work,
and a list of requested revisions that the Committee agreed must be
addressed in the revised submission.

----

The reviewers liked this work very much. They believe it can have as much
impact as your previous work on the semantics of JavaScript.

The paper could be accepted as is. We encourage you to address the minor points
raised in the individual reviews to improve this paper for final copy.

----

If you are unable or unwilling to perform these revisions, please
contact me as soon as possible explaining the situation.

Failing to revise the paper according to this main editorial feedback
may lead to the paper being rejected. Also, if the revisions are such
that would affect the main conclusions of your paper, that should be
clearly noted in the cover letter, and the new conclusions should be
reflected in the paper. While it may be acceptable to present weaker
conclusions than originally submitted, trying to defend the same
conclusions with weaker results will likely lead to rejection of your
paper.

*** Individual Reviews ***

Additionally to the Committee's feedback, each reviewer produced a
technical review of your paper that you may want to take closely into
consideration when revising it. While it is not mandatory to address
every single revision request in the individual reviews, it is
generally a good idea to acknowledge their existence and to try to
improve the paper accordingly, when it makes sense.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=

First reviewer's review:

>>> Summary of the submission <<<

This paper gives a formal semantics of Python, comprising an elaboration into a
core calculus and a reduction semantics for that calculus. The semantics are
validated by running a test suite of Python programs on an interpreter derived
from the semantics and comparing the result with the real Python
implementation.

>>> Contributions <<<

The semantics themselves are the main contribution.

>>> Technical Review <<<

This is solid work solving an important problem: giving a formal semantics for
a real world programming language. Testing the semantics for conformance with a
Python implementation is absolutely necessary, as the implementation is the de
facto standard for the language. However, the paper does not establish the
usefulness of the semantics. It doesn't use them as the basis for any static or
dynamic analysis tools; it does not prove anything about them, nor does it
argue convincingly that the semantics are a useful human readable artefact. The
explanation of Python in the paper is carried out (very clearly) mostly via
example and prose. The key question then is, what are these semantics good for?
The exercise of making them led the authors to come to a deep understanding of
the oddities of Python, which are explained in the paper, and this is
something; furthermore, by thoroughly testing the semantics, we can have some
confidence that they have identified all of the oddities. Hence, on balance I
think the paper's contribution is large enough to merit acceptance, although it
would be much stronger if it also did something with the semantics.

>>> Revisions <<<

The presentation of Section 4 is essentially a large digression into an
approach that doesn't work. It's worth going through, because it informs the
actual solutions in Section 5, but it should be more clearly identified as a
failed attempt up front, rather than right at the end.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*

Second reviewer's review:

>>> Summary of the submission <<<

The paper describes a project defining the semantics for a subset of the
Python
language. The project follows the approach of the earlier \lambda_{JS}
project,
defining the semantics of JavaScript. The semantics of a core language
\lambda_\pi is
described both as a small step operational semantics using the Redex system and
as an
interpreter implemented in Racket. A four step desugaring maps programs in the
full
Python language to the core language.

The soundness of the formalization is tested by comparing the results computed
with
the interpreter against the result computed with the CPython interpreter. The
test
suite used for this conformance testing is derived from CPython's testsuite.
Not all
of that suite can be used in the current state of the project due to limited
coverage
of the language and native libraries.

The discussion in the paper focusses on the unusual features of variable scope
of
Python. Various of these cases (non-local scope, yield) are translated to the
more
traditional lexical scope constructs in the core language.

>>> Technical Review <<<

The paper fits in the recent tradition of 'semantic archeology' projects that
attempt
to reconstruct a formal semantics of (dynamic/'scripting') programming
languages and
thus arrive at a better understanding of those languages (e.g. the lambda_JS
project
of the authors, the R reconstruction project of Vitek et al.). This is an
interesting
effort. However, unlike those earlier papers I did not gain much insight from
this
paper.

The observations about the scope system are interesting, but hard to follow. I
am not
convinced that expressing the scope rules through desugaring is very
illuminating. A
direct and explicit definition of those scope rules would not require such
elaborate
descriptions; provided of course there would be a good formalization of those
scope
rules.

Also the state of the project is somewhat immature; only a subset of the
language is
covered and it is not clear that it is feasible to finish the project (or that
the
authors will do so).

The stated purpose of the semantics is to support the definition of sound
tools. "Thus, it is vital to have a precise semantics available for analyzing
programs and proving properties about them." (p1) The claim of the paper is
that the
formalization described in the paper can serve that purpose, but does not
substantiate it by doing either. It is not clear to me that the considerable
distance
between source Python and lambda_pi enables analyzing and proving properties
of
source Python programs.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*

Third reviewer's review:

>>> Summary of the submission <<<

This paper presents a semantics for most of Python. It is implemented
by translation to a core langugage, named \lambda_pi, which includes
the core features of the CBV lambda calculus with mutable objects. The
translation manages most of the key semantic intricacies of Python, in
particular scope, generators, classes, and the interplay between
these. The semantics has been tested on some of the Python test
suites, which required modification for the purpose.

>>> Technical Review <<<

This paper reports an impressive feat of semantics engineering. The
authors prior work on \lambda_JS has been the foundation for
significant development of tools for that language, and this work
applies the same technique to Python.

Here, the central challenges relate to scope, and particularly the
interaction with classes and generators.

Unfortunately, the presentation of section 4 obscures what's going on
here. In particular, the problem with the desugaring in section 4.2 is
that the desugaring is to an imagined version of Python with standard
lexical scope, and when that turns out not to be the semantics of
Python, the desugaring fails.

However, as explained later in the paper, Python has the features
necessary to express the desired binding forms, using `nonlocal`. The
transformation involves scope, that is true, and scope is tricky in
Python. The paper does an excellent job of explaining the details of
Python's scope. But the paper does not show that the generators can't
be desugared to Python.

Two other issues give this reviewer pause as to the completeness of the
effort. First, the issue of the `locals()` function in the conclusion
seems as if it would obviate all possibility of avoiding contortions in
the treatment of scope. Is all the work here for naught in the
presence of `locals`? Even JavaScript's `with` and direct `eval` are
better-controlled.

Second, there is next to no discussion of modules. Section 7 mentioned
that `import *` is not yet supported. Modules are discussed in the
(strangely-numbered) appendix, but only briefly, and very few tests
cover them. This seems another tricky area of scope.

Finally, the authors are duly proud of how much of the standard
library can be implemented in \lambda_pi, and how much is in the
desugaring. However, this seems to come at substantial performance
cost in analyzing the standard library, and perhaps will make life
more difficult for analysis tools which cannot simply describe the
behavior of standard library functions. More discussion of the
tradeoffs around this point would be valuable.

*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*=--=*