Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Milad Ketabi <ketabii.math AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] MetaCoq tutorial at POPL on Sunday, January 14th
  • Date: Fri, 22 Dec 2023 10:30:59 +1100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ketabii.math AT gmail.com; spf=Pass smtp.mailfrom=ketabii.math AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f47.google.com
  • Ironport-data: A9a23:2IG7ZK8fGGUZ+2tQU+nJDrUDGHqTJUtcMsCJ2f8bNWPcYEJGY0x3m mVJUTuBbPuPMTDye9xwYYq1pkIPu8LWn9E1GlZu/iBEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPymYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWYoWo4ow/jb8kg25q6r4GlwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TEyKRcHl06LNEjueN6HG0e1 dkfdiASV0XW7w626OrTpuhEg80iKIzmMNpatC0/iz7eCvkiTNbIRKCiCd1whm9hwJATW6yGN 4xFNlKDbzyYC/FLElQaFJs0nebug3DjcxVXrVuUoew85G27IAlZj+W0a4GOJYXiqcN9nXTfo kzCo0/FWksHDuGnyj+H11eur7qa9c/8cNlPTeXnp6ACbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72SuR9j5GhC0+TuK4kFaVN1XHOk3rgqKz8I4/jp1GEAPHwxTdNA36PR1QDE32 g+putS3FSNW5ej9pW2myp+Yqja7OC4wJGAEZDMZQQZt3zUFiNFs5v4oZoY8eJNZnuHI9SfML ydmRRXSap0WhM8Pkqi3pBXJ323qqZ/OQQo4oA7QWwpJDz+Vhqb0OuRECnCCsp6sybp1qHHf5 xDofODAt4gz4WmlznDlfQn0NOjBCwy5GDPdm0VzOJIq6i6g/XWuFagJv2klfRcybphfJGOxC KM2he+3zM8MVJdNRf8oC79d9+xzk8AM6Py8Cq6NM4cTOPCdiifWpnk3OCZ8IFwBYGB3zPhnZ sbFGSpdJXkdDqtjwXK3QexbuYLHNQhvrV4/savTlkz9uZLHPCD9Ye5cbDOmMLplhIva+1692 4gEZ6O3J+B3CrKWjt//qt5Nczjn7BETWfjLliCgXrTcfVs5Qj98W6e5LHFIU9UNopm5X9zgp hmVMnK0AnKm7ZEeAVzSMC4xW6ClRptls3MwMAolOFviiTBpYp+i4O1bP9E7dKUuvr4rh/Nlb eg3S+PZCNR2SxPD52s8a7v5p9dcbxiFv1+FEBekRzkdRKReYTL11OXqRDayyxlWPBGL7ZM/h 5aCyjLkRYEyQlU+LcTON9Oq4VCDnVkcv+NQWUH3DMFZUxju+tIyKgjarPw+E+cTIzrtmxqY0 Ae3B08DhO/v+oUazvjAtZqmnayITdRsPxN9NHbJyJqLLg/mx3qH7a4cdfeXbBbfeXjR+q7/V d5Kzvr5DuILrGxKv6V4Dbxv66A0vPnrmJN30SVmG2ftfX2wK7Y9PESD49ZDhpdNypBdpwGyf ECFofteGLeRPfLaAEwjHxUkYsuDxMMrtGHrt9ptG3rD5Qhz4LajemdRNUPViCVicZ1EALl8y uIl4MMr+wizjyQxCem/jwdWyn+tK0IRWKB2p7AYB47W0jAQ8G9gWqCFKCHK48CoUe5uY20KO T6fgZTQi4tMnnTid2UBLlmT/O5/q6lXhjV04g4jHXqrlODBpMcL5zxK0DFuTg1q3hRNiO1yH W5wNnxKH6aF/hY2pc1PQ1GTHxplATuH8HfQ0HoMrnXSFGOzZ1zOLUo8GOeDx18Y+GRiZQpm/ KmU5WLmcDTyduTz43cWdWt6jcf8FPpd2xbnms+1O+ikRbwBfivDkKuiQUEquinXK5o9q2Ofr NY74dsqT7PwMBAhhpESCq6Y8O81Yw+FLmkTesNR1voFMk+EcQ7jxAXUDV66f/5MAPn48UWYL chKDeAXXjSc0Be+lBwqNZQuEZRVwsFwvMEjf4n1L1Eoq7Gc9zplkKzB/xjE2VMEfY9crtYfG KjwKRS5DW2itVlFkTTsre5FGFaCT/sqWQne5N2xocI1T88tkec0akwj8KqGj1PMOitdwh+kl gfiZajX8u9c9bpRj7bcSqVtOyjkKPfYdvi5zwSogtEfMfLNKZjvsi0WmHnGPiNXH6cgZNBss Yuzs/vMhUbjkL0rYTqIhavbB61t4OOsVtF2KePyFmFRxgGZaf/v4jwC2mG2EoNIm9Vj/fuaR xO0Rc+zVNwNUfJP7SVxRwkHNDhFEIXxTKPrhR3lnsS2EhJHjDD2doK2x0HmfURwV3EuOaSnL iTWpvz3xNRTjLoUNS8+H/s8XqNJeg7ya5AHKe/0myKTVFSzo1W4vbDnqxosxBfLBlSAE+f4+ Zj1fQf/RjvjpJD3yMxljKIqsi01FHpdhcwCTnAZ8fNyiBG4CzciBsYZOpMkFJpVs3LT0LfVW TLzV1YhWB7NBWl8TRbB4drdB1bVQqREP9riPTUm8n+Fcyr8VsvKHLJl8Twm+HtsPCfqyOa8M 9wF53nsJV6Lz4p0QfoIrOmO6Qu9Kig2GlpTkaw8ryDzP/raKbAD1XgkEQYUECKbTIfCk0LEI WVzTmdBKK1+pYgdDu44E0O52jlA1N8s89nsRSiKydfb/Y6cyYWsDdXhbvrr3ORrgNsifdYzq LCee4dJy2+T030X/6AuvrrFREOy5e2jRqCHEUMoeeHec2xcJIjq0wPuUBfjlP0fxTM=
  • Ironport-hdrordr: A9a23:slSGkq5jG+Kx6v95mQPXwPHXdLJyesId70hD6qkRc20tTiX8ra qTdZsgpHrJYVoqKRMdcJW7Scq9qBDnlKKdg7NhWYtKNTOO0ACVxcNZjbcKqAeQfBEWmNQts5 uIsJITNDQzNzVHZArBjzVQ2uxP/OW6
  • Ironport-phdr: A9a23:oeWCxBHIcBcxs26SVpsxZJ1Gf3RFhN3EVzX9CrIZgr5DOp6u447ld BSGo6k33BmTBNuQsqoMotGVmp6jcFRD26rJiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalsI BmrrAjdudQajZd/Iast1xXFpWdFdOtRyW50P1yfmAry6Nmt95B56SRQvPwh989EUarkeqkzU KJVAjc7PW0r/cPnrRbMQxeB6XsaSWUWjwFHAxPZ4xHgX5f+qTX1u+xg0ySHJ8L2TLQ0WTO/7 6d3TRLjlSkKOyIl/GzRl8d/i79VoA+6pxxn3YHbfJ2VOvR5fqPYZ9waRGxBVdtVWyFOBo6wa o0CBPcDM+lFtYnwv1QBrRW8CgesCu3hySJGiGHq0qAhyestDRvL0RY8E94SsnnZqsj+OqcIU eCyyanF1TLNb/JS2Tjn9YfDbxUvru+QXb1qasXRyFQkGgTGjlqOtYzqJSia1uUMs2SB6upvT /6vi248pgF+pzig3MYsio3Tio0JzVDE8Dx0zYAoLtK3VEB1e8SrEIdMty6ELYt2RNsvT39mt is0ybALpJ61cSsKxZop2hLRa+KKfpaJ7x/tV+ufISl1iW55db++iRi/80ytx+LgW8S31FtGs y5In8fSun0Lyhfd5M+HSv5n8Ueg3zaCzw/T6uBYIUA0iKrUMIQtzaI3lpoWqUjDBS72mEruj K+SbEok/PKk6+P9YrXpvpOdN4F0igbkMqQ1hsywH/44PhITUGeF4ei80aPs/VPnT7VMlPE5i LXWvIjbJcQdvK65AhVa3pwt6xalFzum39UYnWUHLFJYYx2LlYnpO1bILfvlDvm/m0yhnCl3y /3CJLHsAZXAImLdnLv9frtx8UFRxQg1wNtC+Z9UDqwBIOnvWkDvrtzWEx45Mg2qzOv/FNlw0 J4VV3iVDa+DKqzStEeF5uIxLOmIY48YoDP9JOIk5/7qlHM2h0IScbSw0ZsZZ321HO5qI0qeY XrrjdcBFXkFshAiQ+ztjV2OST9TZ3CsUKIg/jw3Fp6qAIPZSo2ugLGNxjm3EoFVa2xcBV2BE 2/kd4CeVPcNbCKSLNVhkjsBVbW5SI8uyw2uuxXhxLpmL+rY4CgYuoj/1Nh1/ODTmhQy+iZ1D 8SZyW2CU2Z0nmYQSz8wx69wuVZ9xUub0ahkn/xYEsRe6+5RXgcgKZHc1/B6C8z1Wg/ZYtiJT 0+mTsy6DjE1U9I+2MQDY119GtWnlhDMxTCmA74Tl7yRBZw76LjQ33brJ5U193GT3644ylIiX 8FnNGu8h6c5+RKAKZTOlhC8lqKjeew/0TLE/mbLmWmDoEhSUQ82VKzZXVgQY0LXqZLy4UaUH OzmMqguLgYUkZ3KEaBNcNC80QQurJbLPd3fZzn0gGKsHVOTwavKaoP2emIb1SGbCU4ekglV8 2zVfRMmCHKHpGTTRCdrCUqpe1nlpOpztHqxT05yygiWb2Vu0rO0/lgegvnPA+gL0Oc8sTw64 y5xAE772tvXD9SaoA80f6hAaNk84RFC3H7ZnwN4N52kaatlgw1WaBx56mXp0Rg/EYBciY4qo XctmRJ1Mr6d2Uhdeimw2JnxPvjaJjC38kzwLaHR3V7a3ZCd/aJnBO0QjVLlsUnpE0Mj9y4iy NxJyz6H4Y2MCgMOUJX3W0Jx9h5gpricbDNvr4XTnWZhN6W5qFqgk5ogGfclxxC8ftxeLLLMF Qn8FNcfDtSvL+pikkagbxYNNuRfvKAuOMbue/yD0a+tdOFu+VDuxWdK/Il300PK8iNgSsbH2 p8Ex7eT2Q7GHzbwgVG9s9zmzJhebGJ3fCL3wizlCYhNI6xqKNxTWCH+fovtnoU428G+PhwQv ESuDF4HxsKzLB+bblimmBZVyVxSunu/3y2x0z1zlTgt6KuZxi3Hher4J39lciZGQndviVD0L M26ldcfCQKrYhQgnhqko0Pz26hzq6F2Lm2VSkBNNXuTTSkqQu6ru7yObtQaopAlrSxdUeX6Z FmGSpbyphIb12XoGG4Ul1VZP3m6/57+mRJ9kmeUKn1++WHYdc9HzhDa/NXARPRV01LqXQFAg CLMThi5NtitppCPkovb9/u5TySnX4FSdi/iycWBsjG67CtkG0/3k/e2k9zhWQ80tE2zn9pnS SzCrRe6Z4D314y1NOtmeg9jA1q058dhG454m5c9n9lKgSlc1sjTpyJX1zusedxAkbrzdn8MW SIGz7u3qED+1UtvI2jIj4P1W3OBw9dwMtyzY2cYwCU4vIhBDKaZ6qABnDMg+ALp61KMJ6Ilz nFBlqhLijZSmewCtQszwz/IB7kTGRIdJinwj1GT6Mj4qqxLZWGpeLz21UxknNnnAqvRx2MUE Hv/ZJomGjd9q8tlN1eZmn7+9ojuediWaNsPtjWblh7Bi65eL5d7xZ9ozWJ3fHnwu3Eo0btxj hFy1Ju7vc6CInlt1K28Cx9ccDbyYolAn1OlxbYblcGQ0Ye1G5xnETheR5rkQ8WjFzcKvOjmP QKDQ3Us722WEr3FEUqD+V9r+jjRRouzOSjddxx7hZ1yAQOQL0tFjEUIUSUmy9QnQxuyypWpc V8ltGtMoAep8l0Wlr0ub16lDi/evFv6NGtyEsPEakMItkcaoB6EVK7WpuNrQ3MGoNv49FbLc irDIF4QRWARBh7aWRa5YujotYGGq6/CXqK/N6ecPu/I8LAYDqbSg8roi9sDnX7EN93TbCY+S aRhhwwbGyg+QpqRmi1TGXVPx2SUMJHd9FHkvXcu5sGnrKayB1mpvNrTTeMUaZI2pXXUye+CL 7LC3n4ob2YFkMpWlTmQj+FAlF8K13M0LmfrTORG7H+XCvqXw/4fDgZHOXkqao0StPN6hVMLY YmC27aXnvZuh/oxQT+pTHTHncekLYwPKmC5bxbcAVqTca+BPXvNyt32ZqW1TftRiv9Vvlu+o 2TTFUirJTmFmzTzMnLneehRkCGWOgBfs4ChY15sD2bkVtfvdhy8Npd+kzQ3xbQ+gn6CO3QbN HBwdEZEr7vY6i094L03A2ta8n9sNvWJgQ6c5ujcb5sa6L5lXnsymOVd73A3jbBS6WAMRfB4n jfTss87o1yilbrqqHIvWx5PpzBXwYOT6B86aOOJq98aASaCoE1eiAfYQw4HrNZkFND17qVZy 9yU0bn2NC8H6NXMu80VG8nTLsuDdnsnKxvgXjDOX25nBXamM3/Sg0tFnbSc7HqQ+9I5p4Tlk psPDLpSSFwdGfYTC0AjF9sHasQSPHtsgfuAgcgE6GDr5gHWX9lft4vbW+i6BPzuLHOUgeABa UdXh7z/KosXO8vw3EkoOTwY1MzaXkHXW95KuChoaAQ59V5M/HZJRWo2w0v5awmp7Rf78Na7m xc3jk11ZuF/rF8EDH84I1PLoG07l0xjwL0NYBiUeT/1aaq8BMRYV3WyuE82PZf2BQ1yaF/q9 XE=
  • Ironport-sdr: 6584cabe_6LMfn4ubp3W7ieltn+vyvJloUI8ui5j5uHyRb9JOLxl2rQ1 vq073qD5sqj2wGMZfxxhiCMmGwzTpKH/72j9n0w==

Dear Yannick,

It would be my pleasure to participate remotely in the tutorial. I would still be living in Melbourne, Australia, by mid January and therefore remote participation would be my only realistic chance.

regards,
Milad

On Fri, Dec 22, 2023 at 2:04 AM Yannick Forster <yannick AT yforster.de> wrote:
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!



Archive powered by MHonArc 2.6.19+.

Top of Page