On December 5 I got the change to talk about Iris-Lean at the New Jersey Programming Languages and Systems Seminar. My slides are available in pdf.