From 6300a449ffef72d5901c05ab0e3bc97bc223509c Mon Sep 17 00:00:00 2001 From: wadler Date: Wed, 4 Mar 2020 19:16:18 -0300 Subject: [PATCH] revision of scp paper --- papers/scp/PLFA.tex | 42 +- papers/scp/conflicts.txt | 46 ++ papers/scp/credit-author-statement.txt | 3 + .../declaration-of-competing-interests.docx | Bin 0 -> 9120 bytes .../declaration-of-competing-interests.pdf | Bin 0 -> 30669 bytes papers/scp/determinism.coq | 55 +++ papers/scp/determinism.lagda | 24 + papers/scp/highlights.txt | 6 +- papers/scp/response-to-reviewers.txt | 437 ++++++++++++++++++ papers/scp/reviewers.txt | 11 + .../PLFA.tex} | 0 .../scp/{ => submission}/SCICO-S-19-00290.pdf | Bin 12 files changed, 605 insertions(+), 19 deletions(-) create mode 100644 papers/scp/conflicts.txt create mode 100644 papers/scp/credit-author-statement.txt create mode 100644 papers/scp/declaration-of-competing-interests.docx create mode 100644 papers/scp/declaration-of-competing-interests.pdf create mode 100644 papers/scp/determinism.coq create mode 100644 papers/scp/determinism.lagda create mode 100644 papers/scp/response-to-reviewers.txt create mode 100644 papers/scp/reviewers.txt rename papers/scp/{PLFA-submitted.tex => submission/PLFA.tex} (100%) rename papers/scp/{ => submission}/SCICO-S-19-00290.pdf (100%) 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 0000000000000000000000000000000000000000..00d2187beac41918c3356623bf4c2eb0ad8b6e04 GIT binary patch literal 9120 zcmch7WmH^E)^+3BxNERr!6lFog1ftWMzzAQAuo091fXiiL{2rWSPm;qDbY0Du7?02sS~ z>|Ht7|Ixw$a2|emd{rbU$|HzkhMn9IiXX4ovqs2x`r_t3kH1CeR`Bq&-U(Lta(hB4 zF%_zY`0D#uM)*$L*d+nvduZV`!Al)JHWCQGAoT!N_T|+G`TS+n7#+2&U7><7u{zjn z&qQskDWXq_qL`Q2wLF7H_DMy4^!p(yYYT&>Bfeo}WGK(ag%&J}9W9efa2l+?|Faw< zY4Yg?D8+|uzePh}XmBw|{xY}!TmF;=_quoP#YyNir`L$*kT43wXFN)Ic&etgTtd*8 z`_rv*zW0{?cfNPxSEK<8>xUS(eJ@oWEeayd9O0)2!^zhN^xPYBpIn2Q> zAa*YY`~S5x4iH7V5D^@SlY8{E)<(xCh`JXk>O}CeCRO4~Q>IziA77FNym?ytULGRZ z?(@Za`B3kTy2X}Z)#4{r20>_|vul;`>W4B$KCC`c@o?d3J7`cI$tL#+g(rzmLqrHx zpfgQb%XrAhx1v}rd5CjZ&e=z+x9T%OZyBZ%iGZEmEEH1i+DcwbJ=zAIT_GZ@x-Q+5 zb8NqA#HP+WgWClMW5z@allGz2t~aU}Uq?ok-gIz7Bwx}aiJu`nHvS5d#1Z{q{MUys z&hN&XIywEF?OEev=-r$+i0i%|Xt!5C`rt6%wGd2Dm0l&-F9t3EhxGQB$Z`Duu|1sB zGgz$w5kNDSkSrmM27B=6`9iCK?BPn?*3}kJUMXcVbn~WW_4$s#WZ&}smC*{7RncWL&Ahg%bPVfL&{zgO$p5p31G7 zxt6g&dL~*7cuc_lKr}>w(eyitr_@TTyT#|=%t3(A;KHj*hGH;1vm=hWHW;)OOxcw;}GhEdTPp-Qf*}OC-8J)~wWS_)6tyliE%tC2K zZLmCnmO&2gY7ywjOO@}WAN*C{Z1}k?@)U0|Lo7L4d%{OGruYLRmf?9M67p9Sz1R3N z61abBNZ#YJVXJAYVol6JPkE6W zz2Bf%pd$}XF84_;;kS8?|*<+;D&#(dotjhd+ zzsE;sP0GQUfjnUF_o%dT!#;{P~H`g~?;l{%E(3t^j*dhIXu4;rO znFaj--;DD3WGC#tsltN70}4rz$o*>ZZZ#6`2PCnTZtj!Mi39dP_6&R3&XLcG^8{4C zoF!B2gGRNB1iOq=5SI6^Yl3A$#0@=SF_xr-w=^=uIz8CB`S2X5oA4{HHQR$ZKms=F zQRV@m!uJiDp&=54_AYM`Jnc|iZq-!lMwxpxB|j^L)dOxaXR9g6%2Y(eR)d`w3c^f> zgJcOy0rnsmHpkLIh3%p-g7*6<2{mjk%39`7tfEljiRFr@jqFb(!c-=f7VM}#o>7(u z+_jXi(n{h*G?TU6^<*<&HFhTCgNx`R~4~NV~f1GXqVb8PZkol zENl)^;K0@ZeV$ZIq{9Z?4+MSB@*%l3m41ps#C+ZGq#xUnK>?@7hr(A<-C27ZjkU1! z+gI24!T@1oTX!~$bfV&3yCfWdvJ)d6G7r~!?xa&O_f%6v+mLuP6ISaZe7&&c#&xvS9O!gZi2zjV|G*)p{@UVwyb9A!`S`c%RL0ZjRFYl^{jsF16m z!fdc=Rbz1zx!hE(*>;S|M}zcf!?@ItaSVZVOvd2Ep_@|+3K7E3X^g@64OxQ{KFZuz zkzWI`ntnxc`Wi^gf1YS^+OTNm#yt4mkEN$u(!epnQW=u>(b&jwbWH}X$S*ML({|8@ z9}d~9c^pskr*gd!^O`t3vM|aE04qq3|)@E)5sl3&FObKR72a&+$}s@k?+g7$r^B~T1nISZqYLA*n}er;Zb4^K!DiHFrlSH|5C{AA3XT|HRQ zoPw>W>!$aavF!_%a33rzyQsr8VTb+E?!FJfD2;=EK{tjn&wVFqAG21vVh!rURN@JXikK*fSn+ zNK3(i7EKf;PC|l|nc@>3XbTJp>|F=va=gt}@gz?2@~uJ!26KAbZizfr^)&YWVfw(y zLdtuAWd3yE_wbCYE=RoQfF?Ah6NhXY^jvl`^{~c^PUE!XUq-;Z4K$N>-B6qAoYEUJ z{3UIvZ12n{XLtrxyYup17bWl5c!Pnh`|9cJd`UuV#yj=(XEqIm=aDmQn9g=9-R`HC%NBeh1~M4rXryO0a%uwlHCC%ai;VRLx?D;duL{`B-Pn8r-)!chLbF35>Wuah}g3SmPxie)el5D1th zLN1S_M*J2NO&KN?MDN3Jt%aFAM@vBDg(-VW`3faTzb~nplfX7TOzy-I6iv$4RQ2_wh4{^yqncUUQ z+aBclcRYTiBM;u<$LTn!!g1SWi$5Y;nll7#G^65uRty&MDWYGr919nj)@tkQ5Ra?{ zsj6kNMOrqU^`*y(+gb|z0G23!_&^G5)M26ZqQII!F%9%);qFd#zJ_|aU%Fo3Z1xnH zz}O)b`MM3dSWNg3)Xt7Baz1sj4&T{+tmCtW^C&9ST$=cO`9*L&LOyhhlLlUw>MBLSG zf@<*WX^Cy9wtD3vqe%f&1D7CNT^0wJEf7@kx$6Ym)M7O)aGYpLfI`6gBN?jAaJE$B z`O^ZDJh!>GcCvHLaF!Lt^VV`+_j|{FB#BA! zB}K_mVNulfCp=Gb$&Cop0Q=k)!b|yXfI{KP88j19c*b(kbEzcgWi9d;??^g$ z!sxOqLo%b>9FXCdmSMwpVCpB(X842dI(IHCW+Q956PCiCF(uD_MXN=Di!LdhQ8n8U zpE5N;Eb`uqzLFKaYSqCy1F{-Eb(1F#>zP;d2$5_+vrXK=YaT${_UOS|Z?@E7=P4_Z zJU&W4>p{TJZ7`vFHsms!7wsOzb>;kJG=A44QtyaTj#;WU4fKQ^^;ISE&JID`fni7Y za@m%DJG}>NWiIJ$+IIp92oc%HZC#bwH1WP!8}YEAFo|UISr6jWST&c+1O{z#_7X#8 zXh31|5P!ga68CHSpB$Ri2DxA4>CSbQ_@BKm^%QJllE!0W7}o9&EZ5+XB@*b%c!mX5 zoXKrOaAJD5-+;xgUa95gPNDG5b}YA_af?Wplv=K{oAb4=kH9gUFB1(Z6oY<(>f;8N zrp}DN)eNCmM)&xIz=0UyvStvPg7}Zj6O|utrz$-2(tLZKgx7>*8T&R;NbT3G*3}Av zRQ&Wp>TRxHO?mTfiAsx60Da<5rOUP_(byEj!pZfY5O$_WfhGoZ116JZm!Z{z!8Ox( z9)c5dGwn>>>`0Nf14r;YqQ1nt zfX2m%<8f9;av;4K#~7k(o*TwQk{8C*7vy1!{l@i(T`b8^)iBU0g4s=#N?JETmbMYw zi)^+mIavQt!H&TxVGN$FQ47qr^hi#Mcsz8{7&(8RKy|NU*#Ic`VGexYe*xs39M2f# z`>0gs z498xX^TZy$9!UO~DJcOj$%0RnJ&`mN^|LD-va0y27esssW#T-wI)J6m2Odr(mj<*ou?@n=3&Pwc~sQ1>)`a5ur(@j;3~EV zIKuwTuiZq&(Dqw&cf2MYIi@G>(yxIEv_XhmF+E66-8C&|xw|u@0WS3#(0O{rnjT}5G zNrS`tpcGr@(N9_aj7ig0eO$&tiJYp<$-Pt_@QTDfX0ui0s{wV#Zzb>A*-9Cv7?}9^ zx$SWmTzzghiv)sO&UbQRi&>!D!PUKjjc?mf7#NirmyB5J$8P=W?k&d7%XHs7FVn31 zWgVJf<`^IIVLol7`MtN-WX_L2lInOc2zm2?yd<;$0K$JSwVO4_0mSjomg{dR%wWlJ zNdU)xtqKRaI-F2AkF`%AYmkp&p-(qt_Q58t_KQkVO2G`hai{n`)sSrZ({_^qWP2kl z!Jdr`6$-L9SNBgrb9{u{L)Xh5YY_XWbIv7tzn4w04ug)g#go{3FKH}I1$A4v^bv9H zCiB8`@qu_60{k2P5$5nuO!&;IafJF-bc5Qv3?RsJGD-nv*=EB=Vr82TlB#&ql0?U9 z!03!)HVTQ)Z(>LN{YWKJ@;Xf3KNp_k8Fl5LAII z3)G)5hKH`$&s$N%9805%eze~B_I*7A_l0uaX4L!bC!>6LjkSk9tQA6uB3QoQwf=B= zgJipM7lgp4`&IVp1hGrUxySw6jkRpnd+ER z>4*BR6Xvmz;z>PUJeEY6t#8{TXvv?W=(7+^oFMq9*h`~?| z4BD-{jd(5zNotl|)-5Kk*x!j+NPBXvs=nF(?x4M=BxP8B-l%+BB}R z2bdO}ytbR-fBOsUO!0fu zPpu<5Hom4cg{XpJjITLA>iGm#W@8scKjwd3^VILBI^nvshQ8>>Lbj(AvbQbjl*pP( z%pAJF(p$L27&Q9qx(Oj<;0`y4*Lio(vgRAN{~6utz$dY?&VSS<2_+BgRDR2)rD|G3 z&nC#V?{(LhIwMX79_|?Fs;C<~lCyTSJ=W#MPDPV>L8n#`@g%+Iwz@*NN4l4rL__PN zJ?nVyib_j=k2k5U!$H|(a4PILBB!zMetU5i5#JNJZh1Vy!*XT()X*oLD<9R`D&gDH zrvyB@GI&&P+ssaCJz8WMYf6dL-?XVOa5Gc-bD8nT)-C|~dG&%Q)o8~R!s7&ecXR6T9m!bs433TLxGTPea90~0+%=%K4_u>ch))#t0 zU2O??jLhJcIZF*YT4td$)kH3fok>ImZPn6iE!vj6PsiN_Iop+|A2`i56Uz+K3l>uI z7{1mJrYujz##BHVC!l%Ob$&3sqh5&@)yKp0dz&tUR}&wKa(eaX5l|+S6nAU%wvpGP~oG<5a?K9~n+pLrYAReO+U+IZu@6wN{DZm_Sbi>{Z}rbV}?sU=rU%C%H;{ z23+=DM$m528fH$}4bTuMbr4TWQXvg7sizWrJLR*D`Y=HEXut(A|6(xSSWwRxWp8$@ zF7JX(gLU#4b`lU$b;@|X%ka=N+nB0Q3%(Wg$K0or<}8k-=*kgxK@7ef#QkG{gYpZ9 z`Hd2+%D=P|CV0E``Y|V`%;+j9K5%j%!oRAo|IBi%L8cZUm%rtR!o(q^9!{LF6CufM zgeHDwG1Rn=?HWjqGNC9=l#Dgiujb}ucbB#f#blURh&k%~ct)!Fz-)qd%VM3@d{s)nmy9vlyPKI3>EVR#>tv^99~e6eZ|# z%|ybcvT<2nPV*YmmRVlwE@(X=ue^Ph3{6#9#8rnC+Psp7!>B(gD(SNO0CGy9pU&(c zLXOKymXU3itHr2V_2?n@m>DuoiXhYDNlqZ{;trZ(o4I6u0q+$=@7OcWooKEyoxb@l zu&0u|Cwy_m?+@N~?C3`NukEk|gWdkWZpYXwDVjNfNM`2tCSC|7N2sMEQ0x8r2pr!J z(s1Nd=refYaioJ>Po-Xl z&mThK%hGu9EfWh0#KcjC<>VpjPp(+8(l1d8*sR8zVVXX2df^44$(3GA&9a}8wd#nD z$v*o*)Q8I7+w{S#Cs30qZPGd7HF_1T4iNQ+l9U)CEY zxCP|#Y?O>K5C+HP3g`_O7DBbbtsB7By=@LT31CH<+)$KB+UMOAo1X-faBU)ZO{P|9 zLtIQYif0m^O~1x$h#xt2z&(CC4$J4+Jsy;*nTLq=AHvMPY5*WNHycN*zpVnqXpA`G za}lguvC>wVOerM@i>MZ9=Bv4j!ZC*e%{E2_c(jBXLB4pj8bhcwRALcGIa-rI4E}Ol z(p>a+%0qsE0dNyNK!<|Tva?q^Mr#MI%C#+byfiVmcz8Vf!Eyf{Fe2%GKT@NnOe zrmoAm>F>>S@oGd#Kz$JqBbpx$Yv0Rk#$XZ#l}b)XF$0PMy~=`$gb{on=eH3!c>#^) zSTrsCsug?3z+1BK!5WiF{(TR%;Vyde;=F<$WCV(w+btF;ZOv%B&GY`RY2Z`4njo-Bzb#I1w`N?C zEWlzx(`YgOiUc%~`$BVgMX==F_ycvGJDZQ4qr5ybYnDEi9|IIFmn}FHE{81`pZ+wfRd>B~s0kp} zb)F^xFj7s*YpRS+>~hFY1jip(ayV&eo|NC5PmI$=MaD{kFqxQmiZa` zK-&WB+O78tcV#82iltHFev~@Aw!H~lXVUuiDLF>$AclKa`Y7El)u45A7=Rqq5It6j z?OJ|R4LjGOYAIyBPKNx@+P@{(O^F>V|C z1zhbO6uVJYrXS?*8!TDz1cWX4CUNxYC$~8NQfG&G=dPb!ec&_MpxlS3#+_|l=Wypk z^_W!#_>ex7wZo>uDp%SU4j6y8xmTx_%TMvrzo-IAxl^kAMU}tP~1ZggJI{MAb z22W2uFQFN!JC@s?lTc_zc6UH;?{g-3H|1YBbS zQ0K2IKM$nGYo}vyHeB>TiJcEJ9{$7H>5D(4s1NF$v4*!3$kp)gGN*>*k$;-YOfC+(ILk*?r(xa!UmVU>Sv5e=xa#h`H;dTnA zqM$D_3ek3#QAqys`SaZXdF(IPcyo#!W6d^;MgfygQ$`IJ#s?_rau#(H^92{{6 zyojdN(Mz57DeCQl!0oJ;e%~V9NV!hNb(DXcJh6kUEPALQylS9F#9}y-)-=*%_7v z^`bs)3X^xsouzE3+SP{h^nU|Wx(?*w^umQHd3~YYdlPc(?Soq}I+xIJb>?!8q9P9m zFZ{5p|NDi6hv7%pZ?7l(34AQt|BfPjI6VI);r|JLEPMYB$9o{0|G@te!T&@*mYIJ? zuRoywOLYDd{PAFZlnfbpHu{T*mnw{0sXp@S~#6pZLeMiQn;7xPRgQtW^9t z#p9^;_bK9t|C-{r81_%};~?vIG&Sje4ERsT^(XpqOz=Cp@_!${N6butO_}}*HBHy=!c4&IV$Lr*4w6{93{6I zR)S|`_JBsz=DdA9k;u@d-2LxfpGp$qF2Y3m+|GccZhqa$^jIV{t?KE+ zK#$O+6(ot-q;DAI(x{uiD1YUf?l?GHIj{k0n}@)Pszku{uKSxpno<7gph2Y3q{qog z{`6P#omm>ufH=|`xXskV)1X9`1OTvb%)%7XlI`anr z6+B_gN7u5-8Q&giKfRii!q4a+Pz^{-X18TNB<>GLao9dDNO?1fIOg$iQJkZm5c*~c z#SD3cp$Oy;bz5#oB!Y-X>q$L=G(j)LRXRtkT_BB0&MN|`=`je+BwqspxuOSVegcg|12K-|*U7Qg_Fa8MKj#{!qYM~}nT zIRRfF@;yd)8D{Zl-S~O9U zejI+15cnME=USaE4gwL4&-DMmM5J(_G4v6#s^zpCb{_}B0v$h^>r3~|pgn3NW>;6wL3Te>_my_x zWNDmT6yUre$_Xm4V_W7UUrtT$w}QT9G)wmD_oKGKxspunKYQny>t+a9{E83cb(O^R zHZ}p-%czlPd9D`HEF}`DF;;|53OoLZRNKme&$L%Owo3#>|Pd^+ths) zAGmC`y$~$r2Kqs>?VNXQw(ACp$t`{NzsaKndJ(!SLZkQOWo6yZ1tm<~w=ZTs^21^#lVu)@%6enBh0gz3j;$G<1Srlp+_KQ+pgA z9_!X3)vSKPf=VR=bG?J)Uf;5OU_B6Ernyzkj5_s_2hU}GS3eSe$TD|9&Ga>|nc3X> zw25&??fF*<&*D;-y~-QeFAh6+mIKAMZYU1bLfAZ;qOoVAR1`-(I{4Qdxi(kR$N%PK1qI>O(wDHI_?C4=m|$-G&|5Zx0e(x8n||Q zp(7H0$Ovm_W$=fa0Pa0|muHvq{7p~C%o?E%l83+Se#4Gm0n1*}~FnsmSd7J3E%D?5W0EYMT^ zQP1;zzdW3rowdHAp#wk@SecLrfL6)S#Q~rNpcS;Xu(ngQ(bYEuJUc=`dwKxt5Ai%a zKnDn{@kguigyIDS}*gyS$L_ z#zL4m%uy-x*<$iTkNVQ=R_)BJ@sY<&1Bl$cFT_^|HBfJ+EH#wFz4o_A$OD~MU>FFX zaB84!D@H~TqSr!TllRTsNlBl?x+^aaX}k>@=crocNbIMdygm}J3KBtrzzR>XaCwrT zZ-B)rR(4@BJVErI$B{Dx&@-TA!DN>ZtaX-KTo!CnHufbZkgR86sSjf|F{Ot!$}J`n zujGV5WW7x!UN+8ghcawd5>E!%xFVaFxK5Pv1BZ7iocZXyK7`_^jE2G+`33osLW6^^;1Wg*9YYZ3NvTP&!Qa+DGJIV z6PC$`h7OGC-D@0gMjP-&0EnNr7y@`aIE@&XDIdfaex7e2u>ADjK%G9A*?>&?xQ;@| z__EkQzJ*Y2du{XbmA5D#Y(Tpt9q6KuDKs#Qpl0(IMWN-wCkad=U~53X7vz^?Ljms+ z430vG=DQgs`Gi67p(smGj{BU@0jmL8>%(m()F^-n@&VMt4>1vJLihDIkQ(pV3Qino z(XRu`LN2JOQ0Q%QD-v~RJaDyN(O0mKL8$z7zQ#cF^+JP>iKszip9l#=sS$x9;+uaY z$OS7DPL6`h#jXz*`)Iok4jGuGn}~tdjky-69=4*VqC2f8K{u7CpQs{*zR6;Q!02=1 zo2NJRIbV&mgx3j%1u-R@x>My{oDFjSTUDD)WXk% zHG1!Lyj~$WacQDhL^<+>Z?`|zbH{Ii^}_MOU5do(ZY7O^(SR`bg~yKv5Lpl@Az(po zK|lB*er1yP`6TN=5P+OlOt82}w(_-J0aSTYh6SqU6rfms=LiF&^GeD4MG6kdO_np7)FY)I3P zZ5Hy7@SqiqVN5tnSnDf|DgJ04x0m2XEE_wM;GCdClR>J3?U~N?PD?omwdw0#KfSDH-6V@0OdB(I^ zKe9G5$5L*p{nSJrcSB)C;T}g2XA}n-7g;2wY(0fCl~!a~Bs)oGMq;LGHfwe_MN=F; zQZVA2K9Z)x^t65-xLeT>>{@qgcG0oRy&Hp-jMajLiKUE{z|_r*nQWEZm%Nd@#ne+} zqVcjCLSsW?t6G~bF6nSk$%wczls&7o?4W>pj3;-Yn7dT}Q>B`5j!fk+vQ{*WCM$pK z+ge3u0a-~}HCml=`J*fz`Ha$x+*Z+6O|Sm8QNZ_iq5LWBpRz)-T6NQPb5`^Ti#`^Q zQRHakaCWol*Vu-f@T_T)R0OAqM~jE|Nh^MvTvU43Fj6)0%6!v=gsGUhu_wD?UR}LJ zWIB_*gR9p)=Y7fzbSE(z{P?&zVo16=}};jX?pIFU8_c}yYh zZLib~pMd*uAAUWY^YRt?G5RDmhTWL$N*#{fM;Zf~FdY}0tV!j$ zxHXNv+d=7>@GYlK%g%*w+_MjLca-pw@E=7(dtwV>wy;KCY6m5htA121uZ_OaJ2E>e z;Njp2<_YIPZgFZU_MpAieE@rKx?MP%Io`URxs!!pgD8R7hRuZ#flz_sdC35S^uiIM zqaC!p(HD<)T!-lGBpR5&y`Ymn7Yy?&E!10k3>qq?5|aJ*b;>TDF3u3tdcs12osD9V zz2m*2q2XwfXwD*iqFusMqSC@{!U@8X32Id8mFps58exEZZZte>R5v0gyTYsS1k0e*Qs~jfS8GC47`ip z>ZaTZKhe52y#EN1;P=IEOempKD_CE=OdM5w4NR85dfD-d&Z*COVQf@v4mo4tSmBVV zU)6QhgaEN_NCl-9BR6R?Z3j~honS-1>C~YzayH-CM=3IUb)&|_h)1alu`r?(;t%RC zE6u(v8jBic^ve$-Zl13vuUieg={xJY^JF$+c6Kywae556Z)ZL;&yRzp&GArk13qu01;! zgiqr(rpN2-dz$W4A6Yi<*i=5mua!o$yztn%)w-iyyln8;hV-BkT(E4=^J^LRQ zJx`y1&gK;z>>TwSl*%K=(Bz>hkB^J+=p^qt}79Gl_i^qS%4Oq}7zngN#K=UklOCyv4JbKSu3bArwA zQw4@+brk@NKc#2^e$(lPM zKilZv>cjXqInRyrzte~5Z*qP|jQ(Yx{abyQ|0d_xn(%*G%zu9_mcPmQeKqxerw{Aj zFky|87M6**+qs#*TK+3+7(~>o;QrE+GMAKUTNTOJfG| zAH$Ch_BT8KVf+74Pciy`EgNX)f3x&|8rJhd-u~Y$&7W7>j=&KOlrCv%VE;Ure+)*g z-bS* z&o2}Fr2?&*x&}}eAb(i=Qj(`e4hWGOBmVMe_Ri|5{Se6)ipmF=I_?|+^&B$-Or|!(X|8)fPdH4 z7P`jvKN{`%RsrBZfYqd?rvnBZY9=;%AY{YH0<>gib|C&E4zw*(eSRxr3qzn%wEXt^ z&oPIU6}bOgX%+I~_TrLI# zh**KLoQ!|;5`YC5rGVY*^7DwEnGSgWvtmG;-H-tm`25ci>9-d6eOUd05;6XPGW|RR zf>Eq&&qDqSP~W8iDP-T}->;bvK3{r<0zp)GOw9 z3cCTKS#W+JB&K3>M1G^9Xp5AQOobK&LVhG0c~$D{qo^wS4$t) z^fJ%c^c}tuF+b!a(3lwOX>60Xh+2AX0~#N7y0T`42=H z``C*Xk=r3TAom}c1!qblx08*$O%5DCXy)&wu!5U>hr0DBCcLrvXs`o9EaZ?XI?i0- zdG;D{VUqugyN&*mLrZX)hrdlXlzU^SLiQ2>OaAnF;W7y)exNK7q@=IChp$bigAeWzEF(Y) zp&j-lGiU!bduy99z)}VF9?a`SeXNUVmX09uU?7;-i#3Pp0)U58bvEN zl8iXm%l3iq-uLTP8P*A-YSuMDoLg3jHdkfTX;0VI7jT?lV=Yk7Jhc-?Q@l9J!B#VJjBNoFU)$8Tl zc_?Iv*x=WQV+kj0j~Ki7FB<``kJ3$g2?p!D-p-4!E(-}7scU$9>4YGYGGH-SWy?w6 zhkp$Lsgbmr(khxNLM_r$j-Zf?E3^Bgpd?-d;h3sX9w9GUSZ!9VQHVB~iZu!2b9|JG zW7G*F!Hq28!~KH2Y)dT__Z$Ll3WqAd8_6jtz#PeZ6%B)8m&np} zCWz%JO?rUyzQ-c%kpK;5j)S)E=}G9$ywFK;EAEcN9d`S zqS0eNhnlM6aBIR%_2M<%&fb-^?WNm29y|BtXO{ZK)crWB#-Sa|4{?i^5uf7}T8*2e z&CWPH(uadptUIFBJr2@#irep;Z%@B;W2xzs+BLI#Q0vZ?mXs6!_){rVKBOe=X>@u| z?Y)YEfg&qVwn|e0Q~eGcIwS8GGA3(dMHYqDn}rJ%?sQ$9KF+_E<{j8QiqbKe1u4`C z5{}?&HvAyrW9%wjmL@oS7jRG6MNm<&a$c&hTI}pY~De`@9ufUEK{L@5cht^2g zQ~r%(ei!rWo#O<#mpL|A${3L~$1uHt3l4aGf*4(;u#x-(OdYkRs~1+a9HDGUoz07~ZhUuWymp<{t+$w4Yn0cj{`f0AUu(cF z+dPihxL(k9Sg#O5f7Q{2eetylBwC>@67^{>3)y&DxWKYu1~Q7dfMZso8hb z!ex4u4C=GF8fdq=+od*EE?(Dwq0nF}bc3%OVN*Xp zl^QuGaK+Eo)=YJV+{Jk<#gkyYnh?mlfd^cO^S(3{NT?A1MiB-J<<}8n(B94{b;}e(OTfw2PjKHeta;UR`^2`z>*s zEKMaxg&Y-Z1i!9%xIw#-w|Ry(mlGSyF6r=G-uEclPrEfOdeT)vOl zUP9ty^thDxWRvv=$ojT15awiXZlf?f5dU41WdD5-3C_hX=x`Cev={et;}AKs;KsZ-e^del2* z+R&Q@&ikhFiIIyhJg?Y2D<{@ipXNA&y%bwR-doobO^oDC-Q0@q-76gN5Tq40OPwtU zXiV5~G7lW=?jNtwfc5b8ek05Y+Q&C--rM&KubgJ5YbZ-#3!ILyEjGB|aN|z%G}*(b z6+=_+bIcH%*WLgq$gI;0YV{h#5!$*5wbU|3KaP`=AlGI*zUj-a!PJhrIIti}^mM~> z6nKj;ZFjj%8#vZtmmOIqlPh0F%oTc%lZ2G9shZ1tdrvq}pnDC;HL*PXzMC1XxXE%H&75rrXtVrs$$H5)?DPT;&Th^pmih}61wB$ zq%2J1nub%(TFptD{MxXCCe|;0qo_o-v>=otVSS)By@Gc_bVDpl`cX#2y{NjwD`da6 zGDZS*5J23yf57QmA4P|5py(-|i|V?CnMJ}ODyp6`z?lm7R5&)4D_^rqz|qVzA{~{F z4AvGx7XZ#SF5xK7_C}mx1Fqo1J4XhY&_3^027v38ea>~izU3T#%!Bw^rHd7Z$k@+O>sa-d*Nqo`rMx)?fVx`0L_jQHq#n?gL? zq&26N5YEkFWBJ90i`c8dSAKFjg2!$K{pHO9u~*t~8!ZFb?o+SE)nl&^H3$=a*l#~>#5$9`9`;Fg6y9! zNEgVfuCG3>sJIk~Lm4_~XU5LS^~pNDD*-LVnL%7NVTYuPJd_{o5PS>jOnOCig|E|h zv^4_T{FR=feM}r?)cGLBVYkfpMYLd6)fj75=9iO9WoVZ4trD!f{(yJ#<`L|W#XC%v zeFlyLN*72ETT|4xg=U`$(~FF!3sU)x3mf1mJjde9)u3 z$N^=fN(gCr6G-70KtWhUXr(o;vV!KRgb~i!hKB&x$=xYxKPw_#6UV0=f&FY&HE!X=z+6uYGEHU+1A5%_0O0WmS#@`uatB%6JzYrwG*B zP^W!UeOM$wjSKY#LIz2i2Ps`8bISS@8g52w!E%G)xmguoY1NH(xj z4JooH9oEV%4zu=&Z|aZUf3Y)dW-h5v){xh!p!{H8|IUtmNDV|5VK78SLZ=q39EVR*ZmQc-L-grcpysk(@%!M8$+yncRLQACd&Y@|VQ z6BdqBx(^Z@iW8EXadGio_SPhEsA5`})dLibM=N+5$sDZ(#k`!t*sx~1th)D|Egm=- zsW`4I8Uw1;4%Uw=UQ3m$ya9D=ALNnqSdFWgX>ghjkS$B9E#z(GHHIt~?)LV)P(zYy z>$n&>=H!z|HsbGRxJMjNu}73E9L(md;XE*JPiZl(b}*HQ0;20;&R&{Zn=g6_uBErfak6A|p3;u_Zur0-2U!r_ ztk??>hf9kyCc(l>ggfpoz&NigXz&MP`74xHu#oSbhhL`Hs_t9K52U!*H<2&SXIil^ zr(l;Z9z=4(btQPEmI2Y$Jvq@ zPjaD&qh+?1mfi`+3SP}Fp^*uzC+u2vc$27Ww96$wAvm83zlps{5tPQ*DfL#^b3{oO z)MB??nw!rlI&fG)gV-phpFdJhgWWI;-n#RX;dj@I^vVl`ric^7_yd_HtWaX2I-|+lOf0@v58Vqv&xWYSodOheU$nXqT4rtGzOlr za|JFRRUX1$o{6uuOE2>I<*j#=eO# z9KXqgWFV8x#Vc=-&7*b@F>l96_R;2O3`^`@zbOm}*;OUkahW@#VTax5eJx)kBrF4r_5-XqoZjTflPPP2&sw}Nge>Y+kKoj3W+0eVm-$d= zif=94y#r|N{Q7xRb2|vaC!#`dspS}A%>s`*qMwIdI%Er^8g|+SQUjt(s&XBy0GpaB z>S2Ct6mPT}2ScMX5jH`|Op|<#!Ede-o2<`X+=UQ> zD2aO+Tn?y}N{gVPt7+=3hcc%K;y(Sdu7(rveu6SI8;+1Yb@i3!dG#o}{pImNUSHN3 zhK|a&&u*oo+)hRmagFAN+IQ3b4~lEP4t3n6@dsL5lhHbCMCTJ>DW;H`xl)XgyPvq_ z-OiiXIq03FnaXX5Nj^E0VQA@PCsQ(OmhLKi=+b+=eB2pUIKUG#-Lg+tJj-Ik{kFA_ z_z1M{i?f4I2ORO)w~3&6QP!m<%eljaxw@v&o~*0wM+{^WaZNhi-3{aJNE}RTPCEm4 z>23bECk2t8DbF+T?2(4L;0VrrN2SqfuOW`rc-y-~D8bce)mN3r`pHVuE|r7V!kGl$ zhS3oAN56ZuybB|`mmI_`ljbR${wW@pp&QHh4wex#W|mJf>ZSk_t$t~DHRel>m%;{g zbNKD|uhWQG*z^t&TLETHG9LJoJfC^&5ywQ&G_gHD4Ci}92~rw2Rw?DE=4)oZ4__YL zNv;ZSa1HEPjJm)ougUwKQ{_u8N~gYX$QHLeJXyc+S)_Eq$V^-r(_Wd{bh?SGqPlZa zKr(`u^#}=`Q(Wc)Ccn+NTssaGdkplLqVc)$E2A%g=B{P!xUmaRwlY0K>vlkg$?&ur z)m*;so)kk*LY8)Uj?~E`EzxIr;E|M+bsW68xokc{*d6$oS+#DxtDcTy@re=C^F}@_=EwX2^7;T9#qO>XLszoER%Cahz zH#hpB_XNl#Ny%I~Y6v=C7Y!3*g7!a)#6@=-(c$v#eN)?29;-=Q7@?tAp5YCAk%gX~ z!cpDpb6q4brBD~ZDRoAuqk9?JztpHl_K}o#(}%;vTjbWmjQjy?LgXl(a)qKEEE+wm z$(SPP>FwmVDY>ma(``JQ!=qC_p+H!=pgQaU#U^H(_VTC ztZbpA7uZC6?LnbY*!XmOF3d65iMVg?FoLtdDteTXGoas+%YEa8k+5yP6^oaeW1W~| zotmS=EBdsFqxFc_{RDhjg&yUfl-v)@?->bYrekFLlQ?_EPX7sy0)fZ>gh>mjO3OXIFS1g0AtlUsRFON3N>E-Akx{01U`wCLHFbh+boOI6AMbV4sJL7{ky2C#EV&$}gn!+2M zg3OK3NC_vyVar`yvoVD>WF8e%K`Qv^8%P^<8_a*v&A;d;1_q{Iz0CNFpZJTC`u8CC zzv$c__&3wfUVetZ0YLa0$e2>oGqM8M*;xQ=Kl(QefE~%tZe=_fprwlF>P1rFbe^PiSTTJBr+%1imMtTUXQ11pJTm_MW9ySM+!ij))ncXF)zxzQ zU4^d6Rh>h~uH;>G-utTs#)aJ}hP|AJi4Xe4wat*9tl!`?*IHkEFE7~&bjxEc!KGE} zfx}d5X6XO^-o@R?>f$?kNm)*e7JJ!4=c4Ufj)a~b#>?Beyftp~mbIYjv-8Dt9Mur- zFZQmd!%56#p%-7CaIS1&6_sy5_eQf+ILlza)jK<_4xNNvMjm;ct?fBZw6+t1E%%LN z7zlaX4ya}*x0JhwN;vXLzwK}hHXWgu&jE{g8n)dFwM!K4GE;9?v8@h^FV#~oe4FTk zP^z-g?ljriRg-8_U_z09+J33*iV|G>QCH8#n+{1xhjwg1xRVpQInBh9e--BYXh^&} zS8I%$FNQ;v@nh z<$Uh`ZaUXm7a3dmX$14>ZvLs28PE&E@7F8h*GETSz7X z>M!9>?(*aUI-rveLzurM?P09LdLlt@G%PHgSJj*#nH(Y?kQ|Bb6d#>0QM*AJogcm$ zot36dC=j0AH_GoEG%9}5J1Tq?QW1a@pOu1(m=%Z=o0Wizq)VNr9>C+OFhMp5fIfIDrM7RNh#IOftV<;S-l>z^kBf6S4;0GAP)SuM2u4SaUMTy5LU{1OeIz z1)Y3Z;YXHrSiHMnB3kh*wSp5f8DfeIAb<;a1Uv(ZtrZ zCS^*q>4Y|hS_wgBPV;LFJ$67|#LccrIKDu1d=T>RJ;oLSh%>!HXa}OJLQHVTD~JTq z1j!=7n@osr2F`RWwp6-j3z7Y(1;3HPScce0ArE7IWtN;AL_DNgNg{2k4f_7#YXaf! zsgQ@yF)fl0akg#}bQwaHa<*+abUE_JIiU&2u_ke$+B#HQ&d%$dHnNH<>gc;%t z1TPXj_vGLZwT&0)YvdWXGF2&-FvNQ*%qd33<}1b>7Fpzt5f{fiA{ zWn%?a_us-po*ImcVox;>qkTCM?UybqIzZnH*oTd87|`#OsAw5N)m~vlnP5p`R3c+r z#6&^SlM{#H`w+$Yv4BR$=7IKC<9t%X!qJY2&m|wFl0F6Yws=gwv}9#-jrY;rmIUAS z%u(}^$5F&EyM25TyS>q2J)@cStb*)LRRqM%Uc4xFpF3pgiyhV4qS?6RHv>T>w6rE~ z>$uvD!vPAlG;eEM`F-(@iMNY{FUD?Q(#yOT8=!q5M&8NRhsLum#VteKBTd$nWYHAj z9g`l%Z;UlYuT8iuYdH%g%#iLwS-rSmVPRq>eSap}4x=NLFgP!KPl<&-@`#`g z@u8K7Fsm-5X(HUOu^c`lU^HMfpeSYtZiT27m^RRvawHYVa?pt+#ComY;CY>MJV>r zjZea@`hb?xvjG#Ltch)JzKKiviH^(d%oKk|0W_G=0kj~7u0$CccP%S%nUa`eE=>LyyNgoIUllSWz$TnUhB_fsDz_$LJgC8d)5*K2z~C_mBHU?Bs3nnh9 zYN+gwfbK3fyOpZ!6%G|IlrovTP7i1bSm(H8~IdR@Cc1A17=8N>lv3Kr7{(eaMYEe|20hVkJWfplpa z%W2*(LHK2s1^CD_K{Jm9+hjZu#y>>i=9+qIc!!`tjqxC>?dHk!JA)}zI)O5K#^CC( zdID4!+%;y2a_2SLWW4#7phh3PP18QTVc6g}7FOhWt@iy0OpF%(tul@cbc~X zA9W^T<~SyOAPvYeR0Z-VG#i9m=i69zJviPVJ8wJ$?N$#pTGETda9YtTD;CkD4+Z-0 z-)4D`d39Hzq~DsYzV+%Rx|@mFrd0?Mm$*r#8bYqWC~sd6M^q+~ERc5UCjNXUx{2o{FfGr%zF zwJ;c`I(E6Q@t1YGbMieRo^fw-wLcCI%3|Gd#NTCAmZ0B7ODi1*>+2Bh=*$Xzhkr!c z78vDT*T)^j>vF%6xHBGmgj&wX!b!2XVp2{yaQ+gUe_v?ONUFd19^)dA{>Uus7W|aK z^ucBD4nH@ts|nth3+s#qd=}?S3@V}1T`^QKq#*FtN2 zgOr-e{h+HQ1o^MQF{zrl+L?-20`0q*?4!ZO7}NG-lXo0g-b*F7Ge~b8#Of<(N;RT4 ztEFGLZ{O1{*|OW-h8T7`vGKC`+zdh9WmxE0w4Tk&W0obJg|QBEiKezrM{w%&hgZ(h z8yB!zeOS$99iG)S=JYM;h_56Z7F_fn{*YX_P|6>gx41)T^C*|HH-89y_Aa2+l^A%^u6K4f?tozj?7$ ze_n2^hg&$YwOgc;F5IjNOeJx`o3WHq-e~1RRKzG8Y&|hp_>>*b%(sM=iaDNvjW8W* z*oA=rx4UNCVD<9N2BnK&<|&zVED;Vz|KTPj7-Megf)-|rl?ZziqS1PcP_m<31XB*q zv~IFAi(3cF5R6jI7KnI`qD3~-*GqOoENZ6kiXPS8mLg&wOgyoABb|EpOr{P`F^Bk@ zq2cjh!{ju>{FqsFFVo4xlXqOSa%_`4{oo&*M#vPKp8_-(r$p5gbKB)lD=OIG7<qt*_6bVpJiHjqaA$9`{_VlpQVeVY z4W#hq6m>L{MtN(&ljlJ$IFThfm}O_d+^oyu~;jtiu$ z@Q!vmu2O1(|7hV{*HoKhn|fmx=4iYS;~|CbUNe5$;o6{5HV1mzOio5g7DLgLrVs~e zYork8IHKl!Nnb--Xva4%O9t}S~PZ0NMInQzA)vofyR)9ms z;mhquF~h_@Wpi;JRQ%Sp+@r8a)@u!q6c0|1KzB1qNsQG)Qv2cc)=E01Ulc7H_fg*Km)UK=g_1k@dE6@sv zc@KI4V&c8xodgp1_~zQN4a%Dq1hy2)^VKm`rl5q74;i!pby+N7z}T96KT_8lVZu<+ z9{!w{NDiCx5U-`A<#g0-(at}QuM`?4vAHmEK;FYHYqb@4dx0p)Q-ur-uT;8!m7a_p zL7)bkppsYgWE>Fn@3UcL-Pr2jJ4Nsov=}<}mF4M7)_~4x^Yw1)jb-gK!T`4{=g#E` zYrHbB1G`<*i<35Jg1<&M7M~$n3u%b0DkJU|9s?)8dxsRnRTb`}K%=GCv5n$L5PZ~5 zUXWZf?!qA$NcKUcQWa6`bzrE67^+O}J;iQ^(s!AoQOl}mp6t*%I;b74y$DaR$)J~O z7;Ert{H|?mu*FJ6nHi(>HDN=YUJ$5EK5mE*@Rlqbh434g<(SqV+(LNt>P0xE`3|lo zUqhX#xI(aQ6Q76RKb`dEy{}3r)%9xoOd)_BhbWQqIktOT*EQyae2PHvRIMW1+PhaA8g7tC{mDLSMATgxyD`8mnsgpn)sx6k1+GQnG4_XWJAKYv zw;lWR5gjy@>yNU?h4HxA1&HCb+k&ZJhw#_J?=zM_?p|qoRrw^{uDA$`c)PH+sZ&2;FiTj?#|_~?lzz$M z94XDH`5QpR8?)K}Qs?Y*6VisdXFvuzcBj!sh^x*_R~fI97R&eE5G@v5Ta&CU1pn5G z#baG)&9BMdppM;NdTAR#2aa}%$&;7~sc`{nLUclOC@JF}`WttJn2Qc;MH&ycIgBB~ zkMPmhzOP%~Ls(f!wYpy|iANcN$ zWl6vjE=8v1^3KDt9p~k;RqR#;a^&d1IpuBX&fZoSBPu6PsOh)Y+9ev~*pZ6eLM;B$ zqDlS?fkVQFO{v0pKbz{CtY@pQ4Z}CGFGG|y8J8b!N!|=GB3$<1YDx;pVaVcLNkICS6`nv z`%`M?$(@i_#`*WVZiLy%yw|KR;h6Gn5L?Jf|6-siqGqHXua;hc^Tl1SUawlM*j53U z#@Au?jjLC!wXF$WU)q|>Kc2Bf{Gf2Yi*~uW7b$%A!2*rIXoXoX$wlp6M5~Pk2Hh>8 zI=D-(@TBC^su%KW3l`o!J3mG0_Exr(-gkF5clVNypT|R|j(ID%HV`ir7XcJ(kJ@}P z9$GtjC91sb_*b<`UuV9^JR&_-X;|NfNld=k_igx)L6~6o@hbDBOYzZGWX@Rmjb6(~ zfqv)<25OOcuaZT7m&i5vimcVwhEN_vOph;UROX_Xwe@3S-+FT5bzBmzX&Zv?FxL2D z&0h75L{u()W{c>!>(pjRD$uWXurkiES@o2zo5d!G`#LVl5_F|Eb&r%mETc9Y^0DqD zHE(HjL8^jaKh0bgeZhzI9VK2^DjFZl`!rNVH0}uZC&L+-q|Z~eQ{mr?Wna<`WfI)N zdBsT_TelS#}68sYjukYYx)vEstjlm|W$%(-X#A(jFXgPz7`N|nv)7Df!gu$X^H`1UD zeT#g|i8PmVXn0Q{m^o{Qnzco)#+vCG%UdgBth*>LRZRMZxI@(r_nPGLFun-xApWi7751-1aXAZw>%->ijVa!!(;D^xzcs$vOPMNg9>HB`WM^R9-!UyDXDJp| zhOio3^j1N&-T6S!z#x`Fm&JFgf#SQ(3W2!rLVjw9r9rYLRKPJN4=?`ZW8Zj2#ko$c z0bD|)`wMMVKKq?=WwSE26i#lxTfsPuZ+Tuu(*=na)J6*t4Rhg;Wqi}w5(&cuW!~D= zX7ZW<1@&da1JgoO4Pg&6pM>v<6LQjm(nmSWHI+PTiRvpJV8jQh7EV&~M+M4|=Pg*t z+1M*ELR))N6M{bd7PXvjm#5T)(^zCl-?I&~N`Lx_BT}ohtzwTcqxYsVE4<9f+ITL% z?!%_=>BN@#Sx&9L1EMee=kqQ2Yr@R_2XMc}K~( zw<2>Ewfp!uB6u8EO2XfZ=#EKB6y+Aj9a`{l#%Cd41%>+cq$=t;1#3o-e(B6BFxmK? zT|n(Tb9-@y$4sNp>Rnt)l3RZGK$o}XoxAHdO2**)^J?ZlHd@sp?LU(tN_*~lScOK*rW<8)=Ceu zkxAZ2k1N%*A_akE1XAytM1l$BNJ0B*4`DU0gG$~7s$ddgw8%BeXo-5sGHa$ccvb89 z6K7`^S%MpopH8!yZ`=4RM~h7bSu(v<2wHAjuzSzi{lEkt)?(#K z*4}8M?G$$JUng}EH0hu{ah^=fyjNyg#u{nzt!HG-O?pzY_I1PKfW!GAqMA~6<>J$a z2A(YV;Yr^*vwASgkL&5Lr{_C~&lxg((sCg$s1@viR_wxI$Kl0W~m_8Eu&aKOp0n- zQL5#IxrP z9a`Z6?qNh#-)5hM=;RHsc{udjg1Wq7ZOMJw{phMofib)ntgd$aP;fds@xjN&b7*zr zLRxX}D0QrY%T@GZkepfQ={4SD2h2aA@EEp!2O?z zR?nsXKYaep6aFtG|3652ewOF|zi}78r!oCyXaAbJ5c;Qi{e!arlGyCbKoa|B3KtXb zXL#rtfWPTp z=4Sns!1bfx*9iMXS^V*W#V^W&o`L=UgtJ(1b8}G=uCZ1=Fy$^m5H++{CguZ_; z@SdvBEU&Zvt~fWKG0cqQMvbKL#m34YYK^TFg=W0T%1gqg*0xLra{ z_41v)W@siMHnrEG-UqdMtuU^KR7jH4b`JSse8E&n@@;Vo% zi_48j=nC(WniWYKixSr>79EoOF78PHc7I}6bVQk~Bt5BktkO%PLs|(Gs=cvsam1{F~?JUoYwDNNVrr^P3V*AZ?L#g*e7R`O|_)()_cog=k=J^ z*kExbrO7wX<)3paNxayP{T!F*Mz>h^V#|O{zHQTh!L>5+%;3$5OWvY}OghACG!bQusjHJ>Csh&P-HD+J@#Q3zpLbYT(ql4Y76udVPD)JT;_&4JBl!eVvF1m zDcxImM~uh`ZUAPXBNrzvda*0E53!cG73OYkv~=sKD{(O-b-fRzJiUs~nJa;zk1y9P zc2oHgX_#-cVlEu98_!PU-dpm3>C`PkR~U-mO~0TgYXCALF9Bzg2rHzhMl4-U$pV=s z(b@a}jMC6qw=Mj0?qphyzCg5qrou6eOQZ_I;E zKa-}f*)mztx8O%e^l>U^Ep?Q3QeV0+4IHzP#-4{dblZ8d`Nqkv!H#!-*c^iRcF@3# z*TP9oWLnWtk4BEIPsR$1ln;9{-BatSo%KlAECjjYAR> zFsG^fyZAHjpDY?kDVRFG*Y+eBzbVhIinWw#1*b6KvT^k~=R+)DHe+{>#1=8_h|}e!;%pvw^nK?d++Be>5qY#fs_`>HA0ZZ z?gP{2ZypVB_Ox0(!w|s+h57Cw+5-|HuzZdd5@PQe2&F{3!f138ZaOiyrm|_$TrK z38K|Yn+hlNO$Ir5d&j(`J+|DWD`$dsQM&o+;c#E7Fglsbhtv!Y(XMxb%D(V;ISX=l zljh_aYfC-ZbJMEyG0V=06rO=mpnEAd>T+C^rCM7En#8j)kSbz+GOV%Tg!oW8xrzqy z;<2WFkS#8pCfJKVO?18o3Q)m&)ss;=ChF+Q8Hnj0vZ5!|*SjW7B^MMz3{k0-3kp>_ zX=w;3_`?~&Ww5AGjANAMV(Epo>{j1JDQAftbR^U&UrHez*hol`97#G7E<_WV!W}8vO|i; zrpYc&A!$TR-C)8lvCNs~N%>6m$5G6hLxpyhJH|A^CJvjt?QE*3>2~k5f}}c2;Q-g! zAsQHfR0j{@7Df|cKi4r#)vDFxV=OmLQe^&4jY#7(`GBmaVsMYUJ%chlRLe z@>N!Lk`vw8%6N6;6DP$Vt`+w^wOO_*zBdTA!@3zBZr?bYDRhfs9!~iNSomZmO)!^oaD-e)&^*CpRh^F+lyyn$P9J2cXb?2WR7(>ySpPt1 z#5m1XI66A7la7iqQUaSXYU`P&P9~CI_o18ud(~{*X&HBGQ3sulos1Y(wUM=kO3*w% z;G?a-&);bR zR$|iKeH>^xDn$eNE0QkB@0hLBiXFnC()2cnicYCH9C2wW8Vp0rw)Gt z*fAbNjwpTimM()&lJ9XU_T)xC%G;X=9L@&Z;NB&it`LcYXwe1~E6(>QN|zTjkDU;@ zdPJftL6UqpUUnwEKssaFx&kr6eY@lqXa4$&mEiv z(KS$xdr8#MSvCq}fK04mClsg6D|{RmMGJnIPc7K;_68?Q01l!f5`DBs(-hFB=Rf<6 zyUWFwHh6Opr3=g#?6{AUPluC*44P35cAyZ~evO?Aac(e8_$npRXp|)achW=^=F>SU z>Aw>qdJji(a-EHG5=s`(avVzi93;7o(wFYPA%%ak@emfnMTsO(D8uj`<}nFkkqz}7 z{z$h{O*So`H&GhuJBk*nkeKKo0Lk@NnoJmD3gO6UF+Jq>>6h>^VS*^N4nhL{ykcY& za~SJbeWgbFPu@$TxRZ7OD9?CGaNi2O+Y3}fztr$OqIDF!X+sZfeiunL9Z8i$l}fOT zP$VkHKUmT!RVY?9S|%mP@6}5KpRt9@-Pt%9Sk@O>R2Vz5_V9Kv;L%#d+PlXf?!MGZ<6Yd=Puh(2ZP^!l0;M)Qg3D?y32A`C1-3_J5esm1WxpzD)h6&(;QxkRA|E5u2Qe@QOALOnb% zGS%qji^8zCFru-fQx61Rx<7T8cRsj`eP+#Y5@V#g z1o}UH4fEmr?7WqMw!N}j{k+26t`PZUnA|VjQc3-_1#%X!>BsJl034GU9t_&3IKdlY zn}YQx>iX*XpX~Z%4f37@?K*OvFMD_d^SCQp8=;)BU`%&6tqW|*@^VTUsp4=k6NqAk zrE8lJ5GWjYA4EP$^kZHr?`ts6N`Lj6k&k_u8t{ z<9BA)PKY09GGJ;$k2w3wHoXE+Xh*ROl^F8WO$_NV?7Txv?X1P#w)z=T0 z;cLK=%(hQR7IHB&_eu7+CdHT==aNmgBxQ!|I2!14POtAgCce+Qr#iXn7dh|EqFrr_ z*V?S|ZcG2v=J{PS=dH=#6^ihs>D@O;#a0@5EW~0@P^NE4iX+) zgsB|~ajSmF+@o!m3-E2dnqT zxBcfD78QbG$#EN{@<5i8rMAQV_}+StHXbg!fh-Pbp^AtqOU};v$QMaxS2YENLoZ*= ztn~|B*U#aRShS{b9m~ciw^kqb6RjMX51j7DzSZHnVD0;iFv)7ZhkHJ|RL>J(VhabW zV&m=@sF=E}T#Vs6woz?v#p4LGU8XpLbkW}=hScJdnmZc?qi{Jvu$8-|bH-@+Vg*yU zOiSDhe@K|TQ1%E`J7p!kpQDBag=7sV*tGH2J*?&tedOYQCIt(}MeUMR9%p`I z$l_8#a9FvAhpnAboNJ#PV2shy&G?BQqr{U&c(LsJE^w7eFkNDsPjCNdF5K}`tMf2S zZ=ZK*MGj0uusz2zQQznS)*cWEAyCUs{W^wG5xr)z#~P6>f&WtjkdZx)yXR85jFL7a z6w6g%T0~rcy3}&6!0grb;(~EhaKMt+|$MrVRwPSzRs1 z)@^>&CVYJ0q5Y7RS&r7$zSa3^Fni%{tf1NNf^_7LTt8)1pu7CZizUSYkfj| zMe*p+)Smf8uZ!WBs0oEGy&$=GMjZbTD<>VN1lj1eonqpWg@U8KV+A{j@ZJ4jvP?z! zu!$Bk?q@=RpPJ+npCg4+a$1@IY){M`Qn$V6xYLK!;ojs=h@19qxjfuo9)O!K z=9`^F4l)wKkWrT&t_3gp+XXGE)sW{ceg}LHUiS)dB8_Cxx?jk$TLP@ls-%P7Ct;X$gccS@b6Xzo4t=}C{)A0H zlu6~;2JnNZWKLyH#b42GD!yKL;Y?3(6lmluv==yTtm+lAf8Kg-T8XS(!7^>LSteJP zGjVB3;XAUSG=OufS^DK6%UdboitQ$^?7`3vR#uGk84-mR$fJ$(dw4jbmHta_`!ZiH!4<$&Jj(b%4#=|^zAUF2DxM|;w7szIxYcN zMTd?@NzQuU&Qpp)S49h%9ie_K6Go3!go}z8#S9bMYS%xa@(XrX7_z~Hi<5qqq4z%9 zLDl}-p%HF!Li>@d#_NJqhv0|T91m|YOV*0R4(57|vGtthIC$){ujfxIrq(s^?fZ*9 z+K3sSq%6l(I%r(M%LoGRAf&EH+De~>TG0tL@)KD3J@bP)t3u(_Fe86xUnQ%t~WKO>K4 zJ;hM_#PXW7O0!C(Rm3;jwB1k1+Mz}65s8|KsEc$e3TwzZJXWddq4H-76cUn*%zl9R zdt`pSB;D1wsavOW<*7Q|ynTsnaICl2Tz>GokEv-ypY;t=8eD*ssyW2+;@9ejNvRSt0pYnvpGJXZ2NqUi5k+t)sIzGNkgUL7a8UsZ4P*nL&8 zm_gXqk@W2B*{mbSX8E~%vth;_*Gr!fDhtgAcp*oO5tKvWg;vK+Hl}96a=Psk!3uZ= zMf2CF!*SzAGvOAU?AJPe^Q^{+%%6K=_$$lYunYkui9p!=;Xvp&6xC@QNAXv<9;WIA z7{u)A2KfE6xiAx$v~2Lunt`6Ju{W{brixC>c4M74g^!YTwp&rZk?FoY_dj~D3Tiu`I}7c^x@| zQI%<{6DS>L*WlK>Y@+tTa80p|;Y%z0#yv+=xwvMNkLRnm+LP@74Vlgaig`u$%{}JzUpCA;CnJS zM5^GJ!xWe8q}Y3ya`8%)6QXIy*2BI3YLd`Qt{Bkl?vh*EcYb3S9VrK7sr0G^%D zt&)8&O-z8yX3Wa31*@ky>LrK;sTaZK`Wz;L?cpHuDYL~LCmVC=+mh^FCPZlM$_{Ri zvF|G)y><^QSq4IfvqhtEi~--v;?B}j+nw!*v@bB=j=61V^%w?w;E5iYi9NVLMEQD$H(qmc!kf9jNhSmR9rR85#~?alNk$}->$I*vU{InBNf~|DJP#;Cv@)W@a!zpa&l?INBmxi;1a)Y2^Oxz7 zsx{~4v2qk|HEv*+s4C8DHtrRheiYqZX? zxFY+P)bk;sgj2IN(`(U@(TO!UmK$QfBqnx;<-1V#HicyjYm-W=&N%TFsr*`0UNTi= zd|siEN`$gLQtXYr@O@kj7L^xpr#lk_81}fa4F*MJjzHXR~6rP?R`(h0|A!2-21MuW<=R z+fDEhRhmlU7rIT=#ij9A7#L#BER;^XRJ#(#0N@A$?ni5%aNwXzT%pvyf%Ss)%(IUU zPWA~RkTA89LI_IEY0S*U%fYwV%%|eyBU=OU_IKaLj;cOpmRed6oR{50OZ`u=v#n;m zmgb)fL59`hBD?$o1cdADAYX%7?)-9^h|hsuk6rq;y z1WY%%F~YFo;jpsn1{}_yHv}5J)VBV2%P9u>Iz9yt7rm zvSZn`xUa5OYP>vk$KAk}Xwp1C%(=;>KM{6G$V6)5!?Toq8?Cmt{Bb**dk=6R3yF_! zxqs}@*i2j8CBpRLgP+s*qb2L_J1J9X?n-*9>Gi|)OvcZ3$>9rdl1D5)(WCSfR-9xxazvX^U_YZ{`0mp z+NCcl&kM&k1d#wTp)+M7hsuU3Hr}x}^ATypV->EZ*;?;DZ7-`Y!{ab)?b+Lc#pu(W zPGCi&%?L@%d|nzRPqhqjrcSyBnbJ%}1u|KGRylVvvEC=~ck=PQP2A#Gn5i`leE1;4 zw=j8rv)I1C8$rJ8gO{z_Qp?`BbD$-kFnWr^s6q4i}jP3U5}n!eHpPpx3SeKk3K zv+h}6aZ%iWTA5SyP;E66<&y_U&02Pc{6?RaWalvaHsCZd1!MgMCKkk`e=rSg2%|z} z$Cmm7L_QjZ+d8T$DxPKt96x0ZKWD#u1{(M{_+GrJy+~=!Pe+q-GBIem&|p z*d&Vp9H|Ve%FjBO{kIE4H#xSrg(|ed()|H@)hLAMWjuN} zAEXM0t%=kUv8sb)8Vz_H)N!W#+O?{w&*@qDdp8+JB8NIngDUlNzmuo!8oYr;uT*T2 zW>nOJ(2NYNN;$RA#^~K#Uq8u)8zkeh=_Et0PFtIimo2$uHe|}A*}2ZTb+lM@yzPBpBiTYX&?R1> z-;vuK-HGOg**9UGfZakJ0RspQ>sTl-LC8k}JmU9F?yIy+kaUs`IpVAXhnip^5hKcH zse>rfNQtTZNj+nj#jUX_ahK)UT6N1;c&*eR*h!@_uuDD65|=bAir61u11tq*V~Ox{ z#ZlRAV&0F{ECZCgYu9CfbqBmwGZ|I>-Q(i>Ei-FFNJj=(Q_5-%J+BFj_Iu*zJzwXe z?X_M&IT9Pq?T4t@LQdQDOkM4;vfe4%GcQwLmlCC*&fMd{AbzvOP>TH`J&Al@;3`w- zlxJQM^6q?(|IX~y8{Y^=K9~BVN@L{Nk$r$YpB>+!#LctWeyg;qE}xOUBR@v;3?vjAiq20JneMqDjK>qbVc1A|GpqSEyg zq8adQx|OcQ*m&@+af?=xj1$hS-)td(f+0KD8OD%MM%wrO;_lOE0PoJ?K^{r!YGrbH z>@Ke>JSSo5ZoolJ8#0-E)`90Nk!;_yu?;ip#)ve>IlZqD--Z|<91yPOSX>8?9wHOZ zdMO{;h;lehAOG2>j&0@#v0v(s9g}QhPF6%}a(6fNk;z>%1@p-^NV9P&`5)FBcAeXI z4Y`+9NFGHHRouMoEGl%4rFLc1};3?Pv9Z0fwJNLJN}-}Zh4Is*FbgL z$UDppQA;&Cb3FdS7YfnDwwvf>Xp~L^2-H-FmBZH9%$^ifHZHT_`)NjQ^gdL_L7{vx z!mN+uILlio1G#7RP#!BjE*7vL}x_0`4XkJb-)l zffHqjyL@W*2^F$DK0%kShEf`{^4M#zNYJtv9|4n4{g&JInj_?G_>aj+!~0!>D!BV`v8PFu8M zk`;}cSYIHuSW&1l6-fh*zJynle%=5{-auui%o&wPi9Wal<6#MqE0TG4bODZLW>qq7%EkfwP+)$XWkGA#m^2nWRw5-H6Kiw90y7-hjs& z*1?A`pzW zlwbP~XT~q$zz@2>FMqCR?89@I@xA=RW|GTs0zfbS)fCea^ znCAzefrpm|%BF`_<_hov{;%b@yu48N%HQR!Fx2VwZ)?jBi1Dv_Tz=^4 z_*IX~Bk-5a(^B==GLLk7BEhL$SvgqxV=0q-(|N(#i&N8X#kMJO>W&PTL}M4OGPEDGgg!4f~4~6qkymJ zT6GD1g`8*Tp@z(8&l=j;R~`T_l%=!lgW$j5OhVh=>)SNQgR?f6QL|<}tIY<~GfoHS4&Z(5F+~J4$)kran6E z_|)eX>|uI1&xJE!43}yNDmPgx8O-sw}g{#Q%A2an-D&i8|(pK zalUTef2O*hQ~D#T@d*4) zp@GiwUy1I8E0mqhY-Vn1YwT?7`oh7U!@+{X)WOaXia)ovZ=S9!Xj~G|E|gG$IyLi896a=(KLzMfB!BcxW0n+z*0TcuJOB_k5Del5=mG#t z&=)jL!NKhR9r7Qo<2;?sEuellFc1w|pZ@QS8v1-d!7LWk|I)YxxOt(8;KxR7|8ETd zWwS#Q#y>SMHvsyi{8Iw}e)tCesR4mMlFe@#H`FEen+5`cq1L*8#(_alpW$!X&xn6& zP{-U4`{&P3ew{Or2LR0iziIpe;6Kjg=U)Gejwg@Pk72WBcoRq3h)b!{;}R`-j)~Hw_FWJ^ZHe3qT1(zi9$s zzCXqg;Q!IfV5R_*0TO2=-?@tZ%Uo^fy);;vj|M=zpYg|`nV<@8E z`Dcqt|0J9_W?*0Dk=JK=JFnB($T&V}6ja03XnT2WVjm5&!}~reFX+ q*u)rQYQ|?G0R2%I?SF^->#sEzS7`G4nTWUrpoc "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