diff --git a/papers/scp/PLFA.tex b/papers/scp/PLFA.tex
index 5f026bb9..cd74ac64 100755
--- a/papers/scp/PLFA.tex
+++ b/papers/scp/PLFA.tex
@@ -416,7 +416,10 @@ denotational equality to justify code transformations.
PLFA and SF differ in several particulars. PLFA begins with a computationally
complete language, PCF, while SF begins with a minimal language, simply-typed
-lambda calculus with booleans. PLFA does not include type annotations in terms,
+lambda calculus with booleans. We chose PCF because it lets us use
+the same examples, based on addition and multiplication, for the early
+chapters of both Part I and Part II.
+PLFA does not include type annotations in terms,
and uses bidirectional type inference, while SF has terms with unique types and
uses type checking. SF also covers a simple imperative language with Hoare
logic, and for lambda calculus covers subtyping, record types, mutable
@@ -433,8 +436,9 @@ added a fourth volume on random testing of Coq specifications using QuickChick.
There is currently no tool equivalent to QuickChick for Agda.
There is more material that would be desirable to include in PLFA which was not
-due to limits of time, including mutable references, logical relations, System~F, and
-pure type systems. We'd especially like to include pure type systems as they
+due to limits of time, including mutable references, System~F, logical
+relations for parametricity, and pure type systems.
+We would especially like to include pure type systems as they
provide the readers with a formal model close to the dependent types used in the
book. Our attempts so far to formalise pure type systems have proved
challenging, to say the least.
@@ -495,12 +499,17 @@ cases deal with the situation where there are potentially two
different reductions; each case is trivially shown to be
impossible. Five of the ten cases are redundant, as they just involve
switching the order of the arguments. We had to copy the cases
-suitably permuted. It would be preferable to reinvoke the proof on
+nsuitably permuted. It would be preferable to reinvoke the proof on
switched arguments, but this would not pass Agda's termination checker
since swapping the arguments doesn't yield a recursive call on
-structurally smaller arguments. We suspect tactics could cut down the
-proof significantly. We tried to compare with SF's proof that reduction
-is deterministic, but failed to find that proof.
+structurally smaller arguments. The proof of determinism in SF
+(Chapter Norm) is for a different language of comparable size,
+and has a comparable size.
+
+% We suspect tactics could cut down the
+% proof significantly.
+% We tried to compare with SF's proof that reduction
+% is deterministic, but failed to find that proof.
SF covers an imperative language with Hoare logic, culminating in code that
takes an imperative programme suitably decorated with preconditions and
@@ -552,9 +561,8 @@ the icon is expanded. As teachers, we were aware that students might skip the
formal proof on a first reading, and we have to hope the students
return to it and step through it with an interactive tool in order to make it
intelligible. We expect the students skipped over many such proofs. This
-particular proof forms the basis for a question of the mock exam and the past
-exams, so we expect most students will look at this one if not all the
-others.
+particular proof forms the basis for a question on several exams,
+so we expect most students will look at this one if not all the others.
\newcommand{\ex}{\texttt{x}}
\newcommand{\why}{\texttt{y}}
@@ -640,7 +648,8 @@ supporting all the necessary characters. Securing one has proved
tricky. As of this writing, we use FreeMono, but it lacks a few
characters ($\typecolon$ and $\qedsymbol$) which are loaded from fonts with a different
width. Long arrows are necessarily more than a single character wide.
-Instead, we compose reduction —→ from an em dash — and an arrow →.
+Instead of the unicode long arrow,
+we compose reduction —→ from an em dash — and an ordinary arrow →.
Similarly for reflexive and transitive closure —↠.
\section{Progress + Preservation = Evaluation}
@@ -768,7 +777,7 @@ connection becomes more widely known.
% TODO: consider rewriting this?
The second part of PLFA first discusses two different approaches to
modeling simply-typed lambda calculus. It first presents
-terms with named variables and and extrinsic typing relation and
+terms with named variables and extrinsic typing relation and
then shifts to terms with de Bruijn indices that are intrinsically
typed. The names \emph{extrinsic} and \emph{intrinsic} for these
two approaches are taken from \citet{Reynolds-2003}.
@@ -805,8 +814,8 @@ the corresponding judgment in the intrinsic approach does not. The difference
becomes more pronounced when including the code for substitution, reductions,
and proofs of progress and preservation. In particular, where the extrinsic approach
requires one first define substitution and reduction and then prove they
-preserve types, the intrinsic approach establishes substitution at the same time
-it defines substitution and reduction.
+preserve types, the intrinsic approach establishes substitution
+preserves types at the same time it defines substitution and reduction.
Stripping out examples and any proofs that appear in one but not the other (but
could have appeared in both), the full development in PLFA for the extrinsic approach
@@ -835,8 +844,9 @@ advantages of de Bruijn indices and intrinsic types.
There are actually four possible designs, as the choice of named
variables vs de Bruijn indices, and the choice of extrinsic vs
-intrinsic typing may be made independently. There are synergies
-between the two. Manipulation of de Bruijn indices can be notoriously
+intrinsic typing may be made independently. But the two designs
+we chose work well, while the other two are problematic.
+Manipulation of de Bruijn indices can be notoriously
error-prone without intrinsic types to give assurance of correctness.
For instrinsic typing with named variables, simultaneous substitution by
open terms remains difficult.
diff --git a/papers/scp/conflicts.txt b/papers/scp/conflicts.txt
new file mode 100644
index 00000000..16a75691
--- /dev/null
+++ b/papers/scp/conflicts.txt
@@ -0,0 +1,46 @@
+All (Indiana University)
+Giuseppe Castagna (Univ. of Paris Diderot)
+David Broman (KTH)
+Amal Ahmed (Northeastern Univ.)
+Dustin Jamner (Northeastern Univ.)
+Michael M. Vitousek (Facebook)
+Matteo Cimini (Univ. of Mass. Lowell)
+Carl Friedrich Bolz-Tereick (Heinrich-Heine-Universität Düsseldorf)
+David Christiansen (Galois Inv.)
+Peter Thiemann (Univ. of Freiburg)
+All (University of Edinburgh)
+Fabrizio Montesi (University of Southern Denmark)
+Marco Peressotti (University of Southern Denmark)
+J. Garrett Morris (Kansas University)
+All (University of Edinburgh)
+J. Garrett Morris (Kansas University)
+Jeremy Yallop (Cambridge)
+Jack Williams (Microsoft)
+Jakub Zalewski
+Shayan Najd
+Niki Vazou (IMDEA Software Institute)
+Anish Tondwalkar (University of California, San Diego)
+Vikram Choudhury (Indiana University)
+Ryan G. Scott (Indiana University)
+Ryan R. Newton (Indiana University)
+Ranjit Jhala (University of California, San Diego)
+Atsushi Igarashi (Kyoto University)
+Vasco T. Vasconcelos (University of Lisbon)
+Tom Schrijvers (KU Leuven)
+Bruno Oliveira (University of Hong Kong)
+Koar Mantirosian (KU Leuven)
+Marco Carbone (IT University of Copenhagen)
+Fabrizio Montesi (University of Southern Denmark)
+Carsten Schürmann (IT University of Copenhagen)
+Andreas Abel (Gothenburg University)
+Jesper Cockx (Gothenburg University)
+Dominique Devriese (Vrije Universiteit Brussel)
+Amin Timany (KU~Leuven)
+Nobuko Yoshida (Imperial)
+Raymond Hu (Hertfordshire)
+Bernardo Toninho (Universidade NOVA de Lisboa)
+Julien Lange (Kent)
+Simon Thompson (Kent)
+Nicholas Ng
+Robert Griesemer (Google)
+All (IOHK)
diff --git a/papers/scp/credit-author-statement.txt b/papers/scp/credit-author-statement.txt
new file mode 100644
index 00000000..bb473473
--- /dev/null
+++ b/papers/scp/credit-author-statement.txt
@@ -0,0 +1,3 @@
+Philip Wadler: Writing - Original Draft, Writing - Review & Editing, Software,
+Wen Kokke: Writing - Review & Editing, Software,
+Jereemy Siek: Writing - Review & Editing, Software,
diff --git a/papers/scp/declaration-of-competing-interests.docx b/papers/scp/declaration-of-competing-interests.docx
new file mode 100644
index 00000000..00d2187b
Binary files /dev/null and b/papers/scp/declaration-of-competing-interests.docx differ
diff --git a/papers/scp/declaration-of-competing-interests.pdf b/papers/scp/declaration-of-competing-interests.pdf
new file mode 100644
index 00000000..54bc5b7d
Binary files /dev/null and b/papers/scp/declaration-of-competing-interests.pdf differ
diff --git a/papers/scp/determinism.coq b/papers/scp/determinism.coq
new file mode 100644
index 00000000..9667be1f
--- /dev/null
+++ b/papers/scp/determinism.coq
@@ -0,0 +1,55 @@
+Lemma step_deterministic :
+ deterministic step.
+Proof with eauto.
+ unfold deterministic.
+ intros t t' t'' E1 E2.
+ generalize dependent t''.
+ induction E1; intros t'' E2; inversion E2; subst; clear E2...
+ (* ST_AppAbs *)
+ - inversion H3.
+ - exfalso; apply value__normal in H...
+ (* ST_App1 *)
+ - inversion E1.
+ - f_equal...
+ - exfalso; apply value__normal in H1...
+ (* ST_App2 *)
+ - exfalso; apply value__normal in H3...
+ - exfalso; apply value__normal in H...
+ - f_equal...
+ (* ST_Pair1 *)
+ - f_equal...
+ - exfalso; apply value__normal in H1...
+ (* ST_Pair2 *)
+ - exfalso; apply value__normal in H...
+ - f_equal...
+ (* ST_Fst *)
+ - f_equal...
+ - exfalso.
+ inversion E1; subst.
+ + apply value__normal in H0...
+ + apply value__normal in H1...
+ (* ST_FstPair *)
+ - exfalso.
+ inversion H2; subst.
+ + apply value__normal in H...
+ + apply value__normal in H0...
+ (* ST_Snd *)
+ - f_equal...
+ - exfalso.
+ inversion E1; subst.
+ + apply value__normal in H0...
+ + apply value__normal in H1...
+ (* ST_SndPair *)
+ - exfalso.
+ inversion H2; subst.
+ + apply value__normal in H...
+ + apply value__normal in H0...
+ - (* ST_TestTrue *)
+ inversion H3.
+ - (* ST_TestFalse *)
+ inversion H3.
+ (* ST_Test *)
+ - inversion E1.
+ - inversion E1.
+ - f_equal...
+Qed.
diff --git a/papers/scp/determinism.lagda b/papers/scp/determinism.lagda
new file mode 100644
index 00000000..8ac3b057
--- /dev/null
+++ b/papers/scp/determinism.lagda
@@ -0,0 +1,24 @@
+det : ∀ {M M′ M″}
+ → (M —→ M′)
+ → (M —→ M″)
+ --------
+ → M′ ≡ M″
+det (ξ-·₁ L—→L′) (ξ-·₁ L—→L″) = cong₂ _·_ (det L—→L′ L—→L″) refl
+det (ξ-·₁ L—→L′) (ξ-·₂ VL M—→M″) = ⊥-elim (V¬—→ VL L—→L′)
+det (ξ-·₁ L—→L′) (β-ƛ _) = ⊥-elim (V¬—→ V-ƛ L—→L′)
+det (ξ-·₂ VL _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ VL L—→L″)
+det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″) = cong₂ _·_ refl (det M—→M′ M—→M″)
+det (ξ-·₂ _ M—→M′) (β-ƛ VM) = ⊥-elim (V¬—→ VM M—→M′)
+det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—→L″)
+det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
+det (β-ƛ _) (β-ƛ _) = refl
+det (ξ-suc M—→M′) (ξ-suc M—→M″) = cong `suc_ (det M—→M′ M—→M″)
+det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ case_[zero⇒_|suc_⇒_]
+ (det L—→L′ L—→L″) refl refl refl
+det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)
+det (ξ-case L—→L′) (β-suc VL) = ⊥-elim (V¬—→ (V-suc VL) L—→L′)
+det β-zero (ξ-case M—→M″) = ⊥-elim (V¬—→ V-zero M—→M″)
+det β-zero β-zero = refl
+det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
+det (β-suc _) (β-suc _) = refl
+det β-μ β-μ = refl
diff --git a/papers/scp/highlights.txt b/papers/scp/highlights.txt
index 09df6539..86d9e185 100644
--- a/papers/scp/highlights.txt
+++ b/papers/scp/highlights.txt
@@ -11,9 +11,9 @@ Highlights for Review
* Constructive proofs of preservation and
progress give rise to a prototype evaluator.
-* Using raw terms with a separate typing
- relation is far less perspicuous than using
- inherently-typed terms.
+* Using raw, extrinsically-typed terms
+ is less perspicuous than using
+ intrinsically-typed terms.
* An online final examination with access to a
proof assistant can lead to flawless student
diff --git a/papers/scp/response-to-reviewers.txt b/papers/scp/response-to-reviewers.txt
new file mode 100644
index 00000000..84b01648
--- /dev/null
+++ b/papers/scp/response-to-reviewers.txt
@@ -0,0 +1,437 @@
+[We thank the reviewers for their comments. Responses interleaved in
+brackets. The revision includes a few other improvements, in
+particular consistently using standard terms "extrinsic"/"intrinsic"
+in place of "raw"/"inherent".]
+
+Ms. Ref. No.: SCICO-D-19-00172 Title: Programming Language Foundations
+in Agda Science of Computer Programming
+
+Dear Professor Philip Wadler,
+
+Thank you very much for having submitted to the Science of Computer
+Programming Journal.
+
+We have now received reviewers' reports and a recommendation by the
+handling editor; based upon the recommendation and the reviews, we
+would like to ask you prepare a minor revision taking the comments of
+the reviewers into account.
+
+The due date for revision is Feb 14, 2020. If this deadline is out of
+sync with other due dates communicated to you outside EES, then please
+contact the handling editor to settle this.
+
+If you decide to revise the work, please submit a list of changes or a
+rebuttal against each point which is being raised when you submit the
+revised manuscript.
+
+To submit a revision, please go to https://ees.elsevier.com/scico/ and
+login as an Author. Your username is: wadler@inf.ed.ac.uk If you need
+to retrieve password details, please go to:
+http://ees.elsevier.com/scico/automail_query.asp
+
+On your Main Menu page is a folder entitled "Submissions Needing
+Revision". You will find your submission record there.
+
+Once again, thank you very much for having given us the opportunity to
+consider your manuscript.
+
+Mohammad Reza Mousavi, Ph.D. Editor-in-Chief Science of Computer
+Programming
+
+
+Reviewers' comments:
+
+
+The reviewers have been unanimous in accepting the article for
+publication. There are a few remarks to be considered by the authors
+for the final version, as pointed out in the reviews.
+
+Reviewer #1: This article reports on experience teaching basic results
+in lambda calculus using a proof assistant based on type theory. The
+first finding is that the proof style supported by Agda,
+i.e. dependently typed programming, need not be more verbose than the
+tactic-based style supported by Coq. The second finding is a
+functional pearl: constructive proof of progress and preservation
+directly yield an interpreter. The third finding is that
+formalization of typed lambda calculus based on inherently typed terms
+is significantly more succinct than formalization in terms of a
+separate typing judgment. Finally, the authors report on flawless
+student performance on an exam using the proof assistant.
+
+The last point may not seem surprising to readers with experience
+teaching this material as presented in the book Software Foundations
+(SF) by Pierce et al, specifically the volume title Programming
+Language Foundations. (Or for that matter, teaching related topics
+using a proof assistant, e.g., based on the book Concrete Semantics by
+Nipkow and Klein.) The authors have written a book, PLFA, drawing on
+corresponding chapters of the book by Pierce et al which develops a
+more extensive range of programming language theory using Coq.
+Section 2 of the article describes PLFA with reference to SF, and
+Section 7 describes experience with open source publishing.
+
+At first glance I was concerned that this article might be little more
+than a promotion for the book. But in fact the article offers
+insightful comparisons between tactical proving and dependently typed
+programming style, based on extensive classroom teaching experience.
+
+The book SF introduces quite a few proof tactics and it was not at all
+obvious that the same material could be covered perspicuously and
+succinctly in Agda. The examples and discussion in Section 3 make a
+convincing case for the pedagogical effectiveness of Agda for the
+toptics covered. The article acknowledges that this does not
+contradict the effectiveness of tactic-based proof assistants for
+larger scale developments.
+
+As for the second finding, the authors acknowledge that the idea seems
+obvious and can to some extent be discerned in prior publications and
+online documents. But it does not seem to have been explicitly
+presented in the research literature or textbooks, and it clearly
+should be.
+
+The third finding addresses alternatives dubbed extrinsic/intrinsic
+typing by Reynolds, which to my knowledge have been viewed as each
+having advantages and disadvantages -- thus tradeoffs to be considered
+afresh in each situation. The authors make a convincing case for
+intrinsic typing by comparing well informed formalizations in both
+styles and observing that intrinsic is in some sense more expressive
+and also significantly more succinct.
+
+The article is very well written and easy to read. While the
+experience report style is somewhat unusual for this particular
+journal, there is substantial scientific content and the writing style
+is effective in conveying that content. Indeed, it conveys the
+authors' enthusiasm for Agda and my review was delayed because I was
+keen to get experience with PLFA. A previous version of the paper
+appeared in a conference; this article adds substantial material on
+additional chapters of the book and on teaching experiences.
+
+Judgment
+
+This is an excellent article worthy of publication in SCP. Below I
+mention minor points that could be addressed, but significant revision
+is not necessary as the article is already well polished.
+
+
+Further thoughts
+
+Apropos the volume Verified Functional Algorithms of SF, it makes
+heavy use of tactical automation to handle large case analyses
+(hundreds of cases, for red-black trees). It would be quite
+interesting to see whether at least the simpler algorithms can be
+handled well in Agda.
+
+[NOT DONE. Interesting, but we don't have time to do this work.]
+
+page 8 lists logical relations as one of the topics not currently
+included in PLFA, but on page 8 under Adequacy a logical relation is
+used.
+
+[Clarified by changing "logical relations" to "logical relations
+for parametricity"]
+
+page 11 mentions not finding a proof of determinacy of reduction. The
+chapter on Normalization of SF, by Tolmach (Norm.v) does so.
+
+[Thanks! Text updated.]
+
+page 12 near the bottom of the page it explains some notations that
+occur on previous pages
+
+[Not sure what change is requested here.]
+
+
+
+
+
+Reviewer #2: Title: Programming Language Foundations in Agda.
+
+Review:
+
+This paper has an interesting structure: it focus on the overall
+structure of the book "Programming Language Foundations in Agda", the
+choices made and the advantages and difficulties of using Agda to
+construct this material (with respect to other tools, in particular
+Coq). The technical details are mostly about choices and style of
+formalization, and initial results of the application of the material
+in a few courses. Let me start by saying that the article is very
+pleasant to read: the style is rather informal, but very clear and
+provides the reader a good idea of the mindset of the authors that
+lead to the choices they made, and also the influences they had along
+the way.
+
+A little context regarding my backgroung, to contextualize my
+comments: I have been using Coq for roughly three years. During this
+time, I have made several exercises of formalization, including the
+untyped lambda-calculus (with explicit variable names and with
+deBruijn indices), including the Church-Rosser theorem (based on
+parallel reductions) and normalisation of left-most reductions. My
+experience with Agda is very brief.
+
+In general, I liked the article very much, and I would agree with the
+majority of the claims made. The appointed topics below are mostly
+comments, suggestions and some comments on a few claims that I found
+slightly exaggerated.
+
+
+Section 2 ---------
+
+There is not much to say about this section, since it is an overview
+of the topics that are introduced and proved in each section of the
+book. In general, I liked very much the choice of topics and their
+sequence.
+
+Page 4, paragraph "Part I, Logical Foundations": suggestion: (briefly
+explain monus: the operation is known, but the name 'monus' may not be
+as common)
+
+[Not done. It is a standard term, easily looked up. Explaining
+it would expand the text more than warranted.]
+
+Page 7, "Discussion": it is mentioned that SF starts with STLC, while
+PLFA starts with PCF. It was not discussed the reason to skip a more
+restricte, normalizing language (STLC) rather than a more powerful
+language (PCF). Could you comment on the motivations for this choice?
+It would be very nice to be able to speak about termination proofs and
+logical relations at some place (as mentioned in future work).
+
+[Added the requested comment.]
+
+Page 8, "Discussion": It seems that the author claim's that the
+substitution in PCF is weaker because it is only applied to closed
+terms. However, this is a choice, since it is possible to define
+substitution for open terms (only it is usually not worth the effort,
+since it is more complex and involves alpha-renaming).
+
+[The choice with substitution of open terms is described later
+in the paper, pointing out that the code was too long to include
+in the textbook.]
+
+Page 8, "We'd" => "We would" (suggestion: the contraction felt way too
+informal...)
+
+[Fixed.]
+
+Section 3 ---------
+
+Regarding the comparison between Agda and Coq, some remarks:
+
+
+I believe it is clear that Agda's syntax is nicer than Coq's syntax,
+in particular very familiar to Haskell programmers. I found it very
+interesting the usage of "--" coments to replicate the shape of rules,
+mixfix notation and better Unicode support. However, I although I
+believe that it was not clear to me that there is a huge advantage of
+Agda over Coq in the following two aspects:
+
+-> notation: Coq's notation system, although not as flexible as Agda,
+ is quite similar in terms of effectiveness: duplication of names
+ seems like a minor inconvenience, and would not affect the
+ formalization effort in such a negative way, as claimed by the
+ authors.
+
+-> style of proof: it seems to me that proving theorems in Agda feels
+ like programming more than proving in Coq (due to the distinction
+ between the languages). This does not seem to me as good or bad per
+ se: it depends on your objectives.
+
+Although it is possible to construct the proof term directly in Coq,
+it is not encouraged: the tactic language, although intimidating for
+beginners, feels very comprehensive and powerful. Although I agree
+that Coq requires an interactive process to be understood, I was not
+convinced (by the arguments given in the paper and looking at some
+more complex proofs in PLFA) that they are more readable than Coq's:
+it seems more a question of preference of style, and desire to use the
+same mechanics for programming and proving. Moreover, Coq seems to
+"hide" a little better than Adga questions regarding the definition of
+equality (you coud hide this at the beginning, and introduce it
+later). I agree with the authors that Agda exposes more directly
+Propositions as Types and avoid some duplications of Coq.
+
+[The reviewer doesn't ask for specific changes.]
+
+
+Section 4 ---------
+
+Nice idea. (no problems here)
+
+
+
+Section 5 ---------
+
+Page 16, line 45 : "and and" => "and"
+
+[Fixed.]
+
+Page 19, line 34 : it seems that the comparison between intrinsically
+ and extrinsically-typed lambda terms is not completely fair, in the
+ sense that there are two main modifications involved: => explicit
+ names vs deBruijn indices => intrisicly typed vs extrinsicly typed
+ terms The authors comment that there are actually four possibilities
+ and comment on some difficulties with the other options. Did you
+ consider introducing and contrasting each dimension at the time,
+ rather than making two choices at the same time (in the book)?
+
+[Rephrased to clarify that we think only the two options
+we presented work well. The following sentences explain why
+the other options are problematic.]
+
+Section 6 ---------
+
+Page 21, line 21: "Similar results were achieved at Edinburgh over the
+previous five years".
+
+The presented data seems to suggest that the distinction between the
+two systems seems more a question of style, evidencing that it is
+possible to substitute Coq for Agda in this scenario. However, I does
+not point towards a clear advantage in either way. Maybe an
+interesting experiment would be to expose some introduction to both
+systems, and try to measure the effort of doing similar tasks in both
+platforms.
+
+[The paper includes a suggestion from Nate Foster on similar lines.]
+
+------------------------
+
+
+
+
+
+
+Reviewer #3: The paper proposes an alternative to the textbook
+Software Foundations (SF) by Pierce et. al. SF uses Coq, while the
+authors propose the usage of Agda. The authors claim that, with Coq,
+too much effort is spent on learning tactics for proof derivation
+instead of learning programming language theory. In contrast, Agda
+makes use of no tactics, but its proofs are not much longer than those
+in Coq. As a result, the new textbook Programming Language Foundations
+in Agda (PLFA) has been written and applied to 3 courses so far
+(Edinburgh, Rio de Janeiro, and Padova). In addition to this
+contribution to education, the authors mention two other
+contributions: the insight that a constructive proof of preservation
+and progress automatically produces a prototype evaluator of the
+language; and that an intrinsic type relation requires fewer lines of
+code and is more expressive than an extrinsic type relation.
+
+The paper reports the development of a solid contribution to the
+education of programming language theory and an alternative to the
+Software Foundations textbook. On a more scientific note, the usage of
+a constructive proof of preservation and progress to produce a
+prototype evaluator is a nice insight not clearly described in the
+literature.
+
+As suggestions for improvement, I would like to see few comments on
+design decisions taken on PLFA: (i) SF begins with a minimal language,
+while PLFA begins with a computationally complete language. Why is
+that? Apparently, I would regard a minimal language more pedagogical.
+(ii) Why lambda calculus instead of Hoare Logic? Was that decision
+solely based on the proof automation limitations of Agda or is there a
+pedagogical advantage on doing that?
+
+The text is very well written.
+
+Minor fixes: Page 14, line 41. Introduce a line break over the word
+"progress." Page 16, line 45. "and and" → "and" Page 20, line
+50. "Question 3 give the students the the" → "Question 3 gives the
+students the" Overall, I would like to see the text using only the
+British spelling or the American spelling (but not both: e.g. flavour,
+behavior).
+
+
+
+
+________________
+
+Data in Brief (optional):
+
+We invite you to convert your supplementary data (or a part of it)
+into an additional journal publication in Data in Brief, a
+multi-disciplinary open access journal. Data in Brief articles are a
+fantastic way to describe supplementary data and associated metadata,
+or full raw datasets deposited in an external repository, which are
+otherwise unnoticed. A Data in Brief article (which will be reviewed,
+formatted, indexed, and given a DOI) will make your data easier to
+find, reproduce, and cite.
+
+You can submit to Data in Brief via the Science of Computer
+Programming submission system when you upload your revised Science of
+Computer Programming manuscript. To do so, complete the template and
+follow the co-submission instructions found here:
+www.elsevier.com/dib-template. If your Science of Computer Programming
+manuscript is accepted, your Data in Brief submission will
+automatically be transferred to Data in Brief for editorial review and
+publication.
+
+Please note: an open access Article Publication Charge (APC) is
+payable by the author or research funder to cover the costs associated
+with publication in Data in Brief and ensure your data article is
+immediately and permanently free to access by all. For the current APC
+see:
+www.elsevier.com/journals/data-in-brief/2352-3409/open-access-journal
+
+Please contact the Data in Brief editorial office at
+dib-me@elsevier.com or visit the Data in Brief homepage
+(www.journals.elsevier.com/data-in-brief/) if you have questions or
+need further information.
+
+Note: While submitting the revised manuscript, please double check the
+author names provided in the submission so that authorship related
+changes are made in the revision stage. If your manuscript is
+accepted, any authorship change will involve approval from co-authors
+and respective editor handling the submission and this may cause a
+significant delay in publishing your manuscript.
+
+
+METHODSX CO-SUBMISSION (OPTIONAL)
+
+If you have customized (a) research method(s) for the project
+presented in your Science of Computer Programming article, you are
+invited to submit this part of your work as MethodsX article alongside
+your revised research article. MethodsX is an independent journal that
+publishes the work you have done to develop research methods to your
+specific needs or setting. This is an opportunity to get full credit
+for the time and money you may have spent on developing research
+methods, and to increase the visibility and impact of your work.
+
+How does it work? 1) Fill in the MethodsX article template:
+https://www.elsevier.com/MethodsX-template 2) Place all MethodsX files
+(including graphical abstract, figures and other relevant files) into
+a .zip file and upload this as a 'Method Details (MethodsX) ' item
+alongside your revised Science of Computer Programming
+manuscript. Please ensure all of your relevant MethodsX documents are
+zipped into a single file. 3) If your Science of Computer Programming
+research article is accepted, your MethodsX article will automatically
+be transferred to MethodsX, where it will be reviewed and published as
+a separate article upon acceptance. MethodsX is a fully Open Access
+journal, the publication fee is only 520 US$.
+
+Questions? Please contact the MethodsX team at methodsx@elsevier.com.
+Example MethodsX articles can be found here:
+http://www.sciencedirect.com/science/journal/22150161 Yours sincerely,
+
+INTERACTIVE PLOT VIEWER (OPTIONAL)
+
+Science of Computer Programming features the Interactive Plot Viewer,
+see: http://www.elsevier.com/interactiveplots. Interactive Plots
+provide easy access to the data behind plots. To include one with your
+article, please prepare a .csv file with your plot data and test it
+online at
+http://authortools.elsevier.com/interactiveplots/verification before
+submission as supplementary material. PLEASE NOTE: Science of
+Computer Programming would like to enrich online articles by
+displaying interactive figures that help the reader to visualize and
+explore your research results. For this purpose, we would like to
+invite you to upload figures in the MATLAB .FIG file format as
+supplementary material to our online submission system. Elsevier will
+generate interactive figures from these files and include them with
+the online article on SciVerse ScienceDirect. If you wish, you can
+submit .FIG files along with your revised submission.
+
+________________
+
+For further assistance, please visit our customer support site at
+http://help.elsevier.com/app/answers/list/p/7923. Here you can search
+for solutions on a range of topics, find answers to frequently asked
+questions and learn more about EES via interactive tutorials. You will
+also find our 24/7 support contact details should you need any further
+assistance from one of our customer support representatives.
+
diff --git a/papers/scp/reviewers.txt b/papers/scp/reviewers.txt
new file mode 100644
index 00000000..9d04297e
--- /dev/null
+++ b/papers/scp/reviewers.txt
@@ -0,0 +1,11 @@
+Benjamin Pierce
+University of Pennsylvania
+bcpierce@cis.upenn.edu
+
+Ulf Norel
+Chalmers University
+ulfn@chalmers.se
+
+Greg Michaelson
+Heriot Watt
+G.Michaelson@hw.ac.uk
diff --git a/papers/scp/PLFA-submitted.tex b/papers/scp/submission/PLFA.tex
similarity index 100%
rename from papers/scp/PLFA-submitted.tex
rename to papers/scp/submission/PLFA.tex
diff --git a/papers/scp/SCICO-S-19-00290.pdf b/papers/scp/submission/SCICO-S-19-00290.pdf
similarity index 100%
rename from papers/scp/SCICO-S-19-00290.pdf
rename to papers/scp/submission/SCICO-S-19-00290.pdf