coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] FM Teaching Tutorial on March 31, 3 pm CEST --> Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming

From: Luigia Petre <Luigia.Petre AT abo.fi>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] FM Teaching Tutorial on March 31, 3 pm CEST --> Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming
Date: Fri, 24 Mar 2023 21:36:45 +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 7E226110D9A4
Ironport-data: A9a23:vBwuwqoFWJYcc5xarlrE5n/fI7heBmIBYRIvgKrLsJaIsI4StFCzt garIBmEOvbZZTbwf4giaYS1800OvpXXydFhQAZt+39mQ39G9OPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKiefHoZqTZMEE8JkQhkl/MynrlmiN24BxLlk d7pqqUzAnf8s9JPGj9SuvLrRC9H5qyo42tD5ABmP5ingXeH/5UrJMJHTU2OByCgKmVkNrbSb /rOyri/4lTY838FYj9yuuuTnuUiG9Y+DCDW4pZkc/DKbitq+kTe5p0G2M80Mi+7vdkmc+dZk 72hvbToIesg0zaldO41C3G0GAkmVUFKFSOuzdFSfqV/wmWfG0YAzcmCA2l1DbMy3Ll6GF1e2 vs5BAwwfyre3qGPlefTpulE3qzPLeHwOZ8H/3Z90XfQB/FgT5Grr6fivIQAmm1r3IYURKyYO pJxhTlHNHwsZzVrJ1YYCZt4pOq0nHTXejdf7lyUzUYyyzWKlV0qgOe1WDbTUsSUZ/t1uEXGn F/p+FX0Hw9GGPCW4yXQpxpAgceUx3+jBt1JfFGizdZhh0TWzWgOAjUNRF6jqL+4jFS/UpRRM SQpFjEGtq0u7AmsU8W7Vhe/5nCF1vIBZzZOO64K1iurlafN3xa2AUkocgNQUoF/9/ZjEFTGy WS1t9/uADVutpicRnSc6qqYoFuO1c49djRqicgsFlZt3jXznG0gpkyXEosyQcZZmvWvQ2qpm mDiQD0W2t0uYdg3O7KT03Gvb9iEmoXTTRNdCu7/BDr4slsRiGKNXIu19VjE4O1cZKiYSF2Iu nRspiRzxPsLEYnIkzGRBuwHG/en5p5p0QEwY3YxRfHNFBz0pRZPmLy8BhklfS+F1e5fIlfUj Lf741852XOqFCLCgVVLS4ywEd826qPrCM7oUPvZBvIXPMcgKl/do3oyPxPBt4wIrKTKufxlU Xt8WZr9ZUv29Yw7klJaus9Die50l3lWKZ37Gs6qp/hY7VZuTCXPFe9bbwDmghER8KKJvAjY9 Z5DNsaWzAlSU+v/Yyre98YQIEsJMGNzAoGeliCkXrPrH+aSI0l4U6W56ep4I+RNxv0F/s+Vo C3VchIGmTLX2yebQS3UMSoLQO20Av5CQYcTYHZE0aCAgSZzOO5CLc43KvMKQFXQ3LM9lqEuH 6FcIa1twJ1nE1z6xtjUVrGlxKQKSfhhrVvm0/ONMGRhLa1zDRfE4MHldQbJ/SwDRHj//8gnr rHqkkuRTZMfTk4wRIzbedC+/WOX5HI9oeNVW1eXA99xfE63zpNmBRashdAKIuYNCy75+B2k6 yisDyw1n9L9+70OzIGRhISvjZuYLO9lL08LQ0jZ9emXMAfZzEqCwKhBcua5eGDAZmb3+YGJR +Zc/9fjOtIpwXdItItdFe5w7KQcvtHAmZ5T/j5GLl7qMWvyUqhBJFuC1ulx7px9/KdT41aKa xje6+tkNqWsE+K7NlwofS4OTPmJjNMQkRnstcUFGl3wvnJLzeDWQHdpHke+jQJGJ+FIK6Ij+ +AqvfAW5yGZihYHNtWnjDhex1+TL04vArkWiZUHPLDF0gYb6ElOQZj5OB/E5Juib9ZtME5zL ASE24vEpbBXnXTZf1QJSHPi4Ot6hLY1gi5s8mMsHVqzp4f6tqcF5yEJqTUTZSZJ/ypDyNN2a zRKNVUqBKCg/AVIpclkXkKsKgQRGS+c+U3V4HkKnV3/UEOHeDHsLmo8GODV52Ef0TtWUQZ69 YGi6lTOcGjVJZnq/y0QXUVFlaTSfeZp/FefpPH9TtW3IZYqRBHE3ImsXDMsgDn6C5oTgEbnm 7FbzNxoY/emCR9K8rwJMKjE57E+UxveGXdjR8tm96Y3HW3xXjG+9DyNCkKpcPN2OP343h6kO vNqO/5weUyy5ASWohAfIJw8Ebt+sfoqxdgFI73QNTEntZmbpWFXq57+zHX1q1IqZNRMqvwDD L3tWQiMKUGuoEdFunTsqZBEM1WoYNNfawzb2vu0wdozFJkCkb9Nd2cu3pudo3/ODlND+jyVt hKeYqbt7vdDzL50lNDGCZRzBASTKPLyWt+X8Qu1jc98UNPXPerKtCIXslPCLS0MDYAOWt9yq 6uBgOT30GzBorwydWLTwLuFKIVk+uSwW7BxHv/sDXwHgxaHZtDg0yED90+8N5ZNttFXveujZ gmgbfqPZcwnYMhcyFJVehphPU4kUYqvVZjZpAS5s/ioIToe21aeLNqYqFnYXVsCfSoMY5DDG gv4vsi13e9hraNOOk40N6kzSdswalruQrAveNDNpCGVRDvgyE+Lvrz50wEs83fXA32DC9z3+ o/BWgO4ThmppaXU15tMhuSeZPHM4KpV2oHcv37x+uKaTxihCXIeaOMALdMPAJYSnC2aOFQUo t3SRDNKNMk/dW0sndbADBDLVw2YQOIPUjs8DiJ85FuaMk9aG6vZaIaMNU5cD7NeczHkiu+mQ T3bFrscITDpqqxUqS0vCjBXTAupKj42Bp7FxKwlr/HPPg==
Ironport-hdrordr: A9a23:4SzfWKtdkggdPthgC2HJ0ULB7skDWNV00zEX/kB9WHVpm5Sj5r mTdYcgpGfJYVcqKQ0dcbLpAsO9qBbnmKKdjrNhWotKMDOHhILKFvAc0WKB+UyHJ8SWzIc0vs sOHclD4bbLfDpHZLPBkW2F+qEbsby6Gc6T9ITjJjxWPHpXgulbnn1E4yigYzBLeDU=
Ironport-phdr: A9a23:RznmzBeEvEuRWBi/9AXFZlOJlGM+rtTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWUG9+Htbkd1rKempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjqwbalsI Bi5rAjdudQajIt+Jq0s1hbHv3xEdvhZym9vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2T qFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4 qx2RhLklDsLOjgk+27Ql8JwkblboAq/qBNj347aboaVNP9kcaPce9MRWG5NU8lVWiBEBI63c okBAPcbPetAr4fzuUYArQewCwevBePg1jBHi2Ts0qEm0eQsCx3K0BAgEt8IrX/arM/1NKAXU e2tyqfI0DTDb/xX2Tjn9YPGaA4uoe2WXb1ubMHczk8hFx7EjlWfqIzqJSmZ2P4TvGiH9epvS /mihHQ8pAF2uDSvyMYsh5DPi4kIxV/K6T93z5wpJd2kVkF7e9ikHYNeui+UNYZ7Q8cvTm52t Sg11LALu4K2cTYWxZg62xPSd+GKfpaV7h7/VuucPzZ1iGxldb++mxu/8kiux+/8WMS71ltBs yRLkt7Jtn8X1hzT7NCKSv5h8UekwzmPzBzT5f9eIUwuiaXUMYYtw783lpoUtETPBDL2mF7ug K+Zd0Uk5uio6/n8bbn8p5+cMJd4hRvlPaQpgMC/D+U4Pw4TVGaY4eSxzKDv8EPlTLlQkPE7n LfVvIrEKcgGuKK1GQ9Y3po75xqiATqqzM4UkWcJIV5bYh6LkonkNl/ULP32DPqzm0mgnTl3y /zcILHsDIvBImLenLrjf7tx8UFRxBY1wNtC/ZxbEKsBL+j2WkLptNzXEBs5Mwuszub8DdV9y pseVXuIAq+ELKPeq0WH6fkoI+WWao8VuS7xK/kj5/HwkX80gUIRcKe10ZcNdny1EOpqL1+Hb XbxnNsNC2cHshYmQOzvklKCUDpTZ3ioX6I74zE2EISoDZrCRoCigbyOxj23EIdIaWBaEFCDD 2zleJ+fVPcLci6SLM5hniQCVbe6U4Ahzw2htBfmy7p7KerZ4jAUuYr51Ndp/+3TiQ0y9TtsA suB1GGNVnh4kX8MRz8rx69yuld9y1eG0ahgmfNUD91T5/VTUgc7L5HQ1eJ6C8qhEj7GK52CT 0/jSdG7CxkwSMgwypkAeQw1T96ll1XI2zegK74Tjb2CQpIupPHyxX/0cuJgynnH3eEZgkU8T 4MbEXCnia92sTDeG5TEu0yTkOCkdPJPj2b26G6fwD/W7wljWwlqXPCZDBj3B2PTpNX9vQbZS qO2TK8gKk1HwNKDLa1Dbpvoi09HTbHtIoeWeHq/zkG3AxvA3baQdMzyYWxI+DjcB0kN1Tge4 WyLHQE0AWGvojGWFyRgQGrmeFik6uxisDW+R04wwRuNahhFyru6+xdTvfGAUf4717gD/ikg+ H1vBFjo+dXQBpKbohZ5OqVRZdRo+FBcyWfQrBBwJLS7Krx6w1kDb0J+tUSo2RQf5pxot88so TtqyQNzLfndy1Zdb3aD2oi2PLTLK2709RTpaqjM21iY3szEsqEIoO81rVnupmTLXgIr7mln3 t9J0nCd+oSCDQwcVoj0W1o28B4yrq/TYy007YfZnXN2Nqz8vjjH0tMvTOwrr3ToN/NCMayFH UnKHtEACuCnIutslVnoJhMIMeZO9bIlatu8fqjO06qqMeB82TO+2D0cuMYniRjKrXMmDLOQj PNni7mC0wCKVinxlgKku8HzwsVfYC0KW3G40W7iDZJQYat7ecAKD32vKou53IYb5dalVnhG+ VqkH15D1tWufE/YS0H80gxZk3wavWaqsSKyyHp6knt6y8jXlDyL2OnkeBcdbyRvWWhtjF6qG YWold0yVUKvKQYo3kjt9QPxwK5Vo756Jm/YTBJTfiT4GGplV7O5qruIZ8MnBIoAiSxMS6z8Z FmbTuW4uB4Gy2b4GHMYwjkndjass5G/nhpgiWvbImwh5HbefMhxw1/Y6rm+DbZ1wzsJRSA+s TTLHFWUNtOuu9uV35vOqeGxUWu9W4YbKHKzi9nb7m3hvDcsXEX3luv7gtD9FAkmzSL3srsiH T7FqhrxeMij1qi3N/5mYlg9AVb978RgHYQt2oA0hZwWxT0bnsDMpiJByzypd48Cg+SjNCloJ 3ZD2dPe7Qn71Vc2K3uIw9m8TXCB2o56YMH8ZGoK2yU75sQMCaGO7bUCkzEmxzjw5Q/Xf/V5m S8QjPU073tPycUUuQUsx2OlD6wIEGFRNyuqmRXCvLXc5O1HIX2id7S9zh80uc2gA7CL5DlRR Gz0Up4oGml+748sVTCEmG224Ybidt7KaNsVvRDBiBbMgd9eL5cpn+YLjy5qairt+GcowOkhg VlyzIm36cKZfn518vvzUXs6fnXlItke8Tb3geNCk9aKisqxS455FGxDXYO0H6vzSHRI7q6hb V/VVmRm8j+aAeaNRFTHrh099TSVSsrtainyRjFRxIdnSBDYI1FDxgwdQDwxk5glGxrsys2pc UFy4i0d6wzPsQNCjO9tPhj7X33e4gmpD1V8AJmZJx5L4gwQ/F/bd8mX6O5pHiVc94W56geKL ySaf1gaXDxPAxPZQQm6Zf/3tYCIpOGcAqDWw+LmR7KIpKQeUv6JwcnqyY5653OXMd3JOHB+D vo9004FXHZjGs2flS9dAyoQ3znAacKWvnLesmV+s9y//fL3WQnu+ZrHCr1cNs9q8gy3hqHLP vCZhSJwIzJVnp0WwnqAxL8a1V8UwyZgElvlWawHrjLIRbnMl7V/FBsHc2Z0KdcO5qg7mAdMe Ibaht7zyr9kn6s1BlNCBjmD0omiYc0HJX34NUuSXR3Tcu7df3uRmpuxPPvvLN8YxP9ZvBCxp zuBRkrqPzDY0iLsSwjqKuZUyieSIB1Zvoi5NBdrE2nqCtz8OXjZeJd6iyM7xbosizbEL2kZZ HJYbkJCr7TW1S5EmPhXEmZGqHRkZ7rh+W7R/6zDJ5AavOE+SDxzjP5f6W8mxqF99yRYXLlyh TeUp9Rp5V+n2LrqqHIvQF9FrTBFg5iOtENpNPDC95VObn3D+QoE8WSaDxliTz5NA9fo/a5Rm ICnfE3bIT1FtdzVr5J07yn8M8ebKD8mLAavETTTSgUEH2bDCA==
Ironport-sdr: 641e17f1_wOgV99FmnL8jzT8APaH8ja+fa5o/m1+IO7y2PvAbRMJpI1S IpLxOof2cZy450jnVBBm+XrsYtlOjB5+WmhQBzA==

