We discuss the theory of Lie algebras in Lean’s Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel’s theorem...

Brzozowski introduced the notion of derivatives for regular expressions. They can be used for a very simple regular expression matching algorithm. Sul...

Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-cons...

Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution spa...

The Isabelle Higher-order Tarski–Grothendieck object logic includes in its foundations both higher-order logic and set theory, which allows importing...