coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Orestis Melkonian <melkon.or AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Agda Implementors' Meeting XXXI - Edinburgh, 10-16 November 2022
- Date: Tue, 26 Jul 2022 19:14:41 +0300
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=melkon.or AT gmail.com; spf=Pass smtp.mailfrom=melkon.or AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f45.google.com
- Ironport-data: A9a23:IY5zfqwhJP/enIGqz0J6t+cAwCrEfRIJ4+MujC+fZmUNrF6WrkUFn TMXUWuAPP6Damukc910aty09k8P6paEmIJmQAtvqlhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrVRbrJA24DjWVvS4 42q+qUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPh3l 95SvqyXaj1qFa2QlMg5Qh5HPnlHaPguFL/veRBTsOSWxkzCNnbgmrBgUBxwMoof9eJ6R2pJ8 JT0KhhXNkHF17/wmurrDLUx7iggBJGD0Ic3v3xkzjbfS/E8aZ/GSqTOo9Rf2V/cg+gURa+PP ZJDMlKDajzrPx1vPGwGEahukc23pkD7eWZhsUO88P9fD2/7lVQtitABKuH9cduTAM5Rg0ywv XPD522/AxcANdXZxyDtz563rurGnCe+VY5LUbPkq7hlh1qcwmFVAxoTPbemnRWnokjhUM1UG 2s3wGkFrfQ+2Gi6ScbQByTt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4othpOIxOWCgeFWxC6 7OZoz/6LWcw7+DNGBpx4p/R/GziY3FERYMXTXZcFVNt3jX1nG0kYvvyojtLFae0ipj4FWi1z WzX6ic5gLoXgIgA0KDTEbH7b9CE9sWhou0dvF2/soeZAuVROtXNi2uAtwSz0Bq4BNzFJmRtR VBd8yRk0MgADIuWiAuGS/gXEbei6p6taWOB0QEwRMl7qWr1oxZPmLy8BhkudC+F1e5UKVfUj LP75Gu9GbcIYST2PfctC25PI516kvi+fTgaahwkRoMWPsIZmP6v8yZpakqdt10BY2B9+ZzTz ayzKJ72ZV5DUfoP5GPvG481jOF2rghjmju7bc2ql3yPjOvFDFbIGOdtGAXUMogRsvjfyC2Lq IY3Cid/408AOAEISnKHr9B7wJFjBSRTOK0aXOQOKrPTeFI2RDF9YxITqJt4E7FYc21uvr+g1 hmAtoVwkTITXFXLdleHbG5NcrTqUcotpH43J31+MlOh2nxlaoGqtf9Ne5wydLgh1epi0f8kF 6lfK5vcWqxCGmbd5jAQTZjht4g9JhmmgAS5OSD6MjUyephXQRPEp43/dQz1+ShSVSe67JNso 7Cp2g7Bb4AEQgBuUJTfZP61ngG+uHEcnKR5WE6Reotff0Dl8Y5LLS3tj69vc5tcd0mbnjbDj lSYGxYVo+XJsrQZytiRiPDWtZqtHst/AlFeQDvW4LOwAi/QoTiuzIpGZ+CXJGyPWW7x/pKiU uVb1fTLNvMKwQRRuI1mHrc3lK8z6oe9p7JeyQg4TnzHY07xUeFlK3iCmMRD7+hDmuIftgyxV UaCvNJdPOzRas/iFVcQIisjb/iCha5IwGiMtaxtLRWo/jJz8ZqGTV5WY0uGhhtbIeYnK4gi2 +og5JMb5lDtkBYsKdra3ClY+37WdS4FWqQj85wWWcrl1ldtxVZFbpjRTCTx5cjXOdlLN0ArJ B6ShbbD1+sAnBucKyJrGCifx/dZiLQPpAtOkA0IKWOPl4eXnfQwxhBQrWk6Qwk9Is+rCA6v1 rWH9nGZJJliOx9tjclHGm2gQkRPWEDf9Uv2xF8E0mbeSiFEk4ALwHIVYY6wEIIxqgqwvQS3O JmXzW/kVXDhe8SZMu4aRxt+s/K6JTBu3lSqpS1kdvhp27E1ZDPkhumlYm9gR94Lxy8urBWvm NSGN9qcpUE22eD8bkH750SnOWwsdS25
- Ironport-hdrordr: A9a23:BQs1Ma3f/mzhOf25PE0ezwqjBIUkLtp133Aq2lEZdPUnSL3+qy nIpoVg6faUskdrZJhEo7q90ca7MBHhHPJOkPAs1NSZLWzbUQmTXeJfBOLZqlWKexEWntQ96U 4KSdkHNDSfNykdsS+32njdLz/i+rW6GWKT6Ns2A00DceiiUc9d0zs=
- Ironport-phdr: A9a23:L4nh3xIEnDngi22SxNmcuHdsWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFvrM31QeCDNqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7ye6/94fNbwlVmDaxbrd/I RerpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+V rxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4 aV2Rx/ykCoJNDA3/27ZhcJujKxVvQ6uqRNkzo7IY4yYLuZycr/TcN4YQ2dKQ8ZfVzZGAoO5d 4YBFvABMvhDr4nhplsOtga1Cw6yC+PryT9IgXn23awg3OQnDArL2wkgEMwKsHTXq9X1Mr0eU eevzKTTwjXDaulZ2Tb56ITSbh8hpvSMUKt2fMHMxkYhCxnLgU+MqYz5ITyVzOINvnCZ4uZ+W uyij2AppQ9srjWz2MoihIbHi40Rx13Y+ih13Jg5K9OmREN4Y9OoDppdui+HO4drTM0sQ2Nlt SI4x7MIv5OwYSYEyJMixxHFavyHdZCF7Q7jVOmLJTd4gWxqeKikhxqo6kiv1OvxXdS33lZSt idJjMXAu3QX2xHQ6sWLUOVx8lui1DqV2A3e6vlILV03mKfYMZIszaQ8moQPvUjfBCP7l1v6g amLfUs+4Oeo8f7oYrD+q5+cKYB0jgb+P7wrmsOlAOQ4NhECUHaG9uihzbHj80L0TbVQgv05l anZt5/aJcAFqaKjHwBV1YMj5w6+DzegztsYgWEKIExZdB+DlYTkOFHDLOrmAfujgFmgijhmy vDeMr3kGJrNL3zDkLn7fbZ67k5R0A8zws5b55JXDbEBJuj/WkjrtNHDAR85Nha7w+fjCNlny oweXmePDrefMKzJqVCI/P4gI/GQZI8JvzbwM+Up6+b0jXAlgV8dYbWp3ZwPZX+kGfRmOlyVb mbogtccCmgHpRE+TezviF2aSzFffXeyX6Qm5jE6Eo2qF4nDRpr+yICGiSy8B9hdYn1MIlGKC 3bhMYueCNkWbyfHBdVsiSAFTvCERosi0hevvQmyn79qKunT/Gsfr7rs0dF046vYkhRkpm88N NiUz2zYFzI8pWgPXTJjhMiXwGR4w1aHiu1jhuBAUMdU/7VPWxs7MpjVy6p7DcrzU0TPZITBU 06oF/OhBzx5Vdct25kWeU8oHtimjRfFmS2wK7AQnr2PQpcz9/GUxGD/cv500G2Oz6w9lx8jS 8pLO3ehg/t6+gzQAIiPlF+xmKOjdKBa1ynIpy+Y1WTbmkZeXUZrVLndG3ASYkyDtdPi+kbLV KOjE5wiOwpFjMOOc+5ENoCvglJBS/Puft/ZZgpdgk+WAhCFjvOJZYvuICAG2TnFTVMDi0YV9 GqHMg43AmGgpXjfBXpgDwCnZUSk6uR4pH6hKy18hwiXc01s0aa08R8JlLSdTf0UxLcNpCYmr X19Al+829vcD9fIqRBmee1QZtY04VEP0my81UQ1O5GkLKdkwFkEWwtytkLqkR5wD8QIkMQnq m8r0BsnMbiRgxtKczKV24y1O6WCcDGjukDyLfSOiheCjYXzmO9H8vkzplT9sRv8E0Mj9y4iy NxJyz6H4Y2MCgMOUJX3W0Jx9h5gpricbDNuguGcnXBqL6SwtSfPntwzA+5wgBOte9RYNuWDD if9FsQbA46lL+lgyD3LJloUeftf8qI5JZbscvaC26mteuF6tD2jhGVDpot61wjfvzo5QenO0 ZEfxvie1QbSTDbwgmCqtcXvkJxFbzUfdoam4RDtH5UZJqh7fIJQTHyrP9Xy3dJmwZjkR39f8 lenQVIAws6gPxSIPRTx2ghZ1EJfpnLC+2PwyjFwkDYv6K2F9CPLyuXmMhEAPyZHSXJjglHlP YWvx4pCDQ74Mk5zzEvjuRuyzrMTvKllKmjPXUpEGkq+Z3pvVKe9rPvKYsJC7o8prTQCVe29Z V6ATbuu6xAe0i7lAy5f3GVhL2Ds6si/xUQqzj7AfxMR5DLDdMp9xAnS/onZTP9VhX8dQTVgz CLQHh66NsWo+tOdk9HCtPq/XiSvTM42E2GjwIWeuS+8/WAvDwe4mqX5n9DjEg88lyjh/9ZvX CTM6h37Z8O4ssbyefIiZURuCFLmvoB/F4V9lY12g4s41n0Th5HT9n0C2zSWU50Tyef1a3wDQ iQOytje7V3+2UFtGXmOwprwSnSXxsYyL8n/eG4d3TgxqtxbEKrBpqIRhjN7+xDryGCZKeg4h DoWzuEirWIXk/1c8hR41T2TW/gTBRUKZnGqzkXQqYri8+MPIzzzObmoiBggwZb7V+rE+18EH i6+I8ZHf2c4790jYgySliSrsMe8PoGXN4pbtwXIwUmeybIJedRhzrxSwnA/cWPl4S96kahi0 Vo3jMv85M/eewAPtOq4GkIKaWGzPplOvGmr1eEHwI6Xx9z9R80xXGxUA924C6rvSmtatOy7Z V/RS3tl+yvdQfyHWlbBjSUu53PXT8LxbyDRdCRflI8yAkHafRMXgRhIDm9jwNhkRkbzlZanK AAgt3gQ/gKq8EISjLgzZl+kCCGH4175D1V8AI6WKB4chu1bz2HSN8HWrud6HiUDu4aksBTIM WuDIQJBEWAOXEWAQVHlJLino9faoaCeAaKlIv3CbK/ry6QWXuqUxZ+pzopt/iqdfsSJMH54C vQn201FFXlnEsXdkj8LRmQZjSXIJ8KcoR69/GVwoKXduLzzXxnz4IKUF7ZIGdBm+hTzjKvac uDM2WB2LjFX0p5KznjNifAe0FMUlyByZmytHLAH5kuvBOrbnq5aCQJeajsmbpMZqfJhmFMVa YiH14CQtPYwlPM+BlZbWEa0n8ioYZdPOGShLBbcA17NMr2aJDrNysWxYKWmSLQWgv8H0n/48 TudDULnOSyO0jfzUBX6e+RBiCKcOlpZoqmydx9sDS7oS9esOXjZeJdnyCY7x7E5nCaALWkHL T11aF9AtJWV5CJcx/hzQilPsicjIu6DlCKUqeLfL9xF1JkjSjQxnOVc7nMgzrJT5ywRX/15l hzZqdt2qk2nmO2CotKCeBVLozdPwomMuBc6UU043pxJWHKB8R5UqGvMVlIFoNxqDtCpsKdVm ICnfE3bJzJL8taS9swZVZG8FQ==
- Ironport-sdr: pcj6pEpmESrIGfQayQNiA0URZUiOnmhhvlpIqkqsljI6s/pW7OlUJH6CuHr1mibaaWRgUEgJ0c x+0yRL6aWj/Efpn+WGN/U/zUVK7DhcP4j7Hu1kYXzXm0RsjukbSVk3laeUEWrj2d11G0A8/v9H 3cA6IGifQ/oFhasQVpL1Uzqoi5ZjZh55ymsDPDUJtynHRUz8Qnpma/cfEcdmWo77hGWk4HbFlU PzzIjSlmXuhw+SCimlZK8Mwuj04eSB4sjo9awgRcPE3xgAWerBSSyHjg84Ld17XvakszvYiB0y 3ZO5M4S4L1BMe7Ug8JPiytz9
---------------------------------------------------------------
Agda Implementors' Meeting XXXI
Call for participation
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXXI
---------------------------------------------------------------
The 31st Agda Implementors' Meeting will take place in Edinburgh, Scotland from Thursday 10 November 2022 to Wednesday 16 November 2022.
Note that AIMXXXI was initially planned for 2019 but got postponed due to COVID-19, whilst we had several online meetings XXXII-XXXV.
The meeting will consist of:
* Presentations concerning theory, implementation, and use cases of Agda and other Agda-like languages.
* Discussions around issues related to the Agda language.
* Plenty of time to work in, on, under or around Agda, in collaboration with other participants.
* A full day dedicated to the EuroProofNet COST action, including talks and discussions on translating libraries and proofs between Agda and other proof assistants. Please direct enquiries about that to Jesper Cockx <Jesper AT sikanda.be>.
To register for AIM XXXI, please fill out the form below and send it to Orestis Melkonian by email <orestis.melkonian AT ed.ac.uk>, or simply edit the AIMXXI wiki page yourself.
> ---------------------------------------------------------------
> Registration form for Agda Implementors' Meeting XXXI
>
> Name:
>
> Title and optionally abstract (if you want to give a talk or lead a discussion):
>
> Suggestions for code sprints (optional):
>
> Dietary restrictions:
>
> Additional comments:
>
> ---------------------------------------------------------------
More information is available at
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXXI
Please spread the word about this meeting.
Best regards,
Orestis
- [Coq-Club] Agda Implementors' Meeting XXXI - Edinburgh, 10-16 November 2022, Orestis Melkonian, 07/26/2022
Archive powered by MHonArc 2.6.19+.