**Title:** Hyperduals and Hyperdual Extensions in Isabelle

**Speaker:** Filip Smola

**Abstract:**

In my talk, I will discuss new developments in my mechanization of hyperdual numbers in Isabelle, in particular the hyperdual extensions of real functions. I will introduce how limits and derivatives are defined for hyperduals, along with the mechanized proofs of those properties. I will then describe the idea of a hyperdual extension of a real function on the example of sin and cos. I will also describe my current best guess at a general locale for these extensions, along with a number of example instantiations.