coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 39th Agda Implementor's Meeting (AIM XXXIX) 25-30 Nov 2024 in Gothenburg

From: Andreas Abel <abela AT chalmers.se>
To: coq-club AT inria.fr
Subject: [Coq-Club] 39th Agda Implementor's Meeting (AIM XXXIX) 25-30 Nov 2024 in Gothenburg
Date: Fri, 20 Sep 2024 19:16:35 +0200
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cse.gu.se; dmarc=pass action=none header.from=chalmers.se; dkim=pass header.d=chalmers.se; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=D4h/7UwtRIcer03jLVZkb1xBJYX/A+k92Csb+MpZoWI=; b=W2OlcWsOPgf8yn1KzTsRx2S1tM+iDBvlmKsPjbQorY1L7xrubV+31sNftNy4YR3L9L3BombT2xZ4sW87HoZQk0Rt8xsyPK7hpUWuMmzBE9QPpB18aEa3islfVTZ9rGdg30tmgpm0rrw6PNdPMbNmBBVITndlxLRaLr//PkUI519MF/5funf8rMDThTmkUe7urRLEKB3WuryK0OB12GiCCLiwCmX5o5VOCk2RrebktP2s4QBz9h8JYtop7VciGwx9Th3OfveT8wd0MFqtOKXTECK3zRtCBxMn4GAQq8oQta8mmpWS8sYjecxL38i7qTI9BDarD63QpdGUsjtF+ylsog==
Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=ke5tU6FtAdHe+7eRZqqKRgDBZYaw5nV5uGD9NbiXt6pm0X+go13c7/R2KI6hZ9k4Me4ToDVzPlPB1xINnbtFYuJC6o/213z/aGPsy0iPp3UXXB9Cc1SOoLJs25QnF1uIRTOoUHfvlmso41y3xVYLz8dFh1xkWrLoWevQOPXIOUUTqXatIlxnRWercmNpQq9D753Dgf/IUS1m4jF0phsvh4rVS4zXEbhihVRuHLSwvEPRty91I2U/ikj0jm6Tr9nPjY5cB4FnjThdI6A17lVraiTX9MVFgF9ll9pVGZhYhdjlLS4lLHP5gGeEzvCPk+sekO0Cz/owbJZHHEqBi8g6mQ==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abela AT chalmers.se; spf=Pass smtp.mailfrom=andreas.abel AT cse.gu.se; spf=Pass smtp.helo=postmaster AT GVZP280CU001.outbound.protection.outlook.com
Ironport-data: A9a23:BXXKiqmxYwnYApDWxap9XKjo5gwdJ0RdPkR7XQ2eYbSJt1+Wr1Gzt xIXDWnTPf7YYmKhfI8iO9nkpB5QuZKHyNRjGgs+qH0xRltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayazp8B56r8ks14Kyj4mtA5zTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1HM19sYZIm3tonDE5e3 OcldjA9MEqc0rfeLLKTEoGAh+wMEvvTZtNHkUw4lWifCus6S5feRamM/cVfwDo7msFJG7DZe tYdbj1sKh/HZnWjOH9KUtRnxL7u1iC5KmQIwL6WjfJfD2z7xQp9yrXkK5zccNGObc5OkwCXu yTd8gwVBzlDZIDFmGDZqiLEaunnxXz9dpkNFL+B36B330Oh7GsIBRYyfA7uyRW+ogvkMz5FE GQf/TNrpqwv/mSwX9zlVlu5pmSFt1gSQbJt//YS7QiMzu/P/AuVC24PQzhdctUivd0xQ2Vzj gXQxoq5QztyrLeSVHSRsK+Oqi+/MjQUKmlEYjIYSQwC4J/op4RbYg/zc+uP2ZWd1rXdcQwcC RjRxMSTr+x7YRIjv0l6wbzGv95ojrf3fDZvtl38Yzr9t0V+eZKvYJGu5R7D9/FcIY2FT16H+ n8Zh8yZ6+NIBpaI/MBIaPtYB6mnvp5pLxWF6WOD3bF4n9hux5JnVYtL7XdxOQFyP67ovBf3N VTLt1o5CIB7ZROXgGweX251I88qxKzlGM7+EOvZBjaLjl6dayfflBxTiYWsM6wBXaTifWzT+ XtWTCp0MUsnNA==
Ironport-hdrordr: A9a23:mEbrGK4ifV5CnQM6JAPXwTKBI+orL9Y04lQ7vn2ZFiY5TiXIra qTdaogviMc6Ax/ZJhSo6HnBEDmewKlyXcV2/hpAV7GZmXbUQSTXeJfBOfZsljd8k7Fh5NgPM VbE5SWYeeYZTYasS+T2njDLz9K+qjizEnHv5a4854gd3AJV0k2hD0JcTpzX3cGMTVuNN4cLt 6x98BHrz2vdTA+adm6PGAMW6zmq8fQnJzrTBYaD1p/gTP++g+A2frfKVy1zx0eWzRAzfML9n XEqRXw4uGGv+ugwhHR+mfP59B9mcfnyPFEGMuQ4/JlXgnEu0KNXsBMSreCtDc6rKWG70srqs DFp1MaM8F6+xrqDxGIiCqo/zOl/Ccl6nfkx1Pdq2Dku9bFSDUzDNcErZ5FczPCgnBQ9+1U4e Zu5Sa0ppBXBRTPkGDW/N7TTSxnkUKyvD4LjfMTtXpCSoETAYUh5bD3xHklXavoIRiKpLzOSI JVfY7hDbdtABqnhknizyNSKIfGZAV8Iv+EKnJyy/B9nQIm3UyR9HFouvD3rk1wiK7VdKM0mN gsEp4Y542mHfVmH56VQt1xN/eKNg==
Ironport-phdr: A9a23:u8wvcB3LkdvZdIEhsmDOvAwyDhhOgF0UFjAc5pdvsb9SaKPrp82kY BeHo6w81xSQBN2TwskHotSVmpijY1BI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDebRlEiCCgbb52I hi6ohjdutQKjYB/Nqs/1xzFr2dHdOhR2W5mP1WfkQri6Myt5pBj6SNQu/wg985ET6r3erkzQ KJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/8 6dmTQLjhSkbOzIl9mzcl8p9h79Zrh28vRxy243abo+bO/R+Y63TY88VS2VOUctKSyxMAJmxY 5cTA+YfP+tVqZT2qVsUrRu5AAmhHP/iyjlViX/sw6I1yf8hGhza0QM7Ad0OtGnfodLvO6gJT ++1yLPHwC7fYPNWwzj97I3IfQ47ofGXR75watTexFApGgjYgVqetZbrMCmJ1uQRrWeb9exgW PqshmAnqw99vCWjy9oshIXUgo8Z10zJ+CF5zospK9O1VFN2bcK6HJZeqi2UN5d7TMMtTW12p Ss0yqMKtJ61cSQWzpks2hDRa/uCc4eS4xLjUv6cLit4hH1/fLK/ggi98VK7yuHmTcm7zlBHp TdGnNnUrn0A1wLf5tKaRvdh40utwzWC2x3J5u1ZPEw5lrLXJ4Agz7IsmJcetFnPEjPsl0j3i aKaa0Up9vSt5unpbbjro5qRO5Jphgz4L68jhMi/AfkjMggSQWeb4/my1Lzi/ELnWLhGkvs7m bTDvp/AP8QUvKu5DhdV0ok97xa/CC+r3tUXknYENlxJZhGKg5T3Nl7APPz0Eeqzj06rkDd22 /DJJbrhAojLLnfeirvhZax960lAyAUt0d9f+5NUCrYHIP7pXU/xqcDYDhs+MwyzwObrEsly1 oQbWW6XA6+ZNr3dsUOQ6+8vPeWAfpIZtCrgJ/Q/5PPikGU1lUIAcaSqxZcXbWq3HvViI0WXe 3rshdIBHH8QsQo4UePqkkONXiRIZ3qoRa0z/S80CIa9AIjfXYCinqaN3CimHpFMfWBJFEiAE XHzeIqcQfcDdDqSItN9kjwDTbWtVpct1Quyuw/i17pnMu3U9zUEupLkzdh5/vHclRUv9TNvF MmdyGGMT2RsnmwSXTM23aZ/oVZ8yliZy6R4jeZYRpRv4KZCVR5/PprBxcR7DcrzU0TPZISnU lGjF/ygDSs8R8l56tUDZw4pEt+vihnr1CqjB7oYjafNH5FiofGU5GT4O8sokyWO76ImlVRzG qOnVEWjj697rU3IApLR1l+enOCsfLgd2yjE8CGCy3CPtQdWSl04Sr3LCFYYYEaettHl/gXaV bb7AL4qNgJpws6LLq5HcMavllgVDOz7NoHmanmq03y1GQ7Ow7qNaITwfGBI1SPREkUNiEYa9 3uCHQMlC2GuviTFAW8mDkrhNnvl6vI2s3anVgk0wgWNOlVmzKaw8wUJiOa0ZM0h5uhU4Awc8 20tWlGgw9jRFtyM4RJ7e7lRas8851EB0n/Fswt6PdqrKKUKakc2VQNxsguu0hx2Dt8Fis02t DYwywE0L6uE0VRHfjfe3JbqO7SRJHOgtBaoI7Xb3F3TyrP0su8G9eg4plP/vQqoCltq8nNp1 MNQ2med4ZOCBRQbUJb4WEI6vxZgoLSSbi447oLSnXpiVMv8+jbI1tYgLOAlwxKlcs1EdriJV UfzH8AcG8myObkygVH6JhkAPe1U6Os1J5b7Lb3fgPftbL8mxWv23gElqMhn30mB9jRxULvN1 pcBmbSD2xefEi37hxGnu9z2noZNYXcTGHC+wG7qHt00BOU6cIAVBGOpO8DyyM95gsunUnhU7 lOqHBUP0sKtURGJYhrywEtL2A5ExB7v0Tv91DFynzwz++CW1iHKyszpdBMDP2NRXy95gB2/a ZjxhNccUk+yagEvnxbw/kf2yZ9Qo6FnJnXSS0NFF8TvB1lrSbD49r+LYsoVrYgtrT0SSuO3J 1aTVr/6pRIelSLlBWpXgj4hJXmmvZDwnhoyj2z4Tj47pXzVY8x53lHW7tHYbfVK03wJWW9jh HHbC0O9MN+g4diP38qZ9LnmDiTxD9sKKHmjxJjIrCah4Gx2HRCz+pL70sbqFwQ3y26z1tVnU znJsAepZ4Dq06qgNuc0NkJsBVL69497AtQjyM1p3MhWiSFc38zFrh9l2S/pPN5W2Lzzdi8IT D8PmZvO5RT9nVdkJTSPzp74UXOUxo1gYcO7ayUYwHFYjYgCBaGK4bhDhSYwrEC/qFebaP5xh DoU0r0n4nMeq+oStUwi02OGD/pBeCsQdTypjBmO492k+e9eYmq1fLGrkkN0kNSJB6qP5A5BH m30MMRHf2c4/oB0N1TC12f244fvdYzLbN4dgRaTlg/Jk+lfLJ9i3upPnydsPnjx+GE00+Nux wI7xom05cLUTgcltLL8GBNTMSf5It8e6i24x7gLhd6YhsiuBskzRm1NDcGuFbTwV2tP/fX/a 1TSSHtl8ijdQfyHWlbBjSUu53PXT8L2bTfOfCFflZM6A0DAbE1H3FJJBnNjxsR/Tkbyg5W/O EZhumJMvBih8kAKkqQwcECgNwWX7AawNmVtEMTZcEUQtkcaoB6Kec2GsLApFnkBrMT49V6Dd jTDNVYPUTFsOATMBki9bOOnvYCSqrHBVOTid6CcM/LS+KRfT6nan5v3i9k/pm/eOJnXZSsyV 6VjiBgEACkceYyRmi1RGXYez3ufNpfC9hngonYlpZjnqKa5H1+2rYqXVekIOI02qUnv2PWNa 7bL1ighcW4KhNRRnzeNwbwbljb+kglWfiK2WfQFvC/JFufLn7NPSgQcYGV1PddJ6KQ12k9MP 9Tag5X7zOwwgvkwAlZDHVvv/6PhLdQNOH24PUjbCVyjG4q0HWebm+rKOfvlD7pNkO9Tqhu8/ y6BFFPuNSiCkD+vUA2zNeZLj2eQOxk72sn1fht2CGflRc7rcVXmapku1WRwkeRy3yqafWcHe SBxaUZMsqGd4WtDj/NzFnYApntpIO+YmjqIuunVLpFF1JkjSi9wlu9c/DE70+4ItmcdHKUzy HKU94c+8DTE2qGVxzFqUQRDsGNOjYOP5wB5PLnBs4NHUjDC9Q4M6mOZD1ILocFkA5vhofM1q JCHmaTtJTNF69+R89EbAp2eIcSLKncoKlzgEjPQJAAeQHikKCfEigYO9ZPavm3QtZU8ppX2z dAWTaRHUVUuCv4AImtbLuRYcM9cY2t8yPickdIC4me4oF/JXsJGs5vbV/WUR/LyNDKeiroCb BwNi+CdT8xbJsjw3EpsbUN/lYLBFh/LXNxDlSZmaxc9vERH9HUtBn12wU/ubRmhpWMCDfPh1 ABjkRNwOK5+kVWkq0dyPFfBozE81VU8icmwyy7Eayb/de+xRd0EV3Ky5hJ3atWjBF8oJQyqw R44bHGdH+0X1/04Mjk17W2U8ZpXRawBF+sdOEdWnbfPIKx1mVVE9nf6nwkevbGDUd0601J0O Z+08yAdgUQ6NIVzfeqIY/MWqzoYzqOW4n3xjrx3nFBYfwBVtzrNMC8Q5h5SP+F/dXPxp75it VTayWkEJDhpNbJio+o0pBk0Y73Slnu5gbAfchvjZavDfuuYozaSz8fQGwFpjxpamRUdpuomi Z97IRjTChlKrvPZFgxXZ5DLcVgHNpMLpnaPJX3cur2VmcAneNjkXuHwE73Uvf5N0Bv9RVQnQ 9xXvMpZRsH+ggaFd4+iJboBg33FASzgJFyBCflTY1SQnWVfyyle5LBJ77EHdmk2PD0laGOw+ 6rdoRIsjLybRtAqb3wGX4wCcHUrRMm9nC0ftHNFXmDfOg0xwxOPqTDh4D/dXmCUUg==
Ironport-sdr: 66edae02_ocmWJc8PgB/SHcW5s4ehguIPS/dYXdh2YKkJJnM9gkGsLBZ nbVCBSToJ/sWJCfLqyBiiATk0IWbAaruJsLq1Ng==

----------------------------------------------------------------------

Agda Implementors' Meeting XXXIX

Call for participation

https://wiki.portal.chalmers.se/agda/Main/AIMXXXIX

----------------------------------------------------------------------

The 39th Agda Implementors' Meeting will take place in Gothenburg, Sweden, from Monday 25th to Saturday 30th November 2024.

(This is our 20th anniversary of Agda meetings, the first took place in Fall 2004 in Gothenburg.)

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 special session dedicated to the 20th anniversary of AIM.

Attendance is free of charge, but a registration is warranted until 31st October 2024 (soft deadline). For information how to register check out

https://wiki.portal.chalmers.se/agda/Main/AIMXXXIX

Looking forward to seeing you in there!

Andreas (on behalf of the AIM XXXIX organizing committee)

--
Andreas Abel <>< Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www.cse.chalmers.se/~abela/

[Coq-Club] 39th Agda Implementor's Meeting (AIM XXXIX) 25-30 Nov 2024 in Gothenburg, Andreas Abel, 09/20/2024