Skip to content

Commit 9771529

Browse files
author
twwar
committed
update cslib
1 parent f528301 commit 9771529

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

math.html

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ <h1>Mathematics</h1>
3737

3838
<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>
3939

40-
<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>
40+
<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/leanprover/cslib/tree/main/Cslib/Languages/CombinatoryLogic">formalisation of Combinatory Logic</a> to a project developing a general-purpose computer-science library.</li>
4141

4242
<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>
4343

0 commit comments

Comments
 (0)