From e978fa320f53cc0c83279f6ac19d54624a503f9c Mon Sep 17 00:00:00 2001 From: "github-merge-queue[bot]" Date: Tue, 1 Oct 2024 19:34:30 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20web=20from=20@=20plfa/plfa.git?= =?UTF-8?q?hub.io@3963819aa26c511083313ce0cd52b7db2d788aa2=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- plfa.epub | Bin 4834814 -> 4834819 bytes plfa.html | 2 +- rss.xml | 2 +- 3 files changed, 2 insertions(+), 2 deletions(-) diff --git a/plfa.epub b/plfa.epub index 20c89e24422dcc523bc526ca5a55a3edc85f1072..bd35436ae0a4cc08196b274d9b23a7d1f2a78a47 100644 GIT binary patch delta 7504 zcmZvh2|QF^*vDrvV<-E*FWItW-?z|MBRhqt$i74&6GF0t!6j=EStHAgeHU3OlqFl) zLb5MKyx08e{lEV{?|kO#KF^uod7kH-x%b@b%yCR1EIhUlMt(^TPCyHR5J4ck8S07T zvc%xQs;c3eOHiT#6M8CsPKvfUr%;ZB87Vqc4Hv$B-o;#)HvtlzqBhZ&Lemf(K&?1d zI85Kkv&;9>iB%DWDcG*6sC)Qrd+F`#rQox78%l)l(01#VnajqEA0Z#Skp_w_r`){Q zL_MbqEKt!-+68aQ!>B8x^PC%|25V;qss*2QO-)^?_LWf&M4%Ir!@RM%e7dCjAAPt+H(#2RPUTQeM-l<`i!s}X zUZ8}9zu2zCy(E}z<~mEO80+I2ZZ6wbWyB#_kSxA|1#n_KC+%_q62W{AaH=joS6pZ` z%@eyg2dY1Zb)qe)Z%r>Aqrkc1Xt3nGs-N>3B7sWqNWz_o|ed z9oHua)%hNvVvuK3D#-RU1x>7Azjq_}LW#Fkv^w{52@XF|b*^X>*Fu)=iX- zfK`2npZ?u=Nb`?#I=HNvkdrlr2O%pSH^+4!S}Pn1#_VDC{l3L;w$?@dlJdMMTSF>o zI%S&1^(qWKXh|@e5%KN^)8r75mrKT@HOJ>EM55)A_K&mG)iR9ThX>il*ZJLtO(^Jm zFFdNPjQr49yY%2PM!G4LG=pUv*G@4M@aR@X@nj8bX5PICe#@DEz?gg>^tl{+^>{}& zJEfrx?B>hS){EEpekBO*oRidhwn%o1`u4toQdIuQzgH&_ge^lIvkGs4pB~Eyrs3da zS{0ATM50fx*PHTEJF_GZNSrbRas~o{Xk9YX5OehO@VoBeC+g{SqsC^y=Tkl1^h{xE zMU03-(#1^1>MzH^K%vnyM`G)s>ZE!J%fQpgtTW1pLOV;rnzwOl`6`L*!E*_ zTfUsW_;}ckQCmV}_0+@mp-I54bX)poLf_Wf)OMEEGx@4peMPHbKHt)Nx?&q0T?TJk zp?~>YnKDw|oQG|FL!f^aD{L4J;A;Dt)Jif5J9(KB?8OAq4E?3vHf0e<_K#1cMxlR( z8isC9d!w!vEhnqK(%hk3zQjsqgj?)NVwLTUm>t&H6FSxm{7|0L5LFz&zPF`m)}T5| zX_uS-;oAInM>i7X!*(rZ?65aufpF}=C!JY{!`}5`PZcJ{!K1~?*Us3BkLzS&_9y9x zXwxz!6P;q0=HLA7OxaNMsw12O?;dsQ?;x46&p zJVE$~;90699<`raf;SmUzbjY<%bcmFE*S2X7xp+V`yq|2Su&33?RlQGOxIVa?>MUl zBW$haDR_CwPOL=kFgnzo+MIu(!>GmiMW*XEeEVrj;rqCOK0)`ib_$=0y{=usC(-N=^x^ zeMR`Ge2!!8{q@&p&Nd%~Paa(G3-lEbxD~@eTDwfzpw{t+$xWI}+h!`27fx`lSL zz_x~u1RYQRBYOCP5kh3zGn-9FknYB3mne3Br3YWwRf zg{5B19pf_2v$rvslJE91HK)TJtQ)WsK1sxI8I#et*fL2kD)~!# z$+e0q*wIvm`E&EUCYDtfey};8SV(;6KYKPR-N$9oiyb~;H}4kj5LAdA@5oVS4fkM* zrBzh>v2R;t%D7ca{9flV?YB64s?mfT$NPjT)OOEyug>Zx4ec_$ zjqM{i9|~XO2WRshEP`a=Y|ezN17WhJM|2ysz9m^DVNt19KZ%Z8YuB|x_lfQ~-Po&v zYTMY!pTiII?J=8ItJ7No($$Qs3H@69p2XRA$Z4}}?S3)oWs-llf+mqx%DvmZW0L-0 ziJ~Lw>P-wq_K$OfPWvyczLoFxzvS$xV6C#<`S_HbTe&phJ4ubq-u;7{hB1>jy+w=> zSn~v5gfKCZ?yIWq@gYZlozTW{*yFUyW9MD6yHDOde&ZgMDJ9xBXEqtxV6~C=Xt=$w=F!8MN!?BIIJ=#5IbDpPb=V{Le&@jy08tc9K_*6@RS3 zw`ZIwlEvp^moD=m1~=7??b6?RrCp~EAekV1W9RflQ)7$0V+6W!+~hbEn4K*#GD?7c zGju|oQCG~Fyo zwxC-#$V>t-5jno`^8QSa(HY6P9>uo?G8*0_cR~hVGRY&652>`n;JH7d64P1@4@gou zzNS-A_@1YVcxuPIYnsSoeAL|>{Ka>(rNxX#!%M$9?T0II$2}B5+KUms<8;e~mMb$; zPPir;HTx;EKvd@DbM(e+*+`nWBY~UQ^Kb}^rtn_@ zHwHG|p)b+<8d8`UAF$9I`hN(RdFe07EB1Uh!|$Zu$47`-bX2igy8UC}j{(91sZi^P zaY56Smr?lv7Q)O9eoW;4&Nt6~L*w?Dj)fm=%_)C!K()uoUlv4DM$&74Ia*%kxpf7% zX~`R=cX;qqtGM`ajVt1@Pyb?%*xke`8NiKZU773*4(?dh) zoEsS|Q>6M{hZTmQrIj4^VQ4^?cj3S~M*EhI{pONZB4L?l!q^c#afl2)4yWgkw;ukf$1?h~wE%HXVRIy*kipH27ZzT5#?)%~dyt#XE z;ql|o8T3gaWO?iNfrX2<)}eZdIB$eUY^S@$Y;7Vgi)7M_f*NZR`bq1{o{(42#mNwa z2S>Exi&nN-ue^;zobkiXvUfHQMr=%)l|#)h3qFAldSL58L&rgY19+ zo9h=u(T159JyqxKOOGB~lUe1+mhf_3pPwQP*?Czxlb!Z5!&bKXll4hm-~sy2KcV=? zTq~L9{vO2$2qb_50wIGyFenBVG^CcR6TUp3S2vt4g$Wu~nW0LB)YQ)F`oMne23)t9 zEy#a=agF9xrT^Ra<^GQsel)mSu`gU;8 z9U=BO{&4RH_Cgjh&Uv>}$fJymjLs5B)+kc>C?92K4iso^&!1VO$lI1B8bHg^(n#KS zKuK$}0)A9fP5rmDxsyrD1xI6Eq$-tsHcuTKx>J+CX`gO%Hr!8viG0K5Jo7szjiD;5 z`X|}XshHWZDCg(0$|Z9QIU^c#U)WzRr@W~9Zot$e_q@|a@^iT;V9K5@!D0Q%mwU@d zpP^bZf7v`|Mz1mzC*qL){@fyZmD%kn%Z6b^q_p`%Z@)_ZJ1TDMo@9G#{qiA44@(Al zZ6`^)rLQ?rjmNYJ+&b~#z;)?akFgw!KdI|j+FN8p=Q}k&?61;v&poyXZNsc-16>Y$ zQS_h1-aod}LG!c;3srtJ4dm>X&3lhS?2js^c0cbr;4YS12|Zu}wEPXw#C;ijM^vK{ zPGZ+$6x|3N?*+d#-_+`iX896?vXCo;deJl_m+^6w7O{M6Df-Co$RTwhE(y}_5>;0< z#&m@6dp(~e=ceox(als(=lam&{mkv`I;G_$pQAugqbc)4idE|`8rNU2a81)H(^Y&Q zrYNpi!-y1mY^ZvfEZwk@L=${4EPdw_wYLuw$n>Y(s|}XxpOib&i;p7Tf-t& z(w7A)?7~5uE43=HHud9@f^Xi=u}vIlK>*V$o(J;kw4$-DJ?BxC)U5v3A$e8tiMyXQ zot1p_rTBEYO2{wsJy`a7zY$2O7@5F%elBqU7w#^m;wYFB64aCLyJ%UAi}$7m3^#gn#6`Qj>)}=a19i6-HX7iF*BWCb5(O4kFx#tf>nit7_kQ1 zQ9pYRk~BoUWyIuCs2@~g8Y4ruJ!=|UmMK2nG$z0DP!A)=!hznPOG#cTAeU(89cXAx zXABMbdQ5IlyFMeTU~|=v^>+Ks>G{<6L^_z#6s?l_`xdHPdY6X46}-z_){h+wa|@Y( zDS76RcbhRI&WxjwMNL@w;@IG021%V|uilT8Pt5s=N8w|dbSBkO3L+Nh$Z4mRx6H3U zTXXw=phiWO3!)h&npssWpM{WcAFHe9Q!ItVlRTr`VwzWF%^1Gdp>VLHtDT7ii8Pw%Jiqj?$d5sC_vhVOS_1bPEfrSc3G>Y4FBX!mMXh!Prn%~YIoS0HGB!)5sofPWMNNv8 zVn#__zq~MJUwJ;HKU((an_ar6DRc2#PqCtCI>CFMEnGy)tLnJUAEUXHHmHfm9V1*6 z@lWQsPu_INURLjYk~%Bxbhqru9giW`48@Rs9F;>_nTPW?xg`zX55eVG881ICc^(t~ zyZD~&DUh;R!r_ddaf5Rj4rc-l9bR%6-mu^&hEaeYS@p~=hNXfFv;--}o0G08T%Z7f z7l??Sf#EkMRK@LCDNi>hWLP@qXbm8cHh&mEwF;%FYSZU4z)P0XOSSPv+N=WHQwYCpcRL5Jw^00n5-ukHob5g-u4neTo`*@4s2sTcQw`M8e{E>Kz zI0f#F9}f0jDm8o!#k&ATg0Fc$Sf2%vkIlf z!c~!K|ERUqke@2?YThkm8Uk;%>?56J@s^Mnq4z(Tvb_n*O7LxlY(&>n@m6gWQJok* zeiiIO$?GBr#E}&+RzuQY6XuAmG?( z7eAdnzz&O&{CD3S$iSi`PWSnMw^$SlbOu<(qLlEy5DvuxdrE+5Bwz&Wa47uQ3V48x z&@kW;4#kF#f!_-RDsU(|C>PL;LvdJxq5giR0{002dF6+SG5p>y^z(ES^>Dm%Ne>F6 zg`fT;Ky><(fK_|{0)`t7fdmmlAS{2nfyew%I2)i^hY~zpEdbX#u!^fdR2_=ruQM|6M{L5W4?FwE-@jiohUNouYYUv*7t0O7ORc7r=lb{N&Zw zgOegFjxiKx0KV7%o|IpwjZgG3mHG^ne+>vwYXD364A?e+SxyH?z+-t^0?aZ4^50St zfSf;~eh1@N3qlA)llpJb4)6sO;Y%TI1S5w4e2pmH|6RWT<34c{N6D zU5J1{=mQadrHceAz@B(f!C-r44fyQ4$@X`;U%)mf!lz?y0@E!3GEKkzE2lmWaQBa& zd+Kiiji8SYYFG}n^12U!>|FUfvlVdiN5td*$-D?0q(RHynU4UC=HHoIno%t9F$y@a zK>?=+vYLO-dMVfpgQftz%_tsxh3jAg^fo}+^1Fgtt|Od^Mi7YHH0-aj{{jsEi2hw9 z|1Q%NNCZV(r(arU_6utzh-3 z!w8^!7?d5f{+5M;&Cm)U3zXrfi;J+cN*6pQ2w;ED1T8T8N2GdzLEeNH0#Ta&Ta*a! zwEa$~+Xg12S4IM&%1C-3r0sXYIItNy2^9U2y*u?)fN!9WFCfDrH_#cp%_6~_{r{er ztbkbi?}?BdYq=~Z3xOo>LH`nA_mRNceK6sp_TLH9+rb3fKn>Uz|Mg6QK0MW%5GeO1 zqzBG){FZTafX&)$M8H)xB6{J!E*~obR8U~F7zC0r{&&K1Af)4W>Hpp-i2thU7SQ%b z)FI@41!@C^gtf=m9oE$$&?vGVm4yRDwPX zZUYQa41B!mAAOM(+ZQ!?64khRh4Si6+-c1+92Nd;H~Bqcu{T>NF1QD!P;^3K zyk*^wW`UPGW1K6R5w4a%(E2c(| z2fVZ^zzkbm{h9WljGzC0hMlNTsc#99INltCVe{Eab8S6Nq{dc7O@4X9ti0q&%L!}P zBJ&r#wD7S+s@a*&@!NgPUl|pQtIFN2wcjjd^Bn973#v;}VFSWzpDAXuN3jxFof+kF7+Mxl@cSffm9KW8V`@_x3hPnu_{YGxaxEj8>8|^ z7x8`H+jEQyVj6)eMjRy*xZ2&*-Dn?o!O1RG+XHt52ZJN5}&CYeH%LCP}b_LGVgl}XMVKu zm|Wb+>cnr9CFgCw#nx``h8 zb(GO+*0TpEdy7vC`vig=u;IL#+@0m_qLSLIXW?pj$B+`=6goSL{qlYlhanouPld3N zC@4BlCFo3_rj>85)YEuzf0FCM^o^3GO&0)7<3fU_X+<^fIbtc%G;wH}ay@*D?J3$t zU!|{`8*e&Rdx9m-r;M`Fu?I1W{9080qLL)-G8#;3xk* zn$**~;Fn%tQ`;{JXxwRLm=brv?(U1KtK7ns-+Zbm*07g)HmoZ^Ve2dkZ`Nv^>{HG@ z8RGE5<#_L#7&`2L5dxnAAKYf08YI(oxq5Lc{K-8y^B8Ms=Kxo8Uv8EALKND&ylP2^ zG(!H|*)gNJ8}^EBEd^a8nNNEel0^;2)wXo3oNeOk3^JVu-zpj*Z;Yb9kE5%ub>1Hd zaOhjZdkML1dB8~cL+1wQtZ(;dIKJr5%yY-SAMw=OlF+66b90gbi`8|DIWUES;}O?y1pYZ#{o z3^NrdBrXTaH0Nv0#_>J2>xo&3j;mgNM6ryRVDW~bm4x(Eo^+qc!0UI%cMD{o+7IF* z1o$skO*$`)E{`up!0@xF5fn1jI~)4Zu_2NMH!86|_*|+oP+4?oTC&ptv(vd!zUv!{ z`P1^3>;px}j7000?fUzCOp1DXdh)avV)IT8GdbgS#7<{u__)zJRpsc~2`&K4NJiS1 z^Q#szwjyz{^um-31A8pwZ0;JL&S}rTwczVC8Ca$^#+AQ8a_*$2*j-V08SK2it;F1? z!7PT2)iDv>5GxO@_D~Pe8An7GFh07&V~ayY74jaMcj5AMUH3pa4$;*JWqMXI z%FP*6RE4;|jZ~-roO8SS?Qd%2O}4W8<#^YFOFBdLjxB<*=j5y_2D4s_u}}`V@FsaF za=c^T(omdso^E}IS6uQa4HD;s{bJ9_4`s%}wK?R8!geIB2PzCDKjD!)j1w7o^(5j> zZ>=t)1rl$nh2}eGOjZm#&|KKiEi3IGTjb5^#`z5RFon}jEs5n9Q*@VJKLL8KC*;>i z+U!;8$>6daapyP$l=waW)PL-iQ41H)1@6?P-=7ch2~~Ey$=_)nC2yzUO`6 zyB#8IFmX|8v<;Ti<_gRBSfiG)U|Pjk_O$;FfadCL)avUyPtj^T6{vljm{MS;05zZX z4NeRfShy;{$}I1P@Ym)p=6z#T9Q89!6uW-)_|L0s;m!BDD6D-&%!EQ%gojGlWNOae z-O3sCbcw7miRPsrRV5kcVrz)=6SuB!I@z_;>qIgx$=1++hEjQ+nus2kGYHpYKqFwA zOd;_4gA2;sFJ;J7I)Mca!f8hF* z6<(E?w7DXG$}BsV0k%iu$4$AoepNzBiiyN6v1_7FuuNr3sa2KefPP8!Y=|L}Tv%hj zCR$#8=<}xxB}+2x#HV)4hU>}83!d2Zk(7HjnrdpmrET@R`9#qXnIRX|%XD-%DamyY zw3$%`mRh`R#4vcE%Dq!-+nn>CRt4JIjwz7omT*6rw_WN~cf8seYF%)3UWuM1OxkM4 zQ|0aa$QcH{^XXw{(bC$8T$NAOw*$qk$aT|TqnuwT8TzQeXHOpx%~^WP%~RgPW+mIB z%h6K!9qljT2;v8KzP9nXjQ}6?27`#+TarHw?rGLX?$#%;?3LU}Y*9B_H*nH!>_%AI zF&NreX!c+Ch%_E#(cRZ*nce%==!36lBKEP1zn6^aRB;PRvU%Zl31hbf{n6hVyJFs%?BF%5#6!A*Qv=KeA=Hg{9K zLz-D6NE?55N0^+#C_^>t+_rG;*2Qt6k55dmx!wILag{8$M)O39ZHTts9$Rrt-sK4L z98meq?jyGkGTgD_w)LE@pH`g(^cYrP(-QR`Y{n&Zbi)E~8;HpBlAg1~W`~l>T&gy{ zk@8^5=I5JLm!Vg~B_HoDACrw}s7!C?Ct*#uNr>227&((0#yDh|J=&p+Iv8P33OgPp zSc~e%c;s30zse-u>+HfF+?O|m&tybM;l$BJ={%R{5$-iBy2Bl3{puf1y3s67C%pEx zDyn$)@j6O*!a-jkasJI?JM2RR7PeqlF&^3GDOJRjNjqEqB2t znAN@$?_Iit)Q5q2@on;oD3WEFzAfcw)6w4 z3z(TRGm&baoy)#Sb4zxLpTYl9bUE$EUftCxq(d|?&?YN*z8R43&~zh{!Kx%&8An>S ztiw*1583Dl%z7&xe`KH6b;WqMLj}t~vE9_9&#UgH9hn;Dgv_~pmM?K}MDRn>DUL?- z_tUo34W_DA({JrD^;A!>-%u|$gWa6?Z|cX3uAY=J#4%Rk<;DaOJf&(;hJ}Fzfwcjo zJFC4DgVsMYk2Bvxf6gY86WE%5zM5s3W}i~8D}HmRReGQ+Tszog_01@mX~rixPW&** z4My+$H;&cEVrI;X9CW?aCUokW&g`tN-VQw=&f4`I@bQfybGmd(1e+awKl-Pe|F63y z3wKULhck4au21rxl(zCP4KI%lF_GVjLEJbN`{l zd_`*J`TO$9{q0}6vcy#kCc|cx7RIKU(V|6dd0#&pRu5Lx&a}m+s`i?;cDt3(=01%n ze9%lTGZB%hll;+!`*IhSJ*Xr=ulfRitVdu`;knNpR%;7|JdaH*x!2mo=yq>f*ipZD zUfS}7ZqeK8#FPk<%aYp^*BjCo?6&4iQJ6hCnqq%#W$zR52a~K#(dKpWp)mOeyREe; zPBg)6DWHmS=t~pLGH=Cwgs*W_+f&ABhVUK{H&!~_m7qzrS#MD{sXEOm3%CnS_~gsx z6<&8z#%dVf*Ail%2d$4L-*-Hk)SM!3XxD6LXY`MV_Ky(VWa5o2U=)ZAW8{quU}V9* zPkz8q_!YeCg1f*+s5JHXMm(Pm~u%qrBy=0sz6PEC~#@T6^Y@= zfm2pu+SN>FMi=@N!Zlg_eq?j*IW3O~e)=LXMzvBk%7QIEw#Rw&6O`~R*EoX}Zu~4( zotYnd*EzEdwltqpGn`Zr8!)W&o;CrfteV&IAm01#V`qxb;~Ugmp)V`-9vCe4e*AHJ z$JscORD_W}khWbghfFV>qUEPQ?KHOLSa0@^>#m=a-XBZXI+xSM6@}9Nc!SotqPXnC zx3#skV5>ZDLG|J=m7(DYFNbt=%apa(79wjK8+z>;Lh^V)$Ah^Tah`0@xKA_KP@Hw{E{gTp8^*4kN=nyRBKt)3c#^MTC?);v&k4cG zH`UecPX59-iUY2k8_*G68`b`423`<(+?z-vHX%>D&74Q^j&;bZaKPoM(FL=FlHNtc z#w{#W)f-t~L8DeS(Y8|xmh?)TCm+ipcDz5KRRUY|uhWUUz~|Vc${sAYTQO8(aWqqS zez9dLEKA?ihbsXaQ7V^DSZaKl$U3QeP}q#`^3Lg*Er~f3@$Ky9+Ly(b{Jv-TN0YT^ zg17Bu9-6vgr>{AhnM4j`Yh@pMVCimbYZzC8tv7DTaOXI)b-XIK)mw73^M@^C#@W(3lI8sNnP~HDWPdqG?!A}rB=JvQFakhbvlv3=abjDy%Hgsdc?@N4ra=52NfPXC?N&!!yd$#b=h%zB;KoO@x`vK0_-b zk?6KcI*`&CY4D&KMuJkVhre z!q->VoWv4zXK|m(DsK6`xPqyL7y4GqX;+UPhu|E{Xm_^0d2?aL6Mi8_#_9&TLUx76 z7RzW^*y}ERJ=~x|WM9Yg$HP>avdWs{{g0WY&o8;X8uf{-WoN^>zol~wEf!*a*NC1m z&b~v=vyD-Ub$Ur zPA^isQQ9MygSBb^OR^<=i|1zOv(0vA>l60B%kAMN0*b>32KxXRPFyoE z*eqmd^HC8K3^M`bZ^J>T15Rj>5=RjewjMMjtKc&*?3!2YkD-HCGp--A)tMQuGgYzIs^jpMB54Dh*B*MI zMR6&{lNk{Wn&&oE9f-Z_^y-F(%6C;WW70X-a`ADiUZ9)Grv7GA<81rEKe}V=Rv)&m z5dr{A{-ApRF+Hx-j>sV7unHXc7ov}pG>2u3Oxj6Pr~yE{Dlxc54Wq}={v<-H5k!*m z#JwTr8W?FPK|>u6b0;FC zVXNp+(eHpXugHF<$x49PcMwG6<|Iy+2$t^)l3$(#>lPPW-;iMS`M`%w30BT9oLQY< zH83K64=awF8R1VDU|c#2;vOI2EbnPV>+iNDWrXE#>w+p`vXpREcpZ@lCs=Ji5Dsz# zOG1Lw{deRXchaIlLZ^^{)wZ$;01)=@_t?2}keyE;sO!qfY9t7j&m7s00)plK2r2cu z%BPD+_un~LKO;BYU>~dH!ceB<5EKxU5L6J<5Ht`d2wDg_2zm$x2u27d2xbTt9LkjS zCYBHd`;IjX`;HBQ9Rdx(0dWk16M_qZ8-fRd7lIFhA3^{^5JCuteJAWLL5Q@06baiv zib5QR5Q7khkbsbckb*b?Aq^n|Aq#O5LJr~-ZUZSF7)T5C%Gj(&GOkDx1xTJn0sJ5l zxd;n5-Ht(pJqwkGP=HW`P=YuOp$wq{p$ee}p$>5dLIdI~#5sub5SqAW&`%u6!%+oo zaTw|UZoz|@IE)l0wC88+&t|*p18wbPL5M*dy>f$Qz;8H=(&5G+C{c}JC(a~^Z6IM0 z)xAJO%m6#w*(W>P**CsEW@F-s001GViTdbj=$IQ61U|0DaBv=q{@zGD(&Ywmfj!k2 zPC_Y!FKBQ8@Zkgi$|D6K(s2-3gJI`7jMUQmF_s4g00Bq0`A05ld!9nxC^+C%I z=muR$WDG{uVE8zpRmfNr3A;2+1OPWk0D$oy0TjT2BN0sMQtbpJ^8S}d3#6;X@EtB% zpnNS9*#Oi(@&h5Cm{UAfRh$_tsl`wd#=YrKbOM}&M1+wz$=)`{a1j7rc@zJYJ{~+) z_ebPGpL;y;900T`{4JUSt&c<`yhgXApc>yp{IeqwU@jygr0=PNYFhmei<)Hy59|4Dbad|rXZG?)Sa*#0pjTcC42Mwk#O>F}Z;uoAk6;7=X;Kf#|zK4$~u z<3YuSKS3+H+i#~rL2XI@F7Ft4=SZa3vok283{6Jd-yK~6Umb~biiwQf?gGH3IsC7V zUIj@S|CA%z2&Ml4o$6BVI=&Upj7r?!ja!_=-Yr3fBb}I$gKm>&3|H=&t%~j)Bu1^i|DV! z(V*p#NG|Mt_~GQv{A+Rx!E8uGNZbWQhS4x1Kq+Pf6S&v>XL>1LLCujY2(Xw1YF2&q zr}+}pOhgMhz4}v!LlUk@0t%1+SBf#P_(=5r)Z*2`QUK@{LjF~(Jh*lwN-@mzcYtnO z1oT(IKR=1gpiIl3Voh71^ktyWk)ICvFb)Y)P(^~22^4DjQ{{(4Sv0r@$q3W*-)G0) zldlG3U;_NZB>*4=x@Z4cKmm9k5)nr0c`Fpz4(vGcS0Eo|`3MOHJwh`5W7#-d zFD2U`bu6ge_9w+zO=_h!HvsVJC;2M{Dfk!?aUU+@{zmenC$KbtOdJgWEn@$9Programming Language Foundations in Agda – Programming Language Foundations in Agda

Programming Language Foundations in Agda

Philip Wadler

Wen Kokke

Jeremy G. Siek

2024-09

Creative Commons Attribution 4.0 International License

Front matter

Dedication

de Philip, para Wanda

amor da minha vida

knock knock knock

…

Preface

The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.

Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.

The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.

Personal remarks

Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.

However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While the notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.

I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.

Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda covers related ground, but focusses more on programming with dependent types than on the theory of programming languages.

The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.

I am fortunate that my student, Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.

Most of the text was written during a sabbatical in the first half of 2018.

— Philip Wadler, Rio de Janeiro, January–June 2018

A word on the exercises

Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.

Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.

Exercises labelled “(practice)” are included for those who want extra practice.

You may answer the exercises by downloading the book from github and editing where it says “– Your code goes here”. Alternatively, you may be given a file to edit containing exercises for a given coursework.

In either case, you may need to import additional library functions required for the solution. You may also need to set up PLFA as an Agda library, as described in Getting Started.

Please do not post answers to the exercises in a public place.

There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.

Getting Started

CIpre-commit.ci statusRelease Versionagdastandard-library

Getting Started for Readers

You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:

PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.

There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.

On macOS: Install the XCode Command Line Tools

On macOS, you’ll need to install The XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:

xcode-select --install

Install Git

You can check whether you have Git by running the following command:

git --version

If you do not have Git, see the Git downloads page.

Install GHC and Cabal

Agda is written in Haskell, so to install it we’ll need the Glorious Haskell Compiler and its package manager Cabal. PLFA should work with any version of GHC >=8.10, but is tested with versions 8.10 – 9.8. We recommend installing GHC and Cabal using ghcup. For instance, once ghcup is installed, by typing

ghcup install ghc 9.4.8
+Programming Language Foundations in Agda – Programming Language Foundations in Agda
Programming Language Foundations in Agda
Philip Wadler
Wen Kokke
Jeremy G. Siek
2024-10
Creative Commons Attribution 4.0 International License
Front matter
Dedication
de Philip, para Wanda
amor da minha vida
knock knock knock
…
Preface
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that a certain kind of formal structure may be read in two ways: either as a proposition in logic or as a type in computing. Further, a related structure may be read as either the proof of the proposition or as a programme of the corresponding type. Further still, simplification of proofs corresponds to evaluation of programs.
Accordingly, the title of this book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.
The book is aimed at students in the last year of an undergraduate honours programme or the first year of a master or doctorate degree. It aims to teach the fundamentals of operational semantics of programming languages, with simply-typed lambda calculus as the central example. The textbook is written as a literate script in Agda. The hope is that using a proof assistant will make the development more concrete and accessible to students, and give them rapid feedback to find and correct misapprehensions.
The book is broken into two parts. The first part, Logical Foundations, develops the needed formalisms. The second part, Programming Language Foundations, introduces basic methods of operational semantics.
Personal remarks
Since 2013, I have taught a course on Types and Semantics for Programming Languages to fourth-year undergraduates and masters students at the University of Edinburgh. An earlier version of that course was based on Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.
However, after five years of experience, I have come to the conclusion that Coq is not the best vehicle. Too much of the course needs to focus on learning tactics for proof derivation, to the cost of learning the fundamentals of programming language theory. Every concept has to be learned twice: e.g., both the product data type, and the corresponding tactics for introduction and elimination of conjunctions. The rules Coq applies to generate induction hypotheses can sometimes seem mysterious. While the notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.
I found myself keen to recast the course in Agda. In Agda, there is no longer any need to learn about tactics: there is just dependently-typed programming, plain and simple. Introduction is always by a constructor, elimination is always by pattern matching. Induction is no longer a mysterious separate concept, but corresponds to the familiar notion of recursion. Mixfix syntax is flexible while using just one name for each concept, e.g., substitution is _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.
Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda covers related ground, but focusses more on programming with dependent types than on the theory of programming languages.
The original goal was to simply adapt Software Foundations, maintaining the same text but transposing the code from Coq to Agda. But it quickly became clear to me that after five years in the classroom I had my own ideas about how to present the material. They say you should never write a book unless you cannot not write the book, and I soon found that this was a book I could not not write.
I am fortunate that my student, Wen Kokke, was keen to help. She guided me as a newbie to Agda and provided an infrastructure that is easy to use and produces pages that are a pleasure to view.
Most of the text was written during a sabbatical in the first half of 2018.
— Philip Wadler, Rio de Janeiro, January–June 2018
A word on the exercises
Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.
Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.
Exercises labelled “(practice)” are included for those who want extra practice.
You may answer the exercises by downloading the book from github and editing where it says “– Your code goes here”. Alternatively, you may be given a file to edit containing exercises for a given coursework.
In either case, you may need to import additional library functions required for the solution. You may also need to set up PLFA as an Agda library, as described in Getting Started.
Please do not post answers to the exercises in a public place.
There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.
Getting Started
CIpre-commit.ci statusRelease Versionagdastandard-library
Getting Started for Readers
You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:
PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.
There are several versions of Agda and its standard library online. If you are using a package manager, like Homebrew or Debian apt, the version of Agda available there may be out of date. Furthermore, Agda is under active development, so if you install the development version from the GitHub, you might find the developers have introduced changes which break the code here. Therefore, it’s important to have the specific versions of Agda and the standard library shown above.
On macOS: Install the XCode Command Line Tools
On macOS, you’ll need to install The XCode Command Line Tools. For most versions of macOS, you can install these by running the following command:
xcode-select --install
Install Git
You can check whether you have Git by running the following command:
git --version
If you do not have Git, see the Git downloads page.
Install GHC and Cabal
Agda is written in Haskell, so to install it we’ll need the Glorious Haskell Compiler and its package manager Cabal. PLFA should work with any version of GHC >=8.10, but is tested with versions 8.10 – 9.8. We recommend installing GHC and Cabal using ghcup. For instance, once ghcup is installed, by typing
ghcup install ghc 9.4.8
 ghcup install cabal recommended
 
 ghcup set ghc 9.4.8
diff --git a/rss.xml b/rss.xml
index 841ea435c..4326ffe46 100644
--- a/rss.xml
+++ b/rss.xml
@@ -8,7 +8,7 @@
     
     en
     
-    Mon, 23 Sep 2024 22:59:58 +0000
+    Tue, 01 Oct 2024 19:18:28 +0000
         
       Migration to Agda 2.7.0
       https://plfa.github.io//2024/09/05/migration-to-agda-2-7-0/index.html