Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Diagram showing evolution of program logics?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Diagram showing evolution of program logics?


Chronological Thread 
  • From: Lennart Beringer <eberinge AT cs.princeton.edu>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Diagram showing evolution of program logics?
  • Date: Fri, 15 Apr 2022 14:28:32 -0400 (EDT)
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=eberinge AT cs.princeton.edu; spf=Pass smtp.mailfrom=eberinge AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT violeteyes.cs.princeton.edu
  • Ironport-data: A9a23:xOmkOKtrk5Ny/I1CSgEv6aYPSufnVB1bMUV32f8akzHdYApBsoF/q tZmKW+AbP2IZzDzco0kaYi+pE4Pu8fXmN41SAE5rCsyH3hBgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCY0idfCc8IMsboUsLd9UR38g52bBVPyvX4 Ymo+5GGZQf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnYOvQiEpMIjHochHXUZYGDpUDbVjoZaSdBBTseTLp6HHW2XtxPFjEEwnMJZe8f0xGXtP8 /cVNDcLKB2PmopawpriELkq3515apCwYsVC5xmMzhmBZRoiaZ3JTr/L49BV9DwrwNhUHPDVa tYeb3xiYAmojxhnYQ5GVMhgzbfAan/XWjtd+FCT+aoO80vyliJx4OnvMcHFdYnfLSlSthvI9 zmeogwVGCoyP9uGjDGB73iEnf7KhSq9WYQIFbT++OQCvbGI7nISDxkbSVaqrOL/gVX4Q8heL UcZ5i0o66U+6SRHU+URQTWnv3WivhA5UON8SeNl6AqW4JrMxl+wUz1soiF6VPQqs8o/RDoP3 1CPns/0CTEHjIB5WU5x5Z/I9WjsaHh9wXsqIHBYE1BVu7EPtalp1nryosBf/LlZZzEfMQnqw jaBoTQ5gd3/ZuZTh/jnpTgrbxqKq4eBbAMv/QjGNl9JAytnZYmhapCl+FXAq/1bap6DT1+Ks WQDnY6T4P1m4XCxeM6lHLVl8FKBvqjt3NjgbbhHRcVJG9OFoSXLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp2nPi5RIS8B6yNPrKih6SdkifboEmCgmbMgwjQfLQEy8nTx L/CKpnwUixy5VpPlWXtLwvi7VPb7n1ulDiLGPgXPjy/y7uYb3OJTrFNLV2PcO0j96KYsW3oH yV3aqO3J+FkeLSmOEH/qNdLRXhXfSlTLc2n8KR/K7/cSjeK7Ul8Upc9N5t6INc790mU/8+Vl kyAtrhwkQOh3iyWdV/XMhiOqtrHBP5CkJ7yBgR0VX7A5pTpSd/HAH43e8RlcL852vZkyPIoH fAJd9/ZXKZEUXLf4TUbZpThq4okeRi23FrcMy2gaTk5XphhWw2UpoO4JlWzrHEDXnitqM8zg 7y8zQeKE5MMSjNrANvSdP/ynUi6umIQmb4qUkaReotTdUzg/ZJEMSv0ivNrccgAJQ+amGmRz ECOGxYeruTRpIlz/dXU3PjWo4CsGup4P0xbA2iGserqbXeGpjKumNYSXvyJcDbRUHLP1J+jP egFnevhNPAnnUpRt9suGrlm+qsy+t/zquII1Q9jBnjKMwymB745eSuG0MBDu7d3y6ddqBexX k7TqNBWNa/QZpHuCxgJPgsjZemf0vdSlzXPtKxnLEL/7S5x3byGTUQPY0XQ0HIBdON4YNE/3 OMsmM8K8Aju2BMlP+GPgj1Q62nRfGcLVL8qt81CDYLm1lgrx1VFbcCOAyP6+svQOctNNU0nP jKFibGEjK8a3lDDdXE+CX/Lm+dRmM1W6hxNyVYDIXWPm8bE26NrgEUPrWxvQ1QH1AhD3sJyJ nNvZh98Kqi59jt1gNROAjK3EAZbCRzFokH8lwkTmGvCQxX6X2DBNjdia/iM+0QU729NcyMd9 6re0HzkVz3nYMb3mCY+RBc9+fDkSNVw8CzEmdymQpjZQ8FkPWK9j//8f3cMpjvmHdg11R/Oq uRd9eptbbH2aHwLqKohBojGjbkdRXho/oCZrS2NIU/IIY3dRN128SaPLES8Zs5cKueM+lT+E 9ZvIMlCSxO4kiuCs1j3wIYSdqRskqdBCMUqI9vWyawu6tNzbQaFdLrb7W7mnm4tSNhylsB7J 4/MH95HOnLFnmNawgchs+EdUldVorA4iMnU1/vz6P8IEZkOrOZqN0w+z9NYeplT3BRPp3qpg e8IW0MaIyGOB2ihc0sA35iv3zmJFO4=
  • Ironport-hdrordr: A9a23:9eDsPam9n3fOqxA7axWF57LqfRzpDfIT3DAbv31ZSRFFG/Fw8P re+MjztCWE7Qr5N0tLpTntAsS9qDbnlKKdgrNhX4tKPjOJhILAFugLhrcKgQeBJ8SZzIJgPM xbAstD4ajLfCBHZLHBkXCF+rgbr+VviJrY49s2mE0dKj1XVw==
  • Ironport-phdr: A9a23:FXA//BcvtnnnLmMLk6HS66uwlGM+PdTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWTG9yKtrkd0bGempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffRtEiCCgbb52L Bi6ohjdutcYjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0Q rNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6 apgVRnlgzoFOTEk6mHaksJ+gqJBoBy/pBJwwYDUbpyaO/Vica3dfNQURXZaU8ZNVSFOHp+wY pETA+cDO+tTsonzp0EJrRu7HQSiAv3gyjlOhnDsx606z/kqHBzY0ww6HtIOtnvUo8vvNKwPV u260rLHwivZb/NX3zf955bHfws9rvGXR75wadDRyUgpFwzZkFqQtYvlPzWP2usTrmeb8vNtW OSygGEotw9/uCKgxtswiobXnIIVzEjJ+CR9zYg1JdO1RlB3bNqrHZZQuC+XM4t7T8E/T2x0v Cs3y7IItJq7cSQX1JkqxBrSZvKaf4WJ/B/uSOmcLzd6iX9jZbmxiRGy8U26xe39UMm5yFdKr i5Fk9bWrXACyQbT6seZRfp95Euh3yiA1xzV5+pZIk40jbLWJ4M/zrMzjJYfrFnPEjHslEnrg qKbd18o9+io5uj/f7nquoWQOoxuhgz8NqkigNKzDOo3PwQWQmSX5+ex2Kf+8UHkXrlGlOA6n 6fYvZzAJMkWpqi0CBJP3Ik58RawFTKm3cwYnXYZKFJFfwqKj5boO1HJJPD3E+u/jEqskTh13 PDKJKHuAo7XInjbirfhfLB95FJCxwovytBf4YhYBa8cL/LuQkPxtdrYAQElMwGs3urrFtZw2 pkDVW6SHKOVKr7evFGJ6+41I+SBZJcZuDPnJPgk4/7ug2U5mVgYfaSxw5QYc263Hu5nI0Wfb nrjnMwMHnsRvgYkVOzqklyCUThPaHmsQ6I84Tc7BJi4AojeW4ChmLqB0zyjEZ1Mem9GEkyME Wvvd4icRvsAcDiSLdN5kjwYSbihTJcs2g2ptA/j0rZoMu7U+jADup/4z9h05+jTlQko+jBuD sSd1XuNT2BukW8SST82xvM3nUsowVCalKN8nvYQQddU/rZCVhowHZ/a1e1zTd7oDFH7c8+NW WqhF/GrBzc4VM556dIUYkByFs/q2h3J0jCrBbAYv7eQQoQu86TX0mT2IYBwx2uQh4c7iFxzZ sZJM2S8muZV+hLSAYHEiQ3Nmqynb6Ua0yPl/3zF1XCPukpVTAl2F6jJQCZMNQPtsd3l6xaaH PeVArM9P14ZoSbjAq5Da9mzyE5DWO+mItPVJWS4h2a3Ax+MgLKKdovjPWsHj23GEEZRtQcV8 D6dMBQmQD+7qjfTBjF0FFTgbmvn6q9msnK9RUIoyAfMYkF8hPKu4hBAvfWHULsI264c/iIoq jF6BlG4it/cBsCBoQVsVK5HJ8sn4VFM2H7esUpwMoHzZ7t6iAsmeh9s91jryw0xCohElp0yq 2g2yQNpNa+C+E1AcDeVwZ3hN6aRIXK05AqubaXbxlbYltua58/j8dwerFPu9EGsH0smqTB81 sVNlmGb7dPMBRYTVpT4VgA28QJ7rvfUeHt14YScznBqPaSu112Kk9s0GOsozAqhdNZDIeuFE gH1CcgTG8mpLqQjhVGoahsOOO0a+rQzOouqcP6P2ajjO+gF/nrugG5K+oF73U+k/DE6UvTJ2 Z0I3/aemAaLSna0jVustNz2hZERfSsbTQ/dgWDvAI9cYLE3fJ5eUD3+ZZTunJMn3MCrBiMLk TzrT0kL08KoZxeIOln03AkKkF8SvWTigyyziTp9jzAuqKObmi3I2eXrMhQdaQspDCFvi0nhJ Y+sgpUURk+tOkIknha/5ED1yoBQv+JnNWjVSkpUeC6wIm1/GPjV1PLKc4tU5ZUkvD8CGum2b EqbTLHwixABlTv5Hm1VySw8cXentoizzHkYwCqNaX10qnTeY8R5wxzSscfdSfBm1T0DXCBki DPTCzBQJvGR9M6P39fGu+G6DSe6U4FLNDPsxsWGvTe64mtjBVu+meqyk5vpC1py3Sj+3thsH SLGyXS0KoTh2r67N+1qVkJzQkfm6sxxF515lM09iIxY1XUBh5qT9GYKii+qa4UdgPukKiNWG 3hWnpbc+22HkAV7I2iMxp7lW3nV2cZna9SgIysX1i8788FWGfKR5b1AkzFypwndz0qZavx8k zEBjPo2vSdA06dQ4VBrl37DRO1PTiw6dWT2mh+F7s6ztvBSbWerK/2r0VZm2MqmB/eEqx1dX 3DwftEjGzVx54NxKgGpsjW754f6dd3Xdd9WuAeTlkKKguJYMpM3mfcijjEhIXj8u3Yo1+k9y xFiwNvp2erPY3Uo56+/DhNCY3f4bc4J+zfigI5VhYCOxYGpFZh9HTNNUZf1B6HNcnpapbHsM ACAFyc5o3GQFO/EHAOR30xhqmrGD5GhM3zEbGlc19hpQwORYVBOmA1BFitvhYY3T0r5oa6pO Fc8/D0a4UT07wdB2v49fQeqSX/R/U+ten81UMTNdUAGqFgbvQGMapLYtqUpREQ6ttWgqgeJN 2CWNRxSDGcCV1CDARbuMqTm89DE96Lw6vOWF/LVev3OrOVfU63N3pezys58+D3KMMyTP35kB vl920xZXHk/Fd6L0zkITiUWkWrKYav57F+k/TZrq8mk7PnxcBzu4o+CF7ZDPM4p8Avwmb2CM eWdmCF/bztUy9sAyGTJx74WwFMJ7kMmP2D3QfJZ7HSLFfmO3PIKRxcAIzt+Ls5J874x0kFWN MjXh8m0nr90g/gpCktUAFzsnsb6AK5Ca2q5NV7BGAOKLOHff22NmpitJ/rnF/sN0bYx1VX4o zuQHk79My7WkjDoU0rqKuRQlGSBOxcYvoihcxFrAGylTdT8axT9PsUk6F9+ibAymH7OMnYRd DZmdEYY5LCa4DlZhPpyM2daqGJ/LO+Pljqe6a/VJotc4p4JSmxk0vlX5ng30e4f9CZfWPl8g zfftPZwolain/WC2zd8FhFV7C5RhYSAsFllP+PU+oQKChOmtFodqG6XDRoNvd5sDNbi7rtRx tb4n6X2MD5e8tjQ8JhUF43OJcmAKnZkLQvxFWueEl4eVTDyfzK65QQVgLSI+3aStJR/tpX8h M9EVOpATFJsXvpST01hGJZqyHZfQDIjlbOHgd8F/jy1t1/JXsRctZ3bUfTUDPnyem/xZVZsb ABO2an5K48eKor9nUFudwsj9GwvM0HLG8hXoytqYxMzpgNA/GUsFgUO
  • Ironport-sdr: 5xjTWGFf09izR+WkntwNPpJOOvz7TcvhWsOeGh9/Y7mDG8wVOQL+NQnsix4aFwjl25P7pvHGjC ltmwJnR6jova/dpsARsHrI9lpUL/tIVFs9doIclGZAqYODWPY3MtR18tjGDXwNyGX2JhTWKYBy 4Y/sKjSvkWDk+YJyuUsyO1qwVwCQo9ePDgRyfNG2ElN59K7D0u2Nz9m3i7YcwrEdlFqrjpx06W sdBuy0RvCVjgO+WIR5ASJAh6UDdWurqQv4WHN67BWAq++aWp3Ar3RMK3V49Ilel7ZgNJXcmTB9 /27UDX2YAfJ/mTbdLIYfodYx

Perhaps you had Ilya Sergey's 2016 slide on page 4 of

https://ilyasergey.net/assets/pdf/slides/2016-Sergey-FCSL.pdf

in mind, which traces various concurrent separation logics back to
Owicki-Gries and hence covers only a fraction of Hoare logic.
Nevertheless, it nicely highlights that there's a lot out there...

Lennart.

----- Original Message -----
From: "Stefan Muller" <smuller2 AT iit.edu>
To: "coq-club" <coq-club AT inria.fr>
Sent: Friday, 15 April, 2022 14:11:38
Subject: [Coq-Club] Diagram showing evolution of program logics?

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



Archive powered by MHonArc 2.6.19+.

Top of Page