See report Leveraging Advanced Coinductive Techniques in Coq for Formalizing “Recursive Subtyping Revealed” generated by Gemini
See report Exploratory Directions in Bisimulation - Pre-evaluating Future Applications generated by Gemini
References
- https://dl.acm.org/doi/10.1145/2933575.2934564 Coinduction all the way up
- paper home: https://perso.ens-lyon.fr/damien.pous/cawu/