Andrej Bauer: Command-like expressions for real infinite-precision calculations
Source: Mathematics and theoretical computing seminar
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.