Presenting at #types2025, on playing with constructive negation in Idris2 for fun and profit.

Thanks unnamed colleague for the photo!

(Yes I am barefoot).

Zelfgemaakte #kruidnoten! De speculaaskruiden was ook zelfgemaakt, Britse winkels kennen de kruiden niet.

Dutch festive biscuits. If you know, you know! Another batch might make it to LT1310 & 14th floor.

Typing derivations are great at *showing* the result of type checking.

Derivations are not so great at showing the communication structure.

Given a bidirectional account of the STLC with Nat (Zero and Inc) with term level annotations.

For my 101, I was thinking of showing the derivation for:

\(
(\mathsf{the}\,(\mathtt{Nat}\rightarrow\mathtt{Nat})\,(\lambda{(x)\cdot(\mathsf{Inc}\,x))})\,\$\,\mathsf{Zero}
\)

As the attached MSC chart. (Not yet worked out how to squeeze in context growth and equality checks)

Diagram might be too much change.

I have experimented with a graph representation but let us stick to standardised notation ;-)

I’ve always loved Edge Cliff.

The name is so literal, it’s on the edge of a cliff. I have fond memories of tutorials in the building, not to mention submitting paper essays to a letter box. Just before VLEs took of here.

More so, I love that on the surface the two Philisophy departments (Moral Philosophy, and Logic & Metaphysics) are separate. When you go through the door, however, it’s just the same building that’s been knocked through together.