coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th

From: Yannick Forster <yannick AT yforster.de>
To: coq+announcements AT discoursemail.com, coq-club AT inria.fr
Subject: Re: [Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th
Date: Thu, 21 Dec 2023 15:56:14 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yannick AT yforster.de; spf=Pass smtp.mailfrom=yannick AT yforster.de; spf=Pass smtp.helo=postmaster AT himalia.uberspace.de
Ironport-data: A9a23:DG3/pqh2QKJVjmD8Y7eb3y8/X161bxUKZh0ujC45NGQN5FlHY01je htvWGmGPP6MZGuhctxybdnlph4G65KGydNgGlBlqSg1EyNjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpIg06/gEk35q+r4mlB5gVWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGLH8wFI89p+NNP05hq twfGm02bQGHvrfjqF67YrEEasULLMjuNYceszd9xzzDFu4vSp2FT6iiCd1whWdtwJoQW6+DO YxAM2QHgBfoO3WjPn8GAZQ4neyrrmjxdCdDtF+P46Y6i4TW5FUti+Wyb4KKJbRmQ+1zmkyHr 0/2zl7YBzMGd9+E+TSL6XeF07qncSTTHdh6+KeD3vVtmRiYwnEZIAYHUEOy5/i/kE+3HdxFQ 3H44QIurK078E2iCMT3UgejuHePs1gQVrK8DtEH1e1E8YKMiy7xO4TOZmQdADD/nJ5oH24Zx RWSksn3BDdilrSQRDjPvv2XtD6+c2xdZ2MLeSZOH0NP7sjBsbMDqEvFbu9iN6qp0fzzOzX7m A6RoAYE2r48sM8s1oeAx27hvQ6CnJbyYzAQ2hT2RUOgtwNwW56kbden6H/d9vdxE7yaRVig4 lkBm9CU084VBK6giSCyYuEGGpe21smjNBnZu1pOHoYgxRup6XWMbYBd2xAgBUZLY+IvWy7lX 1/XgixVvKRsBXqNabRmRb6xB+AB77nSJf68Wt/6NtNxM4VMLimZ9yRQVGus9mHKknl0t5ogO J2eIP2ePVxDBYtJlDOJFvogi5k1zSUDxETWd5Dx7zKj9ZG8PHe1a7M0AGGiX9ADzpGvgVvqq o5EFs6w1R9gfvX0YXDX/a4tPFk6FyUHKq6smfNHVNyoA1RAI34gOc/z0Ll6Wo1CnoZprMnq0 Ey5eHdlzAvYuSWaBySMMmtueZH+b6ZZ9HgbBxEhDXys+nokYLus0pshSosKTeEn2dFnnNFJT KgjWsSfA/5wZCzN1BYDYLLc8oFzVhSZqjifHiiiYTUATYBrQSqRyO/FYznAySgqJQi0vPsYv LeP+F76Q50CZgI6F+fQSqul4G2QtEgnutBZfhX3e4FIWUPO9INKFXTAvsUvKZtRFSSZlyqo6 QmGJDw5+8/PmtYR2/vUj/mmq4yJLbNPLnBCFTOG0YfsZDjoxUv984puS+3SQCv8Ulnz86CcZ el46fHwHfkEvVRSubpHDLdZ4vMi1uTruoNl4FxoLFfTY3SvL4FQEH2M8M1Ml69Kn5tymw+9X GCR8dh7Z5SNHu7YE2AqGQl0VdTbiMkomQTT488lf2T8xit8p4ScXWtoYhKjtS16LZlOCr0D/ 9sPgsAs1lGAukIYCere1iFw3EaQH0MESJQi5807Ape0qw8FyWNiQJ37Cw2r0pTeet4XCE0hI 2KXtpHjnJVZ/FLJKFAoJEjO3M1cpJUAgw9Lx1k8PGa0msLJq/s0/R9J+wQMUQVeyytY39JJO mREM1N/IYOM9WxKgPdvcn+NGQYbIjGk4W30lkU0kVPGQ3mSVmDiKHM3PcCP9hs790NeZj1qw 6GK+l36UDrFfNDD4QVqYBRL88fcdN1W8hHOvOuFHM7fRpkzXmfDs5+UPGENr0PqPNM1iEj5v tJVxedXa5DgFCsusqY+Wpi717MRdUi+H1Z8Y8pdpYEHIWKNXwuJ+2m+GxjkMIcFbfnH6lSxB MFSN9pCHUb2njqHqjcAQ7UAOflolfou/8APYa7vOXVAibaEsz51q9jFw0ASXoPwrwlGyq7R6 789dg5u1kSQhH5dn27E6tRON3CjedAPaUvw0YhZNc0XQokbvrgEnV4ai9OJU7e9aWOLPC54e CvSaajM1PBv08JgkuMA141dUh6sJ4qbuPugqWiOXhcnUT8LGdbAsBkOtlT9eQhbVVfUtxKbi pzV2OPKMIj5UHranowXd1Rt10WE2ClqYNdqDw==
Ironport-hdrordr: A9a23:26jxraiY75LV6w4cdDI1qD4JJXBQXhwji2hC6mlwRA09TyX5ra qTdYcgpHzJYVEqKQgdcLG7Sc+9qBbnhONICOYqUotKMDOW2ldAabsSircKoAePJ8SdzIJgPM 5bGsAUZeEYT2IK6foSizPZLz9P+qjjzEnlv4bj5kYodhtyY6VsqyxwEW+gYzVLbTgDPoAhHJ 6QovFKvjy6ZB0sH7+GL0hAZPLbr9nH0KjtZwULbiRXkjWzsQ==
Ironport-phdr: A9a23:NO6/cRTCBi4QHUQ3q4GFcR7nKdpsot+WAWYlg6HPa5pwe6iut67vI FbYra00ygOTDcOBsq8P17GempujcFJDyK7CikxKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxB sVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexf7B/I A+ooQnMtsQajoRvJ6gswRbVv3VEfPhbymxvKV+PhRjw4du+8oB++CpKofIh8MBAUaT+f6smS LFTESorPWMo6sD1rBfPVQSA6GcSXWUQiRpIHhPK7ArmUZfrsyv1rfRy1S+HNsDrV780WDCi7 6B2SB/0jSoMKjA0/H3LhsF2kalUpw+vpwFkw47Mfo6aKOZ+cK3afdMfX2VBX8BRXDFFDo6za 4YDCuwMNvtaoYbgvVsDtRiwCwejC+zh1zFGhmH43aM43Os9Hg/LxxAgEtEUvXjIsNn5KqUfX Oaox6fI1zXDaPZW1C//54fSdBAhp/CMUq5zccHMyUcvEBnFjk6MqYP7JTOey+MAsmiB4OpmU +KvinIoqwJqrzmvyMcsjZPJhpkJyl/a7yV12ps6KsOhRUN9fNWrH4deuTuAOItqXsMtXXtou CAix7AJt5O2eCgHxZQ5yhDRdvCKc4eG7w7+WeqPLzp0mHZodbC9ihi8/0WtxO3yW8e33VtJq idIksXBu3AN2RHX6sWKTOZ28Emm2TaKzQ/T6+dELFg7laraN54hwqMwmYEJvUvfGS/2nV36j LSXdkUr4uio7/7oYrP8qp+bLY90hRnyM6Qgmsy4G+Q4KRQOUHaB+eimybLs41X1QLBUgf0oj KbZtorWKt4HqaKhAg9V1Jwj6xelADu83tQYh2ELLF1EeBKbj4jpJkrBLOr5Dfe4hVmnjTRlx +jeM7H8AZjALmLPnKngcLpn9kJRyAs+wcpC655KC7wMJu/4V1H1tNzFFR85LxK7w/z6BtV81 4IRR3qCDrOfPajPq1GH/PgvLPOJZIINuDbyNfwl5/n2gH85mF8deLOm3Z8WaH+iBPhmPl6Wb mT2gtcaCWcFpBYxQ/LwhFKfTzFff3eyX6Qi6TEnEI+qEITOS4C3jLCf3Sq3BIBaa2BHB1yWD HvkaYSJV+8JaC2II89hljIEVaKmS48kzRyvtBX1y7xhLurV5iIYtonu1dh75+3UjxEy7iB0A NqH022XUm57gHsERzkt069nu0xy1k+D0bRkg/xfDdFf+utFUh0mOp7E0+x6F9fyVxrdcdeOU VaqW8mpATUsTt0q2NIOeEZ8G9C6jh/ZxSaqArkVl6aKBJMu6K7c0WLxdI5BzCPN07Bihl8gR dZJPmCji6hj7CDfBpXClFiDjKuvfKUYmiXK8SPLxm2X+UpcTQRYUKPfXHlZaFGFg87+4xbzR rmoCL8keiVG09WeJ7ECPszgi1NHT/TLKdrZeXmtln32CRveleDEV5bjZ2hIhHaVM0MDiQ1Go Sfu3WkWAy6gpzibFzlyDRf1ZEiq9+BiqXS9R0tyzgeQbkQn2aDmsgUNi6m6TPUelqkBpD9ns y99SUe02dTXANmotgRmZr5AbMl77FoUnXnBuVlFN4e7Z7tnmkZYdg12u0300BAiG4xGl8khr 1s7wg1oMr6VyhVNemDQxoj+b4XeMXK65xWzc+jW11XZhc6R4bsK4e8kpk/LvACsH04j+jN62 dRPyGOV7ZiMAAd6vYvZdEEx+lA6orjbZnN4/IbIzTh2NqLytDbe2tUvDe9jyxC6ft4ZPrnWX An1W9YXAcSjMolI0xCgcw4EMeZO9aU1I9Ludv2I37SuNfphmzTuhHpO4YR02EaBvyRmTeuA0 5EAyvCelgyJMlW0xEaotMb2koNsdD8VBHGjxDKiCIMQLqx+cIAXCHu/dtWtz4Y2jJrsVnhEs V+7UgpWhYnzJ1zLMgK7hFcOhiF16TS9lCC1ziJ5iWQsp6ubhmnVxvj6MQAAMShNTXVjilHlJ c61icobVQ6mdVtM9lPt6EDkyqxcvKk6IXPURBICbiHwKWBpUYOhuL2YeNJC8tUkvG8ENYb0K UDfUbP7rxYAhmnyFm1YxTs4XyCkvY/igxFgzm6QZiU7vD/Sfsd+wg3a7drXSKtK3zYIcyJ/j CHeGlm2O9TBEcy8r57Yqaj+UmugUscWaiz31caasyD942R2ABq5lvT1m9v9EAF83zWpn9VtU CzJql77bOyJn+yrOORhf0JrLE7y7NBhBoxk1Ic9zJ0dwnkVgJyJ8GFPyDeud48Fn/ujMjxUH 2BDysWd+AX/3Ux/Mn+FouCxHm6QxMdsfZjyY28b3D4889EfDa6V6LJemi4m6lG8rA/Xfb18h mJEmaZosiBc2rxX/lN3kHb4YPhaB0RTMC3ymg7d6tm/qP8Sf2Ozaf2q00E4m9m9DbaEqwUaW XDje55kEzUji6c3eF/KznD37ZnpPdfKatdG/AydlRHBhOt9OZw2jOEWiDAhNW+37hhHg6Yry Adj2523pt3NOmxr+qOyATZJODrvfN8e4HfhgOwN+6Tel5DqFZJnFDIRWZLuRv/9CzMeu8PsM AOWGSE9oHOWSvLPWBWS40B8ozfTAoimYjuJcWIBw4woF3z/bARPxRoZVzIgktslGxC2kYb/J Vxh6GlZ406wvBJIzqgA2wDXam7Ev0/obz41TMLaNx9K9kRY4EyTN8WC7+V1FiUe/5u7rQXLJ HbJLwhPCGgIXASDCTWBdvG24sLc9uGDGuekB/vPZLyKqOUYSv2F34m324BruTqBfsmCJXhtC fQn11ELBCAkXZ6H3WxSFWpOzXyFZtX+xl/04iBtq8Gj7PnnEBni44eCEfoaMNli/Qy3nbbWN +OUg3UxIjJZ25UQgH7QneFPgRhI1Wc3KmfrSO5e5kuvBOrKl6RaDgAWcXZ2PcpMtecn2xVVf NTcgZXz36J5ifg8DxFEU0bgk4enf59vQSn1OVXZCUKMLLnDKyfMxpS9cKq6T7xbj81FuRqqo iqWCQnvM37Q8luhHwDqKuxKgCyBaVZGv5qhdx92FWX5ZNLnbxS/MdYxkDc726Ysj3jHc2IRe 2sZEQsFvvib6iVWhe96EmpK4y9+LOWKrC2e6vHRNpcctfY4SjQxje9R5242jqdE9CwRDuIgg zPc95Q9xjPu2vnK0DdsVwBC7ypGlJ7e91s3Ir3Xr9FBQSqWrU9LtDnLTU1V/Z09TYez86FIl oqWxP+1cmkEqo+Ku5NbXZSxSorPMWJ/Y0CxQGeGVQJYFWzybDONwBAN2PCKqi/M/sV888O93 sNTFPkDEwZvc5FSQkV9Qo5YKc8vDD98mubJ1pZQtyj58EmZRd0E7MrODvjAW63kcGTLyuIeL XPgIJv4LIEaMozynVFoZ0NhhI3BFgzcUIIUysWERh46p19W7HVkCGE+iRqNguyF8XEUD+Wok wRwhgYsOIwQ
Ironport-sdr: 65845219_nKDA07SEgo32ANOK4tDxpy8UGvOGTi3gIVWNFKWFh1pqXiA 92K1wia9DuxsgqpbylSOxRDvTwuZOyGqxhVtV0g==

You can find information about the tutorial with a schedule at

https://github.com/MetaCoq/metacoq/wiki/MetaCoq-Tutorial-@-POPL%C2%A02024:-Meta%E2%80%90programming-and-proving-with-MetaCoq

If you plan to attend the event, we kindly ask you to register your attendance on this page.

There is free remote participation. Please send me an email to get access.

We're looking forward to talking about MetaCoq with all of you in January!

On 12/12/23 17:16, Yannick Forster wrote:

Dear all,

as part of POPL's TutorialFest, we will run a tutorial on MetaCoq.

https://popl24.sigplan.org/details/POPL-2024-tutorialfest/8/MetaCoq-Tutorial

The tutorial will happen on Sunday, January 14th, i.e. on the day before CPP.

> In this tutorial, we will present the MetaCoq library of Coq and the meta-programming features it provides. MetaCoq allows users to write meta-programs on Coq terms and to specify and verify those programs w.r.t. the metatheory of Coq, which is formalized in MetaCoq. Beyond the metatheory of Coq, MetaCoq also includes a verified type-checker and a verified erasure procedure from Coq to untyped lambda-calculus. The objective of this tutorial is to give an overview of the library and focus on its features for the development of plugins and tactics inside Coq. We will present an example plugin development and let you exercise implementing your own meta-programs. To give you the tools to verify your meta-programs, we will also provide an overview of the metatheory formalized in MetaCoq that can be used to show correctness (e.g. type-preservation) of a meta-program.

Presenters:
[Yannick Forster](https://yforster.de), Inria
[Meven Lennon-Bertrand](https://www.meven.ac/), University of Cambridge
[Matthieu Sozeau](https://sozeau.gitlabpages.inria.fr/www/), Inria
[Théo Winterhalter](https://theowinterhalter.github.io/), Inria

The early registration deadline for POPL (and thus the tutorials) is Thursday, December 14th.

We invite everybody to sign up!

[Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th, Yannick Forster, 12/12/2023
- Re: [Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th, Yannick Forster, 12/21/2023
  - Re: [Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th, Milad Ketabi, 12/22/2023