Andrej Bauer: Command-like expressions for real infinite-precision calculations

Joint work with Sewon Park (KAIST) and Alex Simpson.

Abstract: I will discuss a minimalistic programming language for real-number computation, with emphasis on how to formalize the language in Coq. The formalization uses coinductive definitions and modal operators to describe non-deterministic aspects of program behavior.