Hyperduals and Hyperdual Extensions in Isabelle

Date: 14th February 2020

Time: 14:30 - 15:00

Talks

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.