Talk on Tuesday 21st at 13:00 : Certified Approximations of Elementary Functions

[Nyx Brain, Martin]

Hi all,

Heiko Becker has kindly agreed to give an online talk for one of my
projects. Everyone here would be most welcome. Please note that this
is organised on BST to make company lunch time, so it may be
unreasonably early for folks on the west coast.

Cheers,
- Martin


Topic: Dandelion: Certified Approximations of Elementary Functions --
Heiko Becker

Abstract: Elementary function operations such as sin and exp cannot in
general be computed exactly on today's digital computers, and thus have
to be approximated. The standard approximations in library functions
typically provide only a limited set of precisions, and are too
inefficient for many applications. Polynomial approximations that are
customized to a limited input domain and output accuracy can provide
superior performance. In fact, the Remez algorithm computes the best
possible approximation for a given polynomial degree, but has so far
not been formally verified.

This paper presents Dandelion, an automated certificate checker for
polynomial approximations of elementary functions computed with
Remez-like algorithms that is fully verified in the HOL4 theorem
prover.

Dandelion checks whether the difference between a polynomial
approximation and its target reference elementary function remains
below a given error bound for all inputs in a given constraint. By
extracting a verified binary with the CakeML compiler, Dandelion can
validate certificates within a reasonable time, fully automating
previous manually verified approximations.

Time: Jun 21, 2022 01:00 PM London

Join Zoom Meeting
https://city-ac-uk.zoom.us/j/86907998953

Meeting ID: 869 0799 8953
Passcode: 815373

One tap mobile
+442034815237,,86907998953#,,,,*815373# United Kingdom
+442034815240,,86907998953#,,,,*815373# United Kingdom

Dial by your location
+44 203 481 5237 United Kingdom
+44 203 481 5240 United Kingdom
+44 203 901 7895 United Kingdom
+44 208 080 6591 United Kingdom
+44 208 080 6592 United Kingdom
+44 330 088 5830 United Kingdom
+44 131 460 1196 United Kingdom
Meeting ID: 869 0799 8953
Passcode: 815373
Find your local number: https://city-ac-uk.zoom.us/u/kcYzE4D76K

Join by Skype for Business
https://city-ac-uk.zoom.us/skype/86907998953

--
Martin is now a full time member of staff.

[Nyx Brain, Martin]

Hi,
My apologies but we have been sunk by the challenges of inter-
organisational video conferencing access controls. The seminar will be
happening via teams:

https://teams.microsoft.com/l/meetup-join/19%3ameeting_OTA1ZjdiYjMtOWQ4NS00MzZiLTg0ZTItOWZmMjIwZWIyMTk2%40thread.v2/0?context=%7b%22Tid%22%3a%220d2cf6e6-30f7-4e63-95a4-73e295f62afb%22%2c%22Oid%22%3a%22f3d572c3-4952-4ed5-a24a-616bfe0b0b77%22%7d

Cheers,
- Martin