Calculating the Q value of a state-action is much more difficult formally than for the original pen-and-paper proof. I discuss my formalization choices and how my current approach to calculating Q values should make proving the Principle of Optimality easier.
Speaker: Mark Chevallier

I will give a practice talk for the 3 minute thesis competition. This will be a description of my PhD work on formalising Euler’s use of the infinitely-small and large.
Speaker: Imogen Morris

I will discuss my research into formal verification of discrete reinforcement learning, with particular emphasis on the possible benefits of this approach.
Speaker: Mark Chevallier