Bisimulation as path type for guarded recursive types

Rasmus Ejlers Møgelberg, Niccolò Veltri

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based o…