Las FP Syd of 2024 _today_, 27 November

[Jost Berthold]

FP Syd concludes 2024 with a meeting that is all about proofs and formal methods, after a pause in October due to a broken screen.
(While the screen is probably still broken, we have a fall-back solution this time).

Craig McLaughlin Now Serving: A Lean Beefy Prover

Presenting the latest in succulent, lean, theorem-proving technology,
Lean4 is the fourth major revision of this delicious recipe. What makes
Lean4 so finger lickin' good?

• Expressive dependent type theory foundations
• Self-hosting and fully extensible via meta-programming
• Efficient code generation to C
• Custom-built hygienic (i.e. capture-avoiding) macro system subsuming syntactic notations and tactic languages
• Fully-fledged functional programming facilities including type classes and state-of-the-art garbage collection techniques
• Active community, industry support, and high-quality learning resources and documentation

There's much to enjoy about Lean4, so gather 'round the good stuff and
we'll explore as many of the above as time permits with references on
where to find out more. Oh, and would you like fries with that?

Alex Mason Functional Programming as a Tool of Thought: Haskell & Clash for higher level hardware design

As usual, doors open at 6pm for the talk to start around 6:45. 
We hope to see you tonight!