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

Datum objave: 4. 12. 2017
Seminar za temelje matematike in teoretično računalništvo
Torek, 5. 12. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19

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.