Dear all,

The Formal Methods Teaching tutorials series resumes in 2023 with a lecture on Friday, March 31!

Prof. Emil Sekerinski (McMaster University, Canada) will lecture on Teaching Concurrent Programming on Friday, March 31, 2023 at 3 pm CEST. An abstract for his talk comes below:

The education in programming has in a certain sense deteriorated since the 80’s and 90’s: programming languages and environments, as common in industry and to which students are exposed in Computer Science, Software Engineering,
and related programs, have become complex. Mastering them consumes students to an extent that courses cannot decouple the (timeless) principles of programming from the (short-lived) specifics of the programming environments
at hand; the mathematical background on program design is often not taught. This is particularly critical for concurrent programming, which has become increasingly relevant but cannot be mastered without a theoretical background. The author has been developing course material for a required 3rd year Software Engineering course at McMaster University, Concurrent System Design with around 170 students, since 2018 to address that issue by web-based interactive notebooks using Jupyter that combine explanations, the mathematical theory, and execution of programs directly in the notebooks.
Correctness reasoning, including non-interference of processes, is explained through hierarchical state diagrams. This talk gives an overview of the course material, which is available as an open educational resource, and reports on
the experience.

More information about our lecturer can be found here:
http://www.cas.mcmaster.ca/~emil/.

The zoom link for Emil' 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 below; we have speakers planned until June!
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] FM Teaching Tutorial on March 31, 3 pm CEST --> Prof Emil Sekerinski (McMaster University, Canada): Teaching Concurrent Programming, Luigia Petre, 03/24/2023