coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ILDS Coq and Lean Autumn School 2023 – THIRD CALL FOR PARTICIPATION

From: Andrei Sipoș <andrei.v.sipos AT gmail.com>
To: undisclosed-recipients:;
Subject: [Coq-Club] ILDS Coq and Lean Autumn School 2023 – THIRD CALL FOR PARTICIPATION
Date: Fri, 14 Jul 2023 11:25:56 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrei.v.sipos AT gmail.com; spf=Pass smtp.mailfrom=andrei.v.sipos AT gmail.com; spf=None smtp.helo=postmaster AT mail-oo1-f46.google.com
Ironport-data: A9a23:1cDx4qCZqUcEqRVW/+Lnw5YqxClBgxIJ4kV8jS/XYbTApGxw0mQOz jdKDWDUOa2LZGbyetkib9vgp08P6MTWm4I3OVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHYTdJ5xYuajhPs/3a80s01BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc53HsIyfK2qRBMHENMNVHyMl+PXtRz vNNfVjhbjjb7w636LeyS+0pgcN6ace3YsUQvXZvyTyfBvEjKXzBa/+StJkIgXFp2JkIQai2i 8kxMVKDaDzJZRFVN1ZRFtQlnf+vnVHwdjRZrBSeoq9fD237lVUujeW9boqLEjCMbfdpjHqXr Ezhw2/oDwkLJOWv2D2PtVv504cjmguiAN5IfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGqKEz8AmsSYC4UUHm5nGDuREYVpxbFOhSBByxJrT83yzJWk4dHxF9WOcr7JAEajUWz ECykIa8bdBwi4G9RXWY/7aSiDq9PykJMGMPDRPoqyNVs7EPR6lj3nryosZf/L2d1YKqRGmhq 9yehG1v2OVJ1J9jO7CTpAif21qRSo71ohnZDzg7s0qg5wJ9IYmiPsmmtQad4vFHI4KUCFKGu RDoevRyDsheVflhdwTXGo3h+Y1FAd7balUwZnYxRfEcG8yFoSLLQGypyGgWyL1VGsgFYyT1R 0TYpBlc4pReVFPzM/8mOd3qU59zlvO/fTgAahwyRooeCnSWXF/XlByCmWbNt4wQuBJ8zP9jZ 8nznTiEUytGUcyLMwZat89EieNxrszP7WzUQp//wnyaPUm2NRaopUM+GALWNIgRtfvayC2Mq oo3H5XQl313DralCgGJqt57ELz/BSJkbXwAg5cHKLDrz8sPMD1JNsI9Npt7JdI6wv4NzLiQl px/M2cBoGfCabT8AV3iQhhehHnHBv6TdFpqZnR+DkXiwHU5f4ek4YEWcpZ9L/Ft9/VuwbQwB 7MJctmJSKYHADnW2SUvXb+kpqxbdTOvmV2vOQiha2MBZJJOfVHC1eLlWQrNzxMwKBSLm/Ewm JCa7TODc6E/H1xjKO30dMOQy0iAuClBueBqAGrNDNphWGTt14lILSbOoOc9CJwOI0+bxx+x9 QWfMTEHr8bj/q4399jog/ifjoGLSuFRIGtTL1P5352XaxbI3zOE6pBSdcq1ZhbhbXPQ1IT+Q PRK3tf+HeYinl0Xg7FjEr1u870y1+Hvq5Be0A5gOnfBNHavNZ9NPViE2ttppIRW57oEpzazZ F2DyuNaNZqNJsnhNlwbfyghT+ab0MAriivg1us0LGr69R1I0uK+C2sKBCa1iQtZMLdRG6Emy 714uMcptiqOuiBzOdOC1i1p52CAK0IbaJoet7YYPt7PqhEqwVR8c5DjGnfIwJWQWe5tbGguA BGp3ZTnuZoN53D/Y0ISFGfM19VznZ4hmg5H535cKkWrmujqvO4W3hpQ+wsZVg5+lwtNwc9vC GpSbWlwKbuEpTtztvMeXWr2QwBlLz+a83zX1FEmujD4TU6pd2qVN0w7G7+H0344+lJmXApw3 e+n2kP6dzf1befN3icWcmx0mczJFNBe2FXLp5G6Ip6jAZI/XwvAvoavQmg58z3cHsI7gRz8l 9lApepfR/XyCn8NnvcdFYKf6LU3TSKELkxkRdVK3vsAPUPYSQGI9Qm+EWKDUeITGKWS6m69M dJkGexXXRfn1CqukCESNZRRH5BKxswW9PgwUZK1A15eqLaOjCtbgLSJ/AjEuWIbadFPk8E8F 4DvSwy/AlGg3UVzpWucg/RHa0yZYMYFbjLSxOqa0vsEPLNdvfBOcXMd6KqVvXKUAlE+/xuro x7yPf7K7u19yLZDm5nnPbVDCj6Vd/LydrWs2yKiv+teaejgNZ/1iDoUjV38LiJqMqA0Sf0us Ziw6PvMw1LikJMtdmLoi72tNvJu252pfex1NsnXEiFrrRGaUpWx3ypZqnGKF5NZtfh8uOy1T BScQ+mtf4c3X9x9+iVkWxJGGUxAN5WtP7bSngLjnfGiERNH7BfmKumg/nrXbW12UC8EFpn9K w3sscaV+dFqg9VQNSAAGs1ZLcd0EH37VYsiUu/Bhz2SI22ro1GF47XczEtqrXmBD3SfC8/17 K7UXhW0Jlz4pKjMy8ofqIBo+AEeCHFmm+QrY0YB4JhMhiunCHIdZ/EoWXnc5kq4TgSpvH05W N3MUIfmISD0XDABdhKlpdq/AEGQAesBPtq/LTssl69Rh+FaG6vYaIaNNA85i5u1Rtcn5O6iI NAavHb3O3BdB7l3EP0L6KXTbfhPn5vnK7Fhxaw5u8P3ChcaR74N0RSN2eaLuTPvS6nwqakAG YT5qa2ojq12pY4d3PuMo0JoJSw=
Ironport-hdrordr: A9a23:HAWM3arD455CvKSzanDmFToaV5oteYIsimQD101hICF9WcaT/v re+sjztCWE7wr5PUtLpTnuAtjifZqxz/5ICOoqXItKPjOW2ldARbsKheDfKlbbakjDH4BmpM NdmmtFZOEYz2IWsS832maF+h8bruW6zA==
Ironport-phdr: A9a23:XkGQyhD/wFHQZ3jAhgUUUyQUD0oY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8zygSUFtyBtLptsKn/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys+pDfeQtFiTqybb9vM hm7rxjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3T bpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjul8 qlrVQToiD8ZODEl7GHZhMtwjKdBrxKgoRx03orYbY6ROfZ7eK7Ses4aRWxcUcZQTCxOHoe8b 4wUD+UfIOlTso3xqlQSoRe7AwSnGeHhxSJShnLu0qI00+ovHwLb0gM8At8Dq27boMnvOaoIT ey50KvFwDPeZP1Wwzf9743Ifwg9rPGKQL1wa9TeyUgyHA3Yj1WQsYvlPTOI3ekKqWeb6fdvV fixhG4msQ1xvCKjxtwtionRgYIV0UvJ9Sp8wIkvJN24TFR3bsKjEJtVriyXMZZ9Tcw+TW9yo ik61qEGtoChfCgM0Jkq2h7RZ+GEfoaG4R/uVPicLzd2iX9lfL+xiRe//Ey8xuD4WcS4zFhEo zRFn9XQtn4BywHf5taaRvZ8+kqs2iqC2gbO4e9KJkA0kLDUK58nwrMol5oTtVnMHjTslEXsi 6+ablgk+u6p6+v8f7XpuoWQN5Vzig3mPKQunda/AeEjMgQUUGib/fqz2bv+9kP6WLVHluM6n rXdvZzAJskWprS1DxJU34o+8RqyADar3dIFlncdNl1FYgiIj43xNlHOPv/4CfC/jkypkDhxx vDGOqTtApLKLnTeibvhc7lw5k9GxAo8ytBf4J1UCrUfL/7pRkDxs9nYAgc4Mwyy3ennFM1w2 p0CVW+LGKOUM6PfvUWV6u8uPuWAfoAYtTflJ/gg/fHujHs5mVEHfamu2JsacGq3HvJ7LEWDf 3Xsg80NEXkQsgolTezqkFqCUSVIana9WqIz/DA7CIa8AYjfQYCthaSN3CGgEZJOfGBJFkiME Wv0d4WDQ/oAdTqeItV9nTwcSbihV4gh2Amyuw/90rprN/bb+ikFtZ34z9V1/O3SlRQq9TNuF cid0meNT3t1nmwSXTM20rp/8gRBzQKe16R5mPdcEsde67ZTXww7LZ/RyfBhWYOhdBjGe4KgT lq8T9TuOjApSTB5l9YIb1xwGpO8yAvCxy2xK7AQnr2PQpcz9/SPjDDKO89hxiOeh+EahF48T 54fZAVO54Z6/gnXXcvSllmB0rytfuIa1TLM82GKySyPultZWUh+S/aNRmgRM23Rq9mx/UbeV /m2E71yOw1N08ODbLUMcdzxik5uS/LqOdCYaGW0yC+rHRjd/rqXd8LxfnkFmiDUCUwKiQcWq H+AORIzB2G/5XnfFDt1PV3qakLot+J5rSDzVVc6mieNaUApzL+p4lgViPibHusUxa4BsTw9p i9cGV+825fRDIPFqVY/OqpbZtw57RFM0mexWxVVGJumIugig1cfd14ypEbyz1BtDY4Gl8E2r XQsxQ40KKSC0VoHeSnKlZb3cqbaLGX/5nXNI+bfx03e3dCK+6wO9OVwqlPtuxusH1Yj9HMv2 sdc0n+V7JHHRAQIVpe5XkEy/hl877bUB0t1r4rS2WdhMO+q9CTDw9UyLOQgwxekOdxYNeLMF QP/FdEbG9n7MPYjyD3LJloPOOFf8rJxPtvzLaPXnv72er8+xXT60zcigsg1yE+H+itiR/Sd2 p8Ex6vdxQ6bT3Lmi1zntMnrmIdCbDVUH2ylyCGiCpQCA886NYsNF2qqJNW6g9tkgJu4EXde+ ESuBhUYntSoYR2JR1P41AxUk08QpDb0/EnwhywxiDwvoqeFiWbHxej4eRtBJChQRXFlln/jJ IG1i5YRW03iPG1L3FO1oE39waZcvqF2KWLeFFxJcybBJGZnSqKst7CGbqaj8bsQuD5MGKS5a FGeEPvmpgcCljnkFC1YzSw6cDejvtP4mQZ7gSSTNiQ7oH3ccMB2jRDRgb6UDfdX0iALRW9mz yLWHl+nF9as9NSQ0ZzEt6iyWnmgWZtabSTwhdnY5W3ruCszX0T5w677k8aCc0ByySLh0th2S SjE5A3xZIXmzeXyMO5qeFVpGE6p7sN7Ho9klY5jzJoU2HUcmtCU5S9dyTa1YYgdgPynKiZTF ltpi5bP7QPo2VNuNCeMzoP9DDCGx9d5IsO9aSUQ0z486MZDDOGV6qZFlG17uAndz0qZbP5jk zMa0fZr5mQdhrRDsQwh1CicRK5UBkhAOjfEmBGB7tT4p6JSLjXKE/D4xA9lkNatAavX6AhaV Gz0e9E8WzRx9sJkGF3J2Xz3rIrjfZODCLBb/g3RmBDGge9PLZs3nfdfnitrN1X2ung9wvI6h xhjjtmq+ZKKIGJ38OelEwZVY3frMtgL9Gin3sM81o6GmpqiFZJ7FnAXUYv0GLi2RSkKu62vN h7SQmZh7C7KQfyFQVDZsAA88zrOC8z5aS3RfiJCi4w8HF/FYxUO5WJcFDQiwsxnSEbznJanK AEhoWpJrl/g9kkSlKQya0i5Aj+Z/EDyMn81UMTNc0AQt10EvhaPd5TZt7IWfWkQ/4X9/lPRb DXBOkIQSzlOAxLMBki/bOD2tZ+ZrLfeVqzmaKGXKbSW9b4HCKzOnMPzlNMgp3HVaKDtdjFjF 6FpgBISGyAkXZ2Dy3NXDHVI3yPVM5zB/Un6p30x95HltqysAVOn5JPTWeELb5M1oEHw2v3Fb 6nJ1UMbYX5O35cIjxck0ZA521gfw2FrfjipS/EbsDLVCbjXkelRBgIabCV6MI1J6bg9109DI 5yTjNS9zbN+gvMvbjUNHVX8hsGkY9ALKGChJRvGAkiMLrGPOTzMxYn+f6q9TbRaiOgcuQe3v H6XFErqPzLLkDeMNVjnKeZXkCSSJwBToqm4exdpTG/kFZfoNkP9P9hwgjk7h7YzgzKCNGIRN yR9b1IYrrCU6nA94L03EGhA43x5aOicznzBvq+Id9BP76ItXnon8oASqG43wLZU8ixeEfl8m S+I68Vrv0njiO6EjDxuTBtJrD9PwoONp0Rrf6vDpfwiET7J+gwA6WKIBlEEvdxgX5fmvaxKx 9mJiuToKS9F6Prb+MIdA47fL8fNYx9DeVL5XSXZCgcIV2vhLWbEm0lUi+2f7FWQp5k+75/rw d8AFuEdW1syGfcXTE9iGZZRRfU/FiNhmrmdgskS4HO4pxSEX8RWsKfMUfeKCOnuIjKU5VGhT xQNyLL8a48UM9+js6SDQlxznYCPHE2JGN4R/GtuaQg7pEgL+397HDVbM63NZQak4XtVHvmxz Edetw==
Ironport-sdr: 64b106ba_nn5xlqcYvuloPFv+604Bxmxw7sgFaZhw36sTLAioBHqblbk jDKps0It0cuHbZMG9MpbkCiYG4z+TeJW2V5NKUg==

