coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ben Knoble <ben.knoble AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Diagram showing evolution of program logics?
- Date: Sat, 16 Apr 2022 10:15:34 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ben.knoble AT gmail.com; spf=Pass smtp.mailfrom=ben.knoble AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f171.google.com
- Ironport-data: A9a23:XU3M16qT8N8HnZonBVhlb9puKqdeBmImYxIvgKrLsJaIsI4StFCzt garIBmAOPePamH3Lt1zPYy18BkF75OBm9JmSgs++Xg1Hi4W9OPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHkZqTZMEE/Nszo68wICqtMu0IDR7z+l4 4uo+ZWDYQH9glaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSPE1ZwOJHcxt8iTj9KKChGPoxEp4HudC3XXcy7lyUqclPpyvRqSVg1ZMgWo7kuR25J8 vMcJXYGaRXra+CemurqDLkxwJ55do+yY9p3VnJIlVk1Cd4sTJaFQKPN79tV9Dg1j8FKW/3ZY qL1bBI2NUuYPk0VZT/7DroyhM2Mo2CvagZ6oRWVgogw7nbK0iBuhe2F3N39I4TWH625hH2wr WXfum/9HxsyL82a0TPD83S2h+aJkzmTZW4JPLix9/ovmV7Kg2JKV0RQWly8rv20zEW5XrqzN nD45AIR9/lr8nC7EOLCQjuqm3e8vT8eBOR5RrhSBB629oLY5AOQB24hRzFHacA7uMJeedDM/ g/Z9z8OLWw/2IB5WU5x5Z/P8mzvYXl9wXsqIH5bHVFcsrEPtalq1kqXJuuPBpJZmTEcJN0d6 zWDrSx7nrZKyMBSiPz98lfAjDah4JPOS2bZBzk7vEr1s2uVh6b/P+REDGQ3C94edO51qXHc7 RA5dzC2trxmMH10vHXlrB8xNL+o/e2ZFzbXnERiGZIsnxz0pSLyLdkBv28jfx42WirhRdMPS B+D0e+2zM8DVEZGkYcqC25MI5hynfm5TYqNug78N4IVOcAtHON4wM2eTRfIgzqFfLkEnqY4N pOWGftA/l5LYZmLOAGeHr9HuZdynn5W7TqKGfjTkkr6uZLDOyb9YepUaDOmM7FihIvZ8VW92 4gFa6OilU4EOMWgOXm/zGLmBQpVRZTNLcum9ZI/my/qClYOJVzN/NeImO16Kt05xfkN/goKl 1nkMnJlJJPErSWvAW23hrpLMdsDhL5z8iA2OzICJ1Gt1yRxaIqj9vZNeJ4+fL1h/+tmlKYmQ /4AcsSGI/JOVjWXo2RHPceh9NRvJEaxmAaDHyu5ezxgLZNtQgr+/NW7LAbi8S85CDW66Jklq Lq62wKHGpcOHlwwDMvfZP+14Um2uHwRxLB7U0fSc4tcfUzt9M5hLCmo1q07JMQFKBPiwDqG1 lbOUU1I+7WV+4JsqYvHn6GJqYutAtBSJEsCEjmJ96uyOAnb4nGnnt1NXeOOSjbXCzH59aCkU uNKlq2uPfACmmFKhIpyCbNcy6wzuon0rLhAwwU4RXjGYgj5Cr5kJXXaj8BDurcXmu1csAqyH 1uMo5xUYOrQfsziF1EVKUwuaeHajaMYnTzb7PIUJkTm5X8ooODWDx0KZxTc2jZAKLZVMZ8+x btzssAh7QHi2AEhNcyLj3wJ+mnQfGYMVb4r6sMTDIPx0FZ5z1hDZdnFCXaz7sjQMpNDNU4lJ jLSj63H3uwOyk3Hens1NH7MwesN2shU6U4SlAcPdwaTh97Ipv4rxxkNoz45eQJYk0dc2OVpN 2k3akB4KM1iJduzaBSvgoxtJ+1AOPFd0kn4yl9MjW6ACkfxCTWLI2o6NuKAukse9gqwu9SdE K6wkA7YvfTCJakdHRfenWZqrvXiSZp68QiqdAWPAZGeB5djCdb6qvbGWIfLwicLxes+gUTGo a9h++MYhWgX88IPi/VTNrR2Hoj8hPxJyKKujB2hEG408bngRQyP
- Ironport-hdrordr: A9a23:amaOQap1nbNBD2u2gx8Kcq0aV5oGeYIsimQD101hICG9Ffbo9f xG/c5rtiMc7Qx6ZJhOo6HnBEDtewK4yXcx2/hrAV7dZniehILYFvAH0WKK+VSJcE3DH6xmpN 9dmsBFaeEYZmIK6voSjjPIaerIA+PqzElrv4rjJrtWIj2CE5sQkjuRwzz0LnFL
- Ironport-phdr: A9a23:k5HMKBMgZcZtgudKmdsl6nbtBxdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv68r1Q6WFtqBo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6s95HJfglFgDiwbbxwI RmosA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5 KlpVRDokj8KOCI2/m/XhcN+kaxVrhGvpxN93YDaZ5qYO+B8c6PYZ94aRXZNU8RXWidcAo28d YwPD+8ZMOtFsYb9oUYFox64BQmrH+zvziFHjWLx0KIhzeshFxvK3A8mH9IJq3vUqMv6ObwdU eCw1qbIzDHDY+lK1jf67YjFaxYsquyDUrxsa8Te01UvFx/bgVWKr4zoJzOY2vgQvmaU4ORsS /6jh3ImpgxwrDWhxtohhInXi44JxF3I6yd0zogoKNO3SUN2fMCpHYVeuSyGN4V7Td0vTm9ut S0nybMGoYa2cDYWxJkj3RLSaPyKf5KW7h79SuqdOyp0iXB4dL6nmRq/8FSsxvD5W8S0zFlHo S9In9bCu3wRyhDe78iKR/Vh8Uu93DuAzQDe5+FELE0xiKbUN5Esz7A1m5YNrEvOHSr7l1/og KOIakop/PWj5f79bbX8vJCcMpd5igHgPaQqncyyGeE4PRIPX2if4Oi8zb7j8VDgTLVEk/E7k LTVvIrVJcQcoa65DAtV3Zg55xmjCDem1cwUnXgBLF1bZBKKl5blN03KLfziDvqyg06gnCl1y /zYJLHtH5fAImXbnLfkZ7l96kpcyAQpzdBY4pJZEqoOL+z1WkPrt9zYCBg5PBeww+n5E9h92 YYeVniOAq+dKq/drViI5uc3L+mKf4AaoCz9JOQ95/7ykX85nkcQcbSx0ZsNdH+4BuhmI1meY Xf0ntgBFn4KshMiQ+zulV2NSiVeZ22yXqI5/jE0EpiqDYbFRoC3gbyOxj23HpNMZjMONlfZG nDxMo6ARv0kaSSII8YnnCZXe6KmTtoL2Bfmlwn9wb5qZr7e9ytetpTk3tx4z+LWnBA2szdzC pLOgCm2U2hokzZQFHcN16dlrBklor/i+a1xgvgDUMdW++sMSQAic5jV0+19Ddn2HAPHZNaAD li8EZ29GT9kaNU3zpcVZlplXc24h0XJ0izsALkSnbiGLJMx+6PYmXP2IpU10G7IgZEolEJuW c5TLSujj697+RLUAtvDnkPflKCtf6AR9CHI/WaHi2GJuRIQSxZ+BIPCW31XfU7KtZL560fFG qepEqgiOxBdxNSqL6JLbpjwjgwDSq68YZLRZGW+n2r2DhGNrl+VRKztfWhVnCDUCUxf1hsW4 W7DLg8mQCGov2PZCjVqU1PpeULlt+dk+ju9SQcvwgeGYlcEtfL98wMJhfGaV/IY364V8CYnp TJuGV+h3tXQQ9Oergtlda9YbJsz+lBCnW7esgV8ONSnIcUAzhYUfgIxvEXp3RF6IopFmMku6 ngtyUs6KK6V1k9AayLNxYr5afXcLmj/+gzqaraDgAmPlobLvP1VsrJh9Ayw2WPhXlAv+Hhmz dRPhn6V55GRSREXTYq0SUEvsR5zu7DdZCA5oYLSz3xld6eu4Vqgk5okAvUozhG4cpJRKqSBQ UX4HstcBM6pIugns1esZxMAeutV8eRnWqHuP+vDw6OtMOt6yXisgGIB44Z62EaB3yV5Q+/Mm Z0CxrvLu2nPHye5h1CnvMftnIlCbjxHBWuzxx/vA4tJb7Fzd4IGYYu3C/W+3c42x5vkWnoDs UWmG0tDw8ixPxybc1362wRUk0URu32u3yWinXR4lDQgr6zX2yKroayqfhcBfG1NQ2NmgH/jJ IG1i5YRW03gYwUylRSj7Fr33OAB/PU5fzSVGx0SOXGpdilrSeOou6CHYtJT5Z9N020fS+m6b V2AC/b8rxYczyL/Dj5bzTE/eSutv8axlBh7hWSBaXdr+SCBKIcgmFGFvoaaHKEIjV9kDGFih DLaB0axJYys9NSQzNLYt/ymEnmmTttVeDXqyoWJsG2643drCFuxhaPW+JWvHA4k3Cv8z9QvW z/PqUO2aITtkae8Nuhjc2FnAVb974xxHYQ0we5SzNkAnGMXgJmY5y9Nm2r1d9Zd3qj6YVICQ DcKx5je5w2viygBZjqZgon+UHua2M5oYdK3N3gX1iwK5MdPEK6I7bZAkHg9sh+ioAnWe/Q4g iYFxK5k9isBm+9Q8llIrG3VEvUIEEJfJyCpixmY84X0svBMfGj2ObmoiBglwJb4XenE+F0DH i6+IMtqHDcsvJsjdgiXizuqtNmiIJ6JPLdx/lWVi0uS0bYTccpr0KJM3W09YSr8pSF3lbB91 0A/m8Hi+tDAcT0l/brlUEECcGSpIZpCoHe1yv8O+6Tel4G3Qsc+RnNSBsauFbTwV2tM/fX/a 1TXSG168yjEX+qZRUjFsQ9nty6dSs/wcSjGeD9Bi40lHUf4RgQXgRhIDm9iz9hpS0bznpynK AAguXgQ/gKq8EISjL84cUCuCCGH4175IjYsFMrFdUQQtFoToRyPd5TZt7MWfWkQ6JSlqEblx nWzQQNOAClJX0WFAwumJbyy/Zzb9PDeAOOiLvzIaLHIqOpEVv7Oy4j9mo1hty2BMMmCJBwAR 7Uyx1ZDUHZlGs/YhyRHSioZkDjIZtKaoxH08zN+r8S2+vDmEAz14o7HB7xXONRpsxe45MXLf /aXnzp8IC1E24kkwHbJzP0G3wdXhXgxLn+iFrMPsSOLR6XV2+dWAxMddyJvJZ5I4qY7jWwvc YbQjtL40KI9j+ZgUQ8UEwy83JvzP4pTfDjuUTGPTFyGP7mHOzDRlsT+YKfnDKZVkP0RrBqo/ zCSD07kOD2H0TjvTRGmd+9W30T5dFRTvp+wdhF1BC3tVtXjP1exPdkxjjsxy7k5rnzPPG8Yd zN7dgkey9/YpTMdmfh5F2FbuzB9KvKYni+C8+TCApMfsP8uGyct0uwDvy18xLxS4yVJAvdyn WGBy7wm60Hjme6JxD19VRNIoTsen4OHs3JpPqDB/4VBU3LJlPrixWqVAhUO4dBiD4+200i14 tfKnaP3bjxF9oCMlSP9L83dKcbCKXl4dBSwR2eSAwwCQjqmc2rYgh4F+Mw=
- Ironport-sdr: BQFN1ZfWNolk7FhTrgvZhJSYJ/QEwQF29+84TDI1TwlMVlqnIdeYRnbXhLbbmsqa8WJevAZnA+ YxWPdFVTW/FYNAzRBP5cUps+dCVTIt7a291GOCphQEztTp9YC56CgR6XzdbEM+mfwM+jkPxD/G sOrIeUSMsm1zZ4o7E06aNKt6HBmUk2R/PWtXVAGGcxxDicn+70Epl8dtqGjnlII5Vomv20TnaZ JnQR3uDxWD5H2cDIVXI/WOqReyuygSh58qtrzQzk3eUVFRAW7xXEXdWL0araOMOufQCPypJumk BdRLab/7BZ/HKYilFqtKDJSy
I also recall a slide from one of Ralf Jung’s talks on Iris about the many separation logics that could be of interest. Unfortunately I do not have the reference handy.
D. Ben Knoble
Le 15 avr. 2022 à 14:12, Stefan Muller <smuller2 AT iit.edu> a écrit :
Hi all,
I vaguely remember seeing once, in a paper and/or conference talk (helpful I know), a web-like diagram showing the history of various program logics (transitively) influenced by Hoare Logic. I'd like to show something like this as a "there's more out there"-style wrap up in the course I'm teaching, but can't seem to find it. Does anyone know if such a thing exists or if I'm making it up?
Thanks!
Stefan
--
Stefan Muller
Gladwin Development Chair Assistant Professor
Computer Science Department
Illinois Institute of Technology
- [Coq-Club] Diagram showing evolution of program logics?, Stefan Muller, 04/15/2022
- Re: [Coq-Club] Diagram showing evolution of program logics?, Lennart Beringer, 04/15/2022
- Re: [Coq-Club] Diagram showing evolution of program logics?, Ben Knoble, 04/16/2022
Archive powered by MHonArc 2.6.19+.