Email Gateway (Aug 22 2022 at 18:57): Email Gateway (Aug 22 2022 at 18:57):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
Paul-Andre Mellies [1, 2, 3] developed a theory about the relationship
between knots and programs/proofs. I know that there is a repository about
knot theory in AFP [4]. I wonder if there are researchers applying this
theory to practice, and if so, I would like to have links to some
repositories in Isabelle/HOL (or another proof assistant) about the
concrete applications of Mellies' ideas to static program analysis, e.g.,
operational semantics, denotational semantics, Hoare logic, etc. Thank you
in advance.
Kind Regards,
José M.
References.
[1] Mellies, Paul-Andre. "Game semantics in string diagrams." *Proceedings
of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science*.
IEEE Computer Society, 2012.
https://hal.archives-ouvertes.fr/hal-00721662/document
[2] Paul-Andre Mellies: "String diagrams, a topological account of proofs
and programs", OxfordQuantumVideo (video-lecture)
https://www.youtube.com/watch?v=Sr_tEm3Kxc0
[3] Paul-Andre Mellies, "Programming languages in string diagrams",
Mathématiques et programmation (video-lecture)
https://www.youtube.com/playlist?list=PLGCr8P_YncjWX6YHOq1-SyyP7zf4a_E_E
[4] T.V.H. Prathamesh, "Knot Theory", AFP
https://www.isa-afp.org/entries/Knot_Theory.html
Last updated: Nov 21 2024 at 12:39 UTC