coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ACL2-2023 Second Call for Participation

From: Matt Kaufmann <kaufmann AT cs.utexas.edu>
To: acl2 AT utlists.utexas.edu, agda AT lists.chalmers.se, cicm-members AT lists.informatik.uni-erlangen.de, cl-isabelle-users AT lists.cam.ac.uk, coq-club AT inria.fr, fm-announcements AT lists.nasa.gov, fmcad AT utlists.utexas.edu, hol-info AT lists.sourceforge.net, lean-user AT googlegroups.com, mizar-forum AT mizar.uwb.edu.pl, nuprl AT cs.cornell.edu, pvs AT csl.sri.com, theorem-provers AT ai.mit.edu
Subject: [Coq-Club] ACL2-2023 Second Call for Participation
Date: Sat, 14 Oct 2023 11:33:12 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kaufmann AT cs.utexas.edu; spf=Pass smtp.mailfrom=kaufmann AT cs.utexas.edu; spf=Pass smtp.helo=postmaster AT newman.cs.utexas.edu
Ironport-data: A9a23:jbVpPaxtn+KPBQogHZ16t+f/wirEfRIJ4+MujC+fZmUNrF6WrkVWm jAZDTvTa/bfYmCgL98lYd7n8BwCuZ+Gzt83S1ZprVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2Uc3l48sfrZ80o35aiq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFO34v9KEVtsBbYdoMF5BVlc8 N5fCR40O0Xra+KemNpXS8Fqi9smJc+tN5hZp21t3TjCS/sqXPgvQY2Tv48ejGx235sfW6+HP 6L1ahI3BPjESx5GJ1kSAZQ4tOyzwGTjfi1RsxSYqbdfD237klwuiuCxboa9ltqiQ8hoklSZ/ 2T9wWniGR1dP5uY5wCp7Sf57gPItX+kBd1LfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGq6Ut8UWtCNLmGQCkrW6NpVgRV8c4//AGBB+lkYvexxuDXFA/S2RmZtgepsoUAh0E7 wrc9z/2PgBHvLqQQHOb076bqzKuJCQYRVPugwdfF2PpBPG4/ukOYgLzosVLS/bv3oSpcd3k6 3Xb83dl3Op7Ydsjjf3TwLzRv967SnElpCYc+x7LX2TNAuhRO976PtbABbQ2EZ99wGuxSFSeu XEC3cOFqv0SAIGEj2qATPhl8FCVCxStbWa0bb1HRsdJG9GRF5iLJ9E4DNZWfhcBDyr8UWW1C HI/QCsIjHOpAFOkbLVsf6W6ANkwwK7rGLzND66FMYAUO8gsKFDfp0mCgHJ8OUi2yiDAdolkZ v+mnTqEUR729Iw9nWbnHr11PUEDnX9krY8seXwL50j4jOXHDJJkYaoDMUWDdPs48LLMpwud7 9tPPtDCwgkXWfDlfijRmbP/3nhWRUXX8ave8pQNHsbae1IOMDh4W5f5n+l9E7GJaowIz48kC FnmARQGoLc+7FWaQTi3hodLM++zA80m9yhnZ0TB/z+AghAeXGpm149HH7NfQFXt3LULISdcH 6hZKfaTSO9CUCrG8Dk7ZJzw5t4qPheyiA7Ee2LvbDEjdtQyD0bE6/31TDvJrSMuNyuQsddhg ruC0giAf4EPaT4/B+nradWu7WiLg14jpMxIUXH1f+ZjIHfXzNAyKgjarOMGHMUXGBCSmhqYz 1m3BDkbl8nsoqg00tvClP3do6iXT9pOO1doIFOCzLepNBv1+nio7p9AXd2pIxHcdjLQ04eza dpFy8rTNKU8o29LlI5nApBXwrkb9fK2l4RFzw9hImrHX26rBpxkPHOC+8tF7Y9J+ZN0piq0X Rip1uRBGLDUJv7gLkEdFDAlYsuHy/sQvDvYttYxAUfi4R5I7Ki1alpTMzaMmR5iAuNMaq19+ tgYuekS9wCboTgpOIzfjilrqkK9HkZZWKAj7pwnEIvnjzQw8W57YLveNH7SwIqOYNByIEUVM meqpK7dtY99mGvGUVQOTEbo48QMpK4zqChrzUADLWungtDqpOE69zwP/CUVTjZ69ARm0eVyM G1VbEdKC7iq+hF6oM59B1KcGwFKFUCdyGzMyn8itm7Qf2+3XEPjcUw/Pues+hgC0mR+JzJ0w pCR+FzHYx3LIv7j+zQUYlF0jcDjQfha1BzwqOr+E+urR5AFMCfY2Imwbm82mj7bKMIWhnyfg 9J1/ex1OJbJBQRJr4IVU4ClhKktEjaaL2l/QNZkzqMDPUfYXBqQgTGuCUSASvlhFszw032TK pJRf5pUdhGEyiyxgCgRBvcML59KjfcZ3oc+VY2xF1EWkYm0j2RPgMrL+znclV0bZYxksfwAJ 7P7cxOAFW2thkVopVLdkfkcOkeFZYgrWQ6t+sG07+QDKLwbus5Ob0wZ8+W5rleVAiRd7jOWu wLyPIrLw9xYzYlDsZnIF5tACz6VMvL2bvyDqyqoguRNbPTOEMbAjBwUoV/ZJDZrPaMddtB0t LaVuvv14R/hkJMpdV6BgLiHNa1CxfvqbdptKsitcUVrx3qTavHj8z4o2j6eK6UQtPh/+8P+Z Q+zSPXoRO4vQ90HmUFkMXlPIS08VZbyQLzr/x6mjvK2DRMY7wzLAfWn+VLtbkBZbiU4AIL/O CClp8eR4s1kk6oUCC8mH/1GB7pKEG3nU4YidPzzsmCWMDD5yBfK8L7vjgEp5jz3G2GJWpSyq 47MQh/lMg++oufUxdVeqJZ/pQATEG07u+QrY0YB4JRjvlhW1oLdwTg1av3qy624kxAeELn+a S7IZW1kAj67QChJYRznptnvQ29zw8QQb8zhKGVBE1y8Mk+L6EGoWdONNRuMJ199YX3+0Oy3I MpY93HtVvR06o88Xv4dv5RXns8+rs43BRs0FYTVmNe0HgoTEbwRknFtAWKhkMAB/97lzC32G IT+eYyIrIxXh6I8/QaMtkO5wC0kgQ4=
Ironport-hdrordr: A9a23:ZbTJb6/6lDUH5G8Lmqtuk+DaI+orL9Y04lQ7vn2ZKCYlF/Bw8v rEoB1173/JYVoqN03I+urwWpVoI0mslqKdiLN5Vd3OYOCMggqVxe9Zg7cL81fbdxEXeYNmpM NdmndFebrN5YkTt7ed3DWF
Ironport-phdr: A9a23:W9EoOBfOVccZowUvoFw+xSPulGM+INfLVj580XLHo4xHfqnrxZn+J kuXvawr0AWZG9uDoK8bw6qO6ua8AzJGuc7A+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohA c5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/I Au1oAnLt8QanYRuJ6YzxxDUpndEZ/layXlnKF6Nnhvw/Nu88IJm/y9Np/8v6slMXLngca8lV 7JYFjMmM2405M3vqxbOSBaE62UfXGsLjBdGGhDJ4x7mUJj/tCv6rfd91zKBPcLqV7A0WC+t4 LltRRT1lSoILT858GXQisxtkKJWpQ+qqhJjz4LIZoyeKfxzdb7fc9wHX2pMRsZfWTJcDI2yb IUAAPYOMP1Er4XhvVYCsQeyCRWwCO7p1zRGhmX23ao/0+k5Fg/JxhAgH84Tu3rRttr1KakSU eWvw6nOyzXIcvRb2TTn54jVfBAhpOuDXbR2ccfK1UYvDBnJjkiMqYP7MDKazP8Nv3KF4OV9S OKikmgqoBx+rTaz3MkjkJXJhp4LxVDe8yV02Jo5K92kREN4btCoDIVduiOeOoZ3Tc0vXWBlt Ts5x7AYupO2fiwHxZUnyRPbdfGKcIaG7wzgWeqNPDt1hG5pdbO5ih2v/0agzej8WdO10FZMt idFj8XMuW4C1hPJ8ciLUOVy8Vq82TqXzQDc9O5EIU4zlavUMZIu3rkwlp8VvE/eHSH2gF37g LKIekgn4OSl6Orqbq/7qpKSM4J4kBzyPrkylsCnHOg0LAsDU3KY9OmyzrHv4EP0TbFQgvA2k qTUto3RK94Bqa6jGQBV154u6xahADei19QVhX8HI0xLeRKClYfpPUvCL+zjDfulnlSsjClkx v/cMb36GJnCMGXMkKr5cbZ87U5T1hYzwMhC655KCbwNOvH+V0HruNDFABI0Nxa4z/v6BNlhz o8eXHiAAq6dMKPcq1+I4ecvLvGPZIAPpTb9Jf0l6OTojX8/glISYbKp0YEKaHCkAPtnLF+WY WH2jtgfDGgKoxIyTOrxh1KaSz5ce26yX74g5jE8EI+qEJ/PRpqxj7yZwCe7AppWa3haBVCLC HfkbpmLW/MRaC2JOcJhiTwFVb25S4A7zx2utQn6y6BmLuXO4CEYu4jjh5BJ4LjanhVo3SFoC 8WGz3rLUn15jmoTATI6weQ3qENxw3+H0LNkmLpTFdVX4v5TSUEhONqUxO1xDpX3VwfLc82SY FKnWcm9RzA3QNUrxtYSYkU7BtOjyx3Z2yOsDLIT0bCGQNQ/9ufdxHH7KsJ5xjPbz6Q7lHEiQ 9BTLiutj6s5/gOVGo2N206ejuOhcbkW9C/L7maKi2SU+AlWVUt5V6PCQHYUa07bq8jizkfDV KO1T7IuKQIHxsmcbuNEb9bggX1bWPPiI8jFJX+tlne5HlCFyq7IJIrtfyAc2ivaIEwFiBwIu 22BKBI1CymmuW3TSjpjCRanZ07l96xjs36hZkAzyA6OYkJ70Ket4VgegvnYA/YSzLse/Skms ShxNFO8zdvMTcefrUxscLgaedd5qFFazXjdnwdmeJenNaZvglpYfghq+wv2yQ5fAZ5E19Mwr TUhyw82Yb6Y3VRbejbdxYr3JLDNMUH7/VaqarKQ113Dg/iM/aJazf0ktx3AtRynE0Mk9T0z0 NBI3X6V4JPiBxFUTI78Qk8ssRV2uueJMWEG+4rI2Cg0YuGPuTjY1odxbANE4hOpftMEdbiBC Be3CMoCQc6nNO0tnVGtKBMCJuFbsqAubIu9b/XT/qmtMa57mS6+y3xd6dV+21+C8iN6TMbDx NAY3/yI1xDBWjvh3x+6qs6ioYlffnkJG3anjy3tBYpffKp3KIUCFGmrKsux7t5lwYPxVm5R7 xiuC05VkNSxd0+qZkfmlRZVyVxRoXGjnn6gyCdoljgysqeF9CrD3OHrclwMIShWWGRyhEyqL ISp5zwDdG6vaQVh1B6s5EKhgrNeuLw6NG7LB0FBYynxKWhmFKq2rLuLJcBVutsutm1MXeKwb Er/KPa1qgYG0y7lA2pVxSwqPzCstJLjmhVmiWWbZH9tpXvdcMt0yF/R/tvZDfJW2zMHQmF/h 1y1ThC/NsSn+NySkb/IqaajS2+xX4YVfCX2jMuBuCa9+Wx2EEinhfng/7+vWQM+0CL9y5xrT XCR9ka6MtKtjv/rd7s+JhoNZhe08cdxF4Bgn5FlgZgR3SNfnZCJ5T8cln+1N9xH2KX4ZX5LR DgRwteT7hK2vS8rZn+P2Y/9UW2Qh8V7YNzvKGAfxyw45sZMIKyPqqFYkDt8uRy1oR+bMp0f1 n8NjOAj7nIXmbRDuwMwwCCUBLY6FlIeIDDhhx2Tqd2yse8EAQTnOaj13014k9e7CbiEqQwJQ 3f1dKApGipo59l+OlbBuJHqwrntY8KYLdcatxnP1gzFk/AQM5Up0PwDmStgP2v5+3wj0e8yy xJ0j9m2u42OKmMl+6zcYFYQNTToacYa/DfFhr0Yg9qbz4m0WJhtB30HUYDpQvShDD8J/a29Z 0DeS3tl8SbdQOOHVQaEoF9rtXfOD4ymOxT1bDECwNNuSQPcbE1TjQYIXSkry5swFwSk3svkI w9y4jEc4EK9qwMZk7g4cUmkFD6E9UHxM29nLfrXZABb5QxD+UrPZMmX7+YoWjpd4oXktwuVb GqSewVPC2gNHE2CHVHqeLe0tryiu6CVAPSzK/zWbPCAs+tbAr2LzI+h14Jg+R6HLYOSInRyB uZ910ZeFyMceYyRi3AURiobmjiYJc2SuRm58ytxhsuktun3VRLm/s2CB6YYYrANs1imxKyEM eCXniNwLz1Vg4gNyXH/w78axFcOiitqemrlAfEauCXKVq6Vhr5PAktRdXZoLMURpfFZvEEFK YvBh9jyzLI9kvMlFwIPSwn6gs/wLc0SfzPkbgOBVB3Nbe/XY2STm4n2ef/uEOcAyrUP8UTr6 HDCSheGXHzLliG1BUn1Yacc12fFbFoH49j1cxBmDXXvQYDRcQW1dtp+jDlw3KE5lnrRc2MQL F0eOwtMqLaU8C9V0MJkA2IH9HdqN+6Zg2Cc5ujcbIsKvOtiGWJ5m/8S9n0+z/E9ADhsfPVug 2OSq9dvpwrjieyT0n98VwIIrD9XhYWNtEEkOKPD95AGV2yWtB4K6GyRDVwNqb4HQpX3vLtMz 9HUiK/pADFP7Nfd+40XHI7JNM+XOWFnPBb0UDLZFwoKSze3OHqX3hYN1qHJsCTO/95j88Ckk YFrKPcTTFEvE/IGFklpVMcPJpt6RHJskLKWitIJ+WvrrBTVQ5YStZTGW/SORPT3fW/D3f8UP F1RmuK+dN1LZeiZkwR4Z1J3nZrHAR/VVNFJ+Wh6axMs5V5K6D54R3Ey3ETsbkWs5mUSHLi6h E1T6EM2bOIz+TPr+1pyKEDNoX56k0Asl9Dshza5eyW3Mbu9TYhNTSf4qgJiV/GzCxYwdgC0k UF+YX3cQKlNirJ7aW1xoAnRpp5GH7hXVutZfBIAzOrRavk1mwc5yG3v1QpM4u3LDoFnnQ0hf Mu3rn5O7AlkacY8Oa3aIKcahkgVnK+FuTWkk/wg2AJLbVhY63ucIWRb3S5AfqljPSej+fZgr BCPiycWMnZZTOIk+7pjvgY0P+DKp8oP+7VYbF2tOvyWNOWUt3WSzKZgo3s221wNnk8D9qMwz NsuY0OPEU0j0enIf/zsHcHZbxxJYtpb7z7ecTvc6Y3w
Ironport-sdr: 652ac2e6_vilX37aTm/RXR0RnQOfmN8z04pqUC7mQ8cMjCczdCdeZ2/o /H2yLaqtChMLqzJoDBTGK2fpCT4OITOsnq8V/LA==

