Zoo Probabilistic Systems
Isabelle Zoo of Probabilistic Systems: Numerous models of probabilistic systems are studied in the literature. Coalgebra has been used to classify them into system types and compare their expressiveness. We formalize the resulting hierarchy of probabilistic system types by modeling the semantics of the different systems as codatatypes. This approach yields simple and concise proofs, as bisimilarity coincides with equality for codatatypes.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
- Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (2020)
- Lochbihler, Andreas: Effect polymorphism in higher-order logic (proof pearl) (2019)
- Hölzl, Johannes: Markov chains and Markov decision processes in Isabelle/HOL (2017)
- Lochbihler, Andreas: Probabilistic functions and cryptographic oracles in higher order logic (2016)
- Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
- Hölzl, Johannes; Lochbihler, Andreas; Traytel, Dmitriy: A formalized hierarchy of probabilistic system types. Proof pearl (2015)