cslib

Author: twwar

math.html

@@ -37,6 +37,8 @@ <h1>Mathematics</h1>
 
   <li>A talk, given to a general audience, giving a brief history of the connection between proof theory and computation: <a href="https://thomaskwaring.github.io/proofs-computation-notes.pdf">notes</a>, and <a href="https://thomaskwaring.github.io/proofs-computation-slides.pdf">slides</a>. Given at il Collegio Universitario "Lamaro Pozziani" (February 2025).</li>
 
+  <li>I have been learning the <a href="https://lean-lang.org/">Lean proof assistant</a>. Recently, I contributed a <a href="https://github.com/cs-lean/cslib/tree/main/Cslib/Computability/CombinatoryLogic">formalisation of Combinatory Logic</a> to a project developing a general-purpose computer-science library.</li>
+
   <li><a href="https://thomaskwaring.github.io/f-norm.pdf">Notes</a> on Girard's strong normalisation theorem for System F (polymorphic lambda-calculus). Also includes some discussion of the relationship to Gödel's incompleteness theorems and second-order Peano arithmetic, expanding on some fairly cryptic remarks in Proofs and Types. (September 2020.) I gave a talk to the <a href="https://cglseminar.github.io/">Computation, Geometry, Logic</a> seminar based on these notes (July 2021, video lost to lockdown restrictions).</li>
 
   <li> A <a href="https://thomaskwaring.github.io/adsn_poster.pdf">poster</a> and <a href="https://doi.org/10.1111/2041-210X.14374">paper</a>, on a partially observed model of invasive species control, published by <em>Methods in Ecology and Evolution</em>. Work conducted at the Melbourne Centre for Data Science. (July 2023, <a href="https://thomaskwaring.github.io/pomdp_supp.html">supplementary material</a>.) </li>