diff --git a/popl19/revisions.md b/popl19/revisions.md new file mode 100644 index 0000000000000000000000000000000000000000..6515a969b0ad8bec56cb22a32283652363a60fa9 --- /dev/null +++ b/popl19/revisions.md @@ -0,0 +1,27 @@ +We summarize the major changes to the paper. There are also some minor +typo fixes/re-wordings in various sections. + +1. To clarify the applicability of the main results, we added a few + paragraphs to the discussion section at the end to discuss what + languages should be models of GTT, how things like reference + equality fit in and the difference between call-by-name and + Haskell's notion of laziness. We also put some forward references + to this discussion in the introduction. +2. We expanded the related work a great deal, adding comparisons to + Henglein and Degen and Thiemann's work. We also clarified that AGT + is based on the *type safety proof* of the static language, and not + just its dynamic semantics. +3. We added an explicit list of contributions to the end of the + introduction. +4. The list of contributions has forward references giving an overview + of the paper structure, and we also added an overview to the + beginning of section 2. +5. To avoid "story of discovery" with the dynamic type models, we + mention type tags and how this is the usual way of constructing a + dynamic type for the value type and the novel aspect is the fact + that the dual is useful for interpreting the dynamic computation + type. +6. We named the rules, specifically in figures 1-5. +7. We re-ordered some paragraphs in the introduction to introduce eta + equality before the discussion of eager and transient cast + semantics.