coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FME Teaching Tutorials series continues on August 26, at 3 pm CEST: Dr. Robert Lewis (Brown University, US) on "Teaching the theory and practice of proof assistants with Lean"

From: Luigia Petre <Luigia.Petre AT abo.fi>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] FME Teaching Tutorials series continues on August 26, at 3 pm CEST: Dr. Robert Lewis (Brown University, US) on "Teaching the theory and practice of proof assistants with Lean"
Date: Mon, 22 Aug 2022 14:05:03 +0000
Accept-language: en-US, sv-FI
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Luigia.Petre AT abo.fi; spf=Pass smtp.mailfrom=Luigia.Petre AT abo.fi; spf=None smtp.helo=postmaster AT smtp-out.abo.fi
Dkim-filter: OpenDKIM Filter v2.11.0 smtp-out.abo.fi 0532F10CFEDF
Ironport-data: A9a23:zuiAbKsG2V2bUd23Y4Ob84Ft+OfnVEFYMUV32f8akzHdYApBsoF/q tZmKWGFOvmLYjfxLtFyb4rk8EhU65SAz94xG1durnhnFiMQgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+52FYgf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnZHvb14sEbXqosIQVAgILx5abIt6wZaSdBBTseTLp6HHW2Dp3+0rC1wqe4QS/aB5AAmi9 9RBc2hLNEvZwbjvmvTmEoGAhex7RCXvFKcCu35hxHfhAOo8TLjKSaKM694wMDIY3JkeQaqAP pdxhTxHbQyQX0RJC3IsD7EwsPao3nDgSxdetwfAzUYwyzOJkFQvj+OF3MDuUteNXIBemluSj nnX+nzwRBAcLt2WjzSfmk9AncfUmD/jHYUPCPux/Pksjlz7KnEv5AM+WASd+PyWkmiEfd9YO hwoxQ5/i5QL3Rn+JjXiZCGQrHmBtx8aftNfFewm9Q2AopY4BS7CWwDoqRYaN7QbWN8KqS8Ci AfVwo65bdB7mOfPEy3Crt94uBvvURX5O1PucgcqbGPpCfHfvZswk3ojpf45SPHt17UZ9RnLx C2WrDcznKlbo88N06y98Tj6b9+EvZ3VVksy+xmRV2iiqA14DGJEW2BKwQaAhRqjBN/HJrVkg JTis5PFhAzpJcrR/BFhuM1XQNmUCw+taVUwe2JHEZg77CiK8HW+Z41W6zwWDB43bJ9dIWG3O x+K4105CHpv0J2CMfAfj2WZV5VC8EQcPYi1PhwpRoQWM8cgLWdrAgk3PRfPt4wSrKTcufplZ c/FLp3E4YcyFaVq0De7Qa8B0LI3wTwzxmXSRJPyyVyk3KGdeWXdTqZtDbd9Rr1R0U9wmy2Mq 4w3H5LTk313CbSuCgGKr9J7BQ1UfBATWMCnw+QKJ7XrClc3SAkJVaWNqZt/INYNt/oOyY/1E oSVBxUwJKzX3yOXcG1nqxlLNdvSYHqIhShhZHJ2ZAb1hilLjETGxP53SqbbtIIPrIRLpcOYh dFcEylZKvgQGDnB5RoHapzx8N5reBix21CHNS3jbjlmJ8xsQAnA+9nFeArz9XdQVHTn5ZNm+ 7DwhBnGRZcjRhh5CJqEYvyYyV7s72MWn/h/XheVL9QKIBfs/YFmJjbflPgyJ81QexzPyiHEh Q+cBlEWpLCV8YMy9dDIg4GCrpuoTbUkQBoKRzGD4O/vZyfA/2elzYtRa8qyfGjQBDHu5aGvR eRJ1PWgYvcJq1BH7thnGLFxwKNiutbiquMIzglgG3mXPV2nBqk5fyud2NVX86pQ2vlQswzwV EPWootWPrCAOcXEFl8NJVR7NLrThalMwjSCv+4oJEja5TNs+ObVW0tlORTR2jdWK6F4Md94z Op96tQa7Rez1kgjPtqc130G7GGQNjkHTrlhv5sdRoHq01J5xlZHaJ3aKyn3/JDRNY8SYhlye meZ1PjYmrBR5kveaH5vR3LD6uxQ2MYVsxdQwV5eelmEl7IpXBPsMMG9LNj2cuhU8vmD+/l2J nAuMFBpY6yE+HFmhaCvmoxq9x5pXHWkFo7ZkjPlV1E1i2GhXGuLImxV1SOl4hUC62wFFtRE1 Ojw9YsmOAoGuOn41Cx0V08NRzkPizBu3lWqpf1L1Php03X3jfQJT0Nuiac1R8PbPP4M
Ironport-hdrordr: A9a23:Nv14xKg4DCg5wp2PC5brKRgVNHBQXvYji2hC6mlwRA09TyXBrb HJoB1p726MtN9xYgBcpTjjUJPrfZq4z/NICOYqTNOftWXd2VdAT7sSkbcKoQeQfBEWn9Q1vc wNHMZD4bbLfDtHZLPBkWyF+qEbsbu6Gc6T5ds2hE0dNT2CI5sQlDuRJDzraHFLeA==
Ironport-phdr: A9a23:+k4ivR1ZawU/tv8TsmDOkA4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaEo68z0xSWBc3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip2e2+4YPfbgRKiTayY75+M Ai9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjT bxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr8zRDqi8 rxrSAf2hygbKz43/mbXislqg6JaphKquhhzzoHQbY2QMvd1Y6HTcs4ARWdZXshfSTFPAp+yY YUMDuoOIelXopLnqFcSrxuzHxWgCP/yxjJOm3T43bc60+MkEQze2gIgAtMOsHvVrNrvKawcS /66zLXSzTrdcvhb3jHz6JXJchAuoPGDR6h8f9DPxkkzDQPKkE6dppb+MDOSzOgNvWmb4vNmW OmyhGEptxt/rSKzxscwlIbJnIQVx0jZ+Ch53Ys5ONy1RkBnbNK4EpZduTyWOol4T84/Xmxkp CU3x7IbtJC1YCQG1IorygPdZvCbc4WF/wzuWPuSLDp8gn9uZbyxhxG38Ue6y+38UNG50VdNr ipCl9nArG0N1wfL5siIS/t94keh2SuU2AzJ6+FEJlg4mrDAJJ4m2LIwmJsTvELeFSH1gEX7l LKae0s49uSy9ejqbKvqqoWCO4NplA3yKKQjltCnDeglPAUCQ3KX9fqy2bH950H1XbRHg/Msn qTXsZ3WPdkXq6ClDwNPzIou5QizAy273Nkan3QLNl1IdA6BgoP0IV/BOur4Au26g1m0kDdk2 fTGPrr5D5XWK3jDjK/hca96605B1Ao/18pQ6IlTCr0bLvLzW1f9tN3eDhAnLwy52/vrBdth2 o8ER26CDLGVPLnMvVOV+O4jOemBaJMNtDb4Mfcl5vrujXEjmV8aeKmkxZ0ZaG25HvRpIkWWe 2DgjM0fHmcWpAoxUvfnh0eZXj5UfXqyUaM86ik9CI29FYjDXJyigKSd3CenGZ1bfn1KBkiWE Xj0b4WER+sMaCWKL8B9lTwETKGtRJMl1RGzrwD30KFnL+rR+i0Ar53vztl15+vJlREz7zN4F cqd03veB11zyykDQCZz16Riq2R8zE2C2O52mbYQQddU/rZCVhowHZ/a1e1zTd7oDFHvZNCMH XK7Q9qnCHkJQ84rzpdaR1t8FNSryCjOwzCnK7YfkPqFBcpnoernw3HtKpMlmD793647ggx6E 6OnVEWjj697rE3IApLR1l6ej+CsfLgd2yjE8CGCy3CPtQdWSl04Sr3LCFYYYEaettHl/gXaV bb7LakmPQpIj/aPNrFHQtTjihNIRaSrI8zQNlq4gHz4HhOU3vWJZYvudX8a2XD5FUkLkglVx XuaLwUWDy2m5WzfX3R1DVy6RUTq/KFlrW+jCE85ywbfd0p6y7+84QIYn9SHTu8Lm7UZpGEoo TIyElfVM8v+Ld2GqkIheaxdZYh4+1JbzSfCsBQ7OJW8Lqdkj1pYcgJtvkqo2Q8lQoNH2dMnq n8n1m8QYeqRzU9BejWE3JvxJqyfK2/8+wqqYrLX3VeW2cif+6MG4vA141v5uwThGk0n+nRhm 95bthnUrrHXDQUTWNTJX1ot+jBzrbacbCh8r4LY2HtwMLWl5yfY0oFhD+8kxxC8OtZHZfrfT EmoSJdcXZH0brFyyD3LJloeMetf9bA5JZajfvqCg+uwOfp42SmhlSJB6Zx81USF82x9TPTJ1 tAL2aL9vEPPWjHigVOmqs2yl5pDYGRYOne+xintQrZcerd/VY8BDiGgIofko7c2z46oQHNe+ FO5Uhkixc6meBPUV1HhxwB43E4Q53Km03jw33l/lDcnqbCa1SrFzrH5dRYJDWVMQXFrkVbmJ YXcY8kyZEGzdEBpkRKk4R2/3K1HvOFkKHGVR05Ufi/wJmUkU62qt7PEbdQdoJ8vtCxWVqy7b zX4AvbZvhoV0iqlJ2ZC3j0Tfjut/Jv41xB3k2OSKn9voWGRIJoog02EvpqGHKQXg2JOTTIwk TTNA1mgI9SlmLfc34zOtOyzTSPpV5FedzXq0ZLVsSK64WNwBhjs1/u3m9DhDU07yXqijIEsD 36S6kylOM+2j/ffU6ovZERjCV7i5tAvH4h/ltB1n5QMwT0BgY3T+3MbkGD1ONEd2KTkbXNLS yRYprydqAXjxkBnKWqEgozjUXDIiO98Zta7ayUu1z4n4uhDAqDS4r0Ozk4X6hKo6BncZ/Rwh GJX7eYv538TxdkEpBAg5iyXBfYcHAMLWE6k3wTN5Ne4oqJNYW+perXlz0tyk+eqC7Saqx1dU nL0Kd8yWDV95cJlPBfQwWX+v8v6LcLIY4tZ5Xj221/QyvJYI5Urmr8WiDp7bCjj6GY9xbdzj AQyj8jh5M7dcD8rpvviREcCbnX0f59Bo2q1y/wFxIDMhtrpQ80EeH1DVcntQfvtFy8O8/juK w+FHTsgp23dF7uXHAmU7FpqoiD4CIilcXySLXgdwM9jAhecQS4XyAESVzEnkpNrDRikgsnod ktj5zQV70bg7BBLz6ppL0WtAzqZ/Vj1LG5tE97GfEMeuQhG4w293dW2yOV1EmkY+5SgqFfIM WmHf0FTCnlPXEWYBlflN73o5N/a8uHeCPDsZ/3JKa6Dr+BTTZLqjdqmz5dm8jCQN86OImgqD vs13VBGVGx4HMKRkisGSigenSbAJ8CBoxL09ipyp8G5uPPlPWCnrZOIEKdXOM5z9gqemqKfL 6uXmTo/IDxfkJ0NhDfJxLUZwF8OmnRuej2qQtFi/WbGSKPdnLMSDgZOMngrcpETteRmh1MLZ JaI77G9nqR1hfM0FVpfAFnom8XyINcPP3n4L1TfQkCCKLWBIzTPhcDxe6K1D7NK34A2/1W9v yiWF0j7M3GNjT7sAlqLLOBDjSjdBBFCooyVexxqT2biBoGDCFXzIJpsgDs6zKdhzGvNLnIZO CNgfllltbiM9WZfn+k5EmZGqHRkZ7rh+W7R/6zTLZAYtuFuCyJ/mrdB4Xg0/LBS6TlNWP1/n Ca6Rj9GuFS6iqyI1yYhWRBJ7DhK1trjVapKMK/esJdBCy+sFPcl5G+XTRoL9YMNNw==
Ironport-sdr: JQG9smPVtuNiter35bKgbyfYToXJWB2+tsT630LbOfwPj9kc+ROossxtqFUr9nMb7xYw8PfhAz kJfClIeHnw4ZdiptGZSjkyQPXI4MucBMIwbY/RmvajpWf+bWrM5dI1g3OoQzh4iLIw3k1h6tC7 EWBwpYHUk28cnbV/MxLMPi8kCyCA6Gz/ABWJd0ZAKUxKL6unbbgMpxDIdtz7HuR01yDA3R4mXw 94ckQoV82Sb0arS/SdhoDQ2QGH+CqS20WkFB6SMJqWkqFAl82czxh7WKiC0nSO6oXmsWRXV9kw RVLgsQTn3+7JMga3fpXFAKky

Dear all,

On the last Friday of the summer, we have the opportunity of a theorem prover
lecture from an Ivy League colleague!

Dr. Robert Lewis (Brown University, US) will lecture on Friday August 26,
2022, at 3 pm CEST on the Lean theorem prover. His talk is entitled "Teaching
the theory and practice of proof assistants with Lean". Rob will complete the
series of 3 lectures on teaching formal methods at Brown; if interested in the
previous two lectures, please check our website (link below in the PS).

The zoom link for Rob's lecture is https://aboakademi.zoom.us/j/64254430116.

The event will last about an hour.

Warmly welcome!!

Best wishes,
Luigia

PS: the tutorial series webpage is up to date with the list of 2021 and 2022
speakers (and links to (almost all of) the recordings of their talks):
https://fme-teaching.github.io/2021/08/24/tutorial-series-of-the-fme-teaching-committee/.

__
Luigia Petre, Docent, PhD
Faculty of Science and Engineering
Åbo Akademi University, Finland
www.users.abo.fi/lpetre

[Coq-Club] FME Teaching Tutorials series continues on August 26, at 3 pm CEST: Dr. Robert Lewis (Brown University, US) on "Teaching the theory and practice of proof assistants with Lean", Luigia Petre, 08/22/2022