ILDS Coq and Lean Autumn School 2023
interactive theorem proving school

September 18-20, 2023, Bucharest, Romania
https://events.ilds.ro/autumnschool2023/
co-located with FROM 2023
https://from2023.cs.unibuc.ro

DESCRIPTION
-----------

The ILDS Coq and Lean Autumn School 2023 aims to introduce potential
students to the Coq and Lean proof assistants, as well as to
theoretical underpinnings of interactive theorem proving. It is the
second school on interactive theorem proving organized in Bucharest,
following the ICUB Coq Autumn School, which was held in September 2018.

The event is co-located with FROM 2023 (https://from2023.cs.unibuc.ro/),
whose participants are eligible for a special discounted fee for the school.

ORGANIZERS
----------

Institute for Logic and Data Science (ILDS, https://ilds.ro/)
Research Center for Logic, Optimization and Security (LOS), University of Bucharest (https://los.cs.unibuc.ro/)

SPEAKERS
--------

Horațiu Cheval (University of Bucharest)
Vlad Rusu (INRIA Lille)
Andrei Sipoș (University of Bucharest & ILDS & IMAR)
Julian Sutherland (Nethermind)
Traian Florin Șerbănuță (RV & University of Bucharest & ILDS)

COURSES
-------

Andrei Sipoș, Introduction to Type Theory for Interactive Theorem Proving
Vlad Rusu, Traian Florin Șerbănuță, Introduction to Coq
Julian Sutherland, Horațiu Cheval, Introduction to Lean

No parallel sessions are planned, so it will be possible to attend all
the courses.

REGISTRATION
------------

The registration fee is 150 EUR for the general public and
75 EUR for those who participate at FROM 2023.
It covers attendance, lunch, coffee breaks, and the official dinner.

To register, please use the common registration form
(https://forms.gle/aZ7zqK3UNwLeGaRL6) for the ILDS Coq
and Lean Autumn School 2023 and FROM 2023. Note that
one can still register later, separately, for the autumn school
and still benefit from the discount.

ILDS offers a limited number of fellowships (waiving the
registration fee) for students. Students interested in getting
a fellowship need to complete an application form
(https://forms.gle/ByrWCxUahQcfK35HA) by 1 August 2023.
Applicants will be notified by 14 August 2023.

IMPORTANT DATES
---------------

Deadline for fellowship (fee waiver) application: 1 August 2023
Notification of fellowship applicants: 14 August 2023
Deadline for registration: 7 September 2023
School: 18-20 September 2023

***************

Further information is available on our website,
https://events.ilds.ro/autumnschool2023/

[Coq-Club] ILDS Coq and Lean Autumn School 2023 – THIRD CALL FOR PARTICIPATION, Andrei Sipoș, 07/14/2023