Registration is open for ACL2-2023.

*** SECOND CALL FOR PARTICIPATION ***

ACL2-2023

18th International Workshop on the ACL2 Theorem Prover and Its
Applications

November 13-14, 2023, Austin, Texas, USA and also online

http://www.cs.utexas.edu/users/moore/acl2/workshop-2023/index.html

The 2023 ACL2 Workshop will be held in Austin, Texas, USA and online.
We invite users of ACL2, users of other theorem provers, and persons
interested in the applications of theorem proving technology to
attend. Keynote talks will be given by:

Jim Grundy, Amazon Web Services
Eric Smith, Kestrel Institute

REGISTRATION

Registration details, including fees ($0 to $140) and sign-up may be found at:

https://acl2.regfox.com/acl2-workshop-2023

Note that the discounted fees for early registration end after
October 31.

AIMS AND SCOPE (quoting from
https://www.cs.utexas.edu/users/moore/acl2/workshop-2023/index.html#scope):

The ACL2 Workshop series is the major technical forum for users of the
ACL2 theorem proving system to present research related to the ACL2
theorem prover and its applications. ACL2 is an industrial-strength
automated reasoning system, the latest in the Boyer-Moore family of
theorem provers. The 2005 ACM Software System Award was awarded to
Boyer, Kaufmann, and Moore for their work in ACL2 and the other
theorem provers in the Boyer-Moore family.

ACL2-2023 is planned to be a two-day workshop to be held in Austin,
Texas, USA, on November 13-14, 2023. The workshop is planned to be
held in-person on the University of Texas at Austin campus. In
addition to in-person participation, the workshop will support online
participation for all talks and presentations. The workshop will be
the 18th in the series of ACL2 workshops, which occur approximately
every 18 months. The workshop will feature technical papers as well as
rump sessions that discuss ongoing research.

FOR MORE INFORMATION:

See the website
https://www.cs.utexas.edu/users/moore/acl2/workshop-2023/index.html
for further information including accepted papers, organization,
venue, and lodging.

[Coq-Club] ACL2-2023 Second Call for Participation, Matt Kaufmann, 10/14/2023