The article isn't loading for me right now, but I thought I'd mention co-inductive types and how they relate to "interaction".
In Coq, co-inductive types are used to model infinite objects like (never-ending) streams or (non-terminating) program executions.
Inductive List (A: Set): Set :=
| Nil: List A
| Cons : A -> List A -> List A.
CoInductive Stream (A: Set): Set :=
| SCons: A -> Stream A -> Stream A.
Fixpoint len {A: Set} (x: List A): nat :=
match x with
| Nil => 0
| Cons _ y => 1 + len y
end.
CoFixpoint ones : Stream nat :=
SCons nat 1 ones.
If you want to talk about how systems interact with the world, you can use bisimilarity relations to prove "these two systems interact with the world in the same way".
You can also use co-inductive types to embed the temporal logic of actions (TLA) in Coq; TLA is the language Leslie Lamport works with for "Specifying Systems".
In Coq, co-inductive types are used to model infinite objects like (never-ending) streams or (non-terminating) program executions.
If you want to talk about how systems interact with the world, you can use bisimilarity relations to prove "these two systems interact with the world in the same way".You can also use co-inductive types to embed the temporal logic of actions (TLA) in Coq; TLA is the language Leslie Lamport works with for "Specifying Systems".
* http://www.labri.fr/perso/casteran/RecTutorial.pdf
* http://www.amazon.com/Specifying-Systems-Language-Hardware-E...
* http://en.wikipedia.org/wiki/Bisimulation