From 8425c7c8539710f6581879a77c26ab461eda80f9 Mon Sep 17 00:00:00 2001 From: Chris Henson Date: Sat, 30 May 2026 14:11:33 -0400 Subject: [PATCH] add Chris Henson --- data/people.yaml | 9 +++++++++ img/henson.jpg | Bin 0 -> 4466 bytes 2 files changed, 9 insertions(+) create mode 100644 img/henson.jpg diff --git a/data/people.yaml b/data/people.yaml index a50d0cc7d..e4a9b1d8f 100644 --- a/data/people.yaml +++ b/data/people.yaml @@ -131,6 +131,15 @@ been formalizing mathematics since 2016, first in Isabelle and now in Lean. img: sebastien.jpg +- + name: Chris Henson + github: chenson2018 + descr: | + Chris is a PhD student in Computer Science, specifically Programming Languages, at Drexel + University (USA). In 2020 he started formalizing computer science in Lean, Rocq, and Agda + while still working in quantitative finance. He has been contributing to Mathlib and CSLib + since 2025. + img: henson.jpg - name: Julia Markus Himmel github: TwoFX diff --git a/img/henson.jpg b/img/henson.jpg new file mode 100644 index 0000000000000000000000000000000000000000..eeedfbf78f9d01ccd4ad8388667850abafd8fd64 GIT binary patch literal 4466 zcmb7`XE+<~*T)lkmLT@tV((qEX=2t0QdN7E*tAM@p;oLCBSr01B{o&6hzdpR)goxA z87=iwX1G&vh>6E>{4|CQvvO00aX5tII`z5rCSKl8Tao znu?N&hMJm&4n$8!OG^i4VrBqwg1Nak!JHgC{1QSud}4eYoWgR#Vv+%BtL<8^uc#s1@05TAe90a`V2k-y@WaPmA zvwLNll8T&ynhfx7P=gsj1|*}PAg3lLC#U>3As`t!1qeXNB1ENVV8!YhOwA^&^faRw zY}hLjf>TzpW_K(3a&UE%8~7jWe{1lc6G%=*K?$I`ib-8P|F3`)K+69u6Oar(n8npO;Yuy|xa^?2H=V~z&&Y?pcdcrop&29Q zLA|>!(Py|fHOyAdB0>1Yz`2;{8E!XU7bArIaBuSQxu1`oo~1=Mql!PG6l zv!Ho;Q&e%*zE4QnEH>#LiV*Mq7n>7$-rj&4EkE|vF4e!w=Gw%@4!%H6y zVNg}}n~Jto9H%WzX{&TezGUw)Wv~_C`>xL8zph1tLryG2JU`z^6C1L8^)$Bbrl6?> z`f#_2N1*bpV5v+%ClmXr3WT~YHBM@QWQ;Wx?#5)aihbL;!^nn%~2f=dn<@z)F ztnA(hrkcXn6L51SZj%SF_cH2$Z zcpu>7O9k%2q6~LcjT8>e-qFp)c8&Gr0Bu0P&6T*JEawqZUL$A&k z{wDBQVHFb`$DiCY{dHtkL+es2ADrS*gT{NRG*jzzPgeVRZUw^u7tK_|!O$NGRhs7d z6i5Mj?^kz-56Ip`=li0ckh{Eg+n02=eX-Uj^;zlqwkt|AiNTRLZK)a!(yA`0EuLUc0!Y%K34gBHdUb;mob zte4CY;(iVYuUBXjHL?%%p@$#KA)ZS??Wrs_gLeN!P1qShzRYPE2~KPWkFzeaAXzs2 zaASjkTV`wd{MjdE+r@1;1+Nk&S+hdd(o#%8Ij)2*o-{Qec6b9lp z;=Y)lh>{lrMK|6S{dtP|AWEjiIC#e?Rg&ZtV1ky<;21QVz<74(?|ec+Z{&WaGd7)4?Y>26-5GtQMd~)qa%yIw2j%f5CzXf_wY`A(;ib4ek5yn2zKGLvn zvX&BiJr#xWbIBB`iMuPzWzfw&-tW04V!?ZyXqgx1bNI8GA*4~Y8Dp*9R>-lguEQvX z;<|v!$;}#d&Q3goNae8$R+`c_Z*4llwZrksr-#$_tHN~&uMCiIwk2r1r(&zJb*dwkyrQE(9dpqYR!pU<0rQ}Sg;H@G^rls(p?O;prV9z9`Bl=p-(E>v4`-e$+7Otj7PP$;n{vk(t{f~AC8P3##Na7`6 z_SC95#Xr{$1)qc(_2)-D`l~o8UZB&%Mz+G!a*a+pr=QX`0>OwjFbxgvA04C z)y>>b4WB&0KsK046Ql4fb&iglX9}Mdon0`axk8ubS6(^B6uWn?J~B}g=@wj+HO%F%O_G-QY_2Ni#6qFwk(+Kg3o>uy&TV7z;!TSwx$zhOF6KdA`(O@O4NSyk{}IIs-<4XrmEI|1&DChj8b3mU?Ls^36oqn z-rr8pRXq3#*gn+Kf(skzx?@sQ7tD2GbMyeUkB+hfey?}U!kf>K8$+j>erVF59*ZGHqE5)>I&ThORzVp{z`H`F%__u z>CwwylRSG|{8)}SHm&@3V!}AlD9S&E@j9V`f3!F^5lbacKb)ZS7$b2=pI%H z=USH+GxTgd!(a8%`53ns$3l{P_WCcFS+igxPkn5(;#Qj(J>6VipJv@7mcG6YbJH)L zN7?#apsJw$j1W^YOF0KK3|0WWm%L@Zv4<~A&nsIGFr@GT`M(3>cUHHZo9&{ zwUISqqFC~f8yx~`44DBcoRMI)rFUnvV+96myAYaJrO^?$?D~J<=CIfZ+()+S@JQsE zTJ^jtFRK?3vNU0N4bvIONa5>sgBq>|xb|Lw04rNx_NvFQ5q#0SO0X@uDkBkgl<-R6 z$SPNhxFg94Psr{vRkHh(K#`(m;HJOluZRrvoK>F?A6mzrPNn`%s*r87{p;3Uw`LfNP0eSKXryLY7N)ZK|i|B1HG@S zOv{U>-)az|s&(uxxJg2XoBi5wtX8|$*|WkGcq~&%dNL&P1$yy|Gegw0DBsxgY+?D8 zgxc%jyINfdO5VT(OOXB!;jtL}Y)xYZv2A!7%oc82f2tYVrAY5L$)6cX9u+=tT;IeM z10Ws5YBmd3w7#))7GYJsp)`;FoaP$*BfgTY)c|k4`9f^C5fZ&V5tVh+v@PYkc&eY; zYdP@k45vEKDLhq;t5vD2s*Y!xtRl21$KR^br(lj;9;O`Vj;qL?{~F_sy}|So%-mp0 z2}kJ37lI1;hp(%dw7>E|?%2$7U}4@?WrdgllakZyG_J5;wq$Nulx-+n-{fO4|23WR z%HbvR^10out+;Y;lQ8h{eVx2I|H-b$rWM4t?A~kQTmvvtI?XLKlhN> zG9NrpS3)PJ_@=^$+1)QxV^0vttqBHq?E1s6RWt5=2;+YMHn11Jwul+tJx*pAETPhwA<3jxQ}MPV3(TCo9}-0a6?=baNQ?o6~x4`8QwsS5e5;-jNFsDfNirXVzjo4eqezIy70 z6~>?IjVd3W91gZLBjXXWj0SVxMkrgC+!}t7y&ciT$GN0bbpj~&U9WbsVIGBNQOdme zU}ERH`v}x~RARDr zhS6t9z}NW2NN0f9o7UD^nQD`>*2h#9?P&jv%t~cK0A%* zPr!(f``vFL^@