## Sewon Park

### Toward verified real computation

This talk introduces a simple imperative programming language supporting
real number computation that can model core fragments of existing
imperative exact real number computation software (e.g., iRRAM). We design
its sound precondition-postcondition-style verification calculus that can
be used to prove various exact real computation programs. Finally, we
extend this framework rigorously with other continuous objects such as
complex numbers, sequences, matrices, functions, and so on.
We also take a quick look at some recent progress on exact real computation
program extraction from proofs based on axiomatic real numbers. This
approach enables us to achieve verified programs in exact real computation
software that are functional such as AERN.