coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Basile Pesin <basile.pesin AT enac.fr>
- To: gdr.gpl AT imag.fr, coq-club AT inria.fr, gdr-ifm AT gdr-ifm.fr
- Subject: [Coq-Club] PhD Offer / Formally Verified Compilation of Interactive Software
- Date: Thu, 22 May 2025 11:46:10 +0200
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=enac.fr; dmarc=pass action=none header.from=enac.fr; dkim=pass header.d=enac.fr; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=c1AQZFo6vQoF7xCVqa4nn5bvUlo9l90t+Q3oh2ejysM=; b=HsmKEHT4ibcms7CumuLagGqU+dIZ0G89UXkDsJJa0xV+ybqSqegz9IP5dsTvO0DqwrSmSOkJlNfqxWSRbX3J38U6+Fe6V1NjkQGVbb8ZXlX19smAdyiuuqeCuEvGTb8GVa/VDAVLy6YFVWmMAtl2sBn6uSb9Ul34Jj2H0B6xZ92NeQMRTWhSqiV5F1SbjhrrKJNPeQdlFGAZBM0TJLIAxzv2iaieFO9t9AO4/kNheURd/9wBDQ1lgFSIQjG+DK427zWDW0ZYWMzKV74FYCr34KtkoBdvGoay65asXKffB9u3ASIAWOaov79i6/5tRawFi8vHiu6dxRSop04f4mWaJg==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=dmRF8eZoIaOVcSjd5mOx5J1HpZnhn6HkQDEK6KJVHb3n/Zk/b2gYWWN5HVdWhdgqQDI7c68sQp6xmDUf2RN2876zKomWqfXCc/B3qyEicrMlqbJLlj0al9twQ1vQ3XRlBaqjSMRmSalzAY8gx+2D1kakh+p74LLHzO7M+vf/84+eHBvFbE/uK9FscbNXWhoALt+MOy3ZNzDYE0bkfkNMslYh+9/BwvzeBbmtA78VIlD6iGoG0W8PuB4zfUMLy7Pqid7wfzA9DILxmSIwHm6lAv8INK9A2MeEm+UlI5TZLZOuqNtsmLCw08jEl1KruntyPBaLSwzehu4SJBwnTAoa6g==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=basile.pesin AT enac.fr; spf=Pass smtp.mailfrom=basile.pesin AT enac.fr; spf=None smtp.helo=postmaster AT imss-1.enac.fr
- Ironport-data: A9a23:FTXlVKiAi5atuSV2qflbWCieX161RxQKZh0ujC45NGQN5FlHY01je htvWWuEbqmKMWT8KdAlYdu0pkgEu8LVndA1S1FqrCk3QXxjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDtJg06/gEk35qmq5WlC5gVWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGUkopFJYm68dLG0ZH6 vo4Iik1bwyEiLfjqF67YrEEasULLczwJ8ZG/HxmxDqfA+xOrZLrGvSXo4UChHFp25EIRqi2i 8kxMVKDaDzKagZOPlpREJ8lneGAi3/2eHtWsjp5oIJtuTOIl1MvjOiF3Nz9f+bJWZ9KnBihg 1n/+H3yXlYGOvet8G/Qmp6rrraTzHKkCN16+KeD3vVtmRiYwnEZIAYHUEOy5/i/kE+3HdxFQ 3H44QIvqLMpsRftQ9/0VFu2uhZooyLwRfIOGPIT8z+c65bOxA+GAEgOVwZAdNsp4ZpeqSMR6 neFmNbgBDpKubKTSG6A+rr8kd9UEXNNRYPlTXReJTbp8+XeTJcPYgXnYOwLLUJYptzwAiq1m HaHqiE1wbsJ5SLq60lZ1Q2d695PjsGUJuLQ2ukxdjj4hu+eTNT6D7FEEXCBsZ59wH+xFzFtR kQslcmE9/wpBpqQjiGLS+hlNOj2u6nVbWeH3A8+RMFJG9GRF5iLI9o4DNZWehwBDyr4UWO4O yc/RCsIvMINYyX6BUOJS9vqVZt0pUQfKTgVfqmIP4sRMscZmP6v5ixobFKdxQjQfLsEz8kC1 WOgWZ/0Vx4yUP03pBLoHbt1+eFwnEgWmziMLa0XOjz8iNJyklbOE+9daDNjr4kRsMu5neki2 40Aa5LWkUsECbGWj+u+2dd7EG3m5EMTXfjew/G7vMbaSua/MDB8U63i0vk6dpZ7nq9YsO7N8 zvvEgVb0VfzzzmPYwmDdnkpOvulUIddvEALG3UmHW+p/Hw/PqepzqMULKUscZcdqedM8P9TT ts+QfumPMhhcDr9xmkiXcHPl7A6LBWPriCSDhWhewk6LsJBRRSW29rKfTnP1SgpDwizv84Qo Zml5BL6QIUCdStmHs35ePKi9HLvnHk/ycZZfVrEHclXQ2roqLNVEi3WiuQmBf0MJTHo5Cqo5 yzPDTg2/eDy8pIIqv/XjqW6nqKVOupZHHsCOVLE7LyzZBLozkD6zaBuCO+3LC3gDkXq86CfZ MJQ/fH2ENsDuH1o64NcMbJa/ZgS1uvVhY1x71pbRS3QTlGRFLlfDGGM3pBPuo1z17Zpg1aKd XzVyOZKG4eiGZ3DK0EQFjoHf+7Y9PAzmxvu19oXDnj+xhdK+OugbR0PETiK0DdQPZlkArMDm O0BgvMb2ya7qxgtM+uFsBxqynSxHiQAfpgj574nA97Nqws0y1t9T4TWJQ3o7bquNdhdEEkYD QWFpajFhoZjm0rzYic2HnnsxstYv4wF4zpR/W8BJnOIu9vLveA21xtv6gYKThxZ4xFE8uBrM E1pChFFHrqP9DJWm8RzZWCgNAVfDhm/+Eaq6V82uEDGbkuvDErhEXYcPLuTwUUn7G5sRDhX0 7WGwmLDUzyxXsXQ3DM3aHF1uc7YUt192Q3Tqv+JR/3fMcEBXgPkpauyaU4jiRjtW5oxjXKag 9haxr97bKmjOBMAp6E+NZKh6o0RbxK5P01Hf+Bq+fIYPGPbeQzq4wO0FWKKRppvKcDJoGiCM O4/AuJUVh+76jSCkSBDO44IPI1PvaAI4PgsR+rVAFAo4pqlkypRkZPP9yLBqnchbPdwnO0cd I7AVTKwPVaBpHlTmmby9dtPKzKoRdw6eTzD+f2H9sQIM7khs+hcV144/ZXpnneSMSphpwm1u iGabYDo7uVS86ZetKqyLbdiXiKaccjSUsaM+yCN6+V+V8vFa5ryhllEu2vZMBRzFppPfdZOz JCmksP9hWHBt5YIC1HpoYGLTfR11J/jTdhsE5zFKVdBlnG/Q+7q2RwI/l64JbFvkN9w4sqGR ROyWPCvdOw6Csts+3lIVxdwSxotKbz7TqPFlxOPq/6hDhs80wueCPiF8XTvT39Qdw5WGpnYJ zL3hc2T5YFjnNwRPCMHOvBoPcYpahurE64rbMb4ujSkH3GlyAHK8KfrkR07ryrHED+YGcL9+ ojIXQX6aA/0gqzT0dVFqMZni3X71pqmbTUYJSrxOuKaigxWyEYHKP8GdMxAB5ddmWr8zvkUo d0LgHQKUU3AsfZsKH0QI+gPmi+SAOUFfNnjTtDs113BcD+4XetsH5M4nhqNIB5Klv/LweeuI pcQ4BUc+/R3Lo5BHY4u2xBwvQurKj42CJ7FFYARXvEe2yojPIg=
- Ironport-hdrordr: A9a23:GMmGo6mvOoP0vHJB+5ksRUp1HyLpDfNhiWdD5ihNYBxZY6Wkfp +V88jzhCWZtN9OYhwdcLC7WZVoMkmsjaKdhrNhR4tKPTOWw1dASbsN0WKM+UyEJ8STzJ876U 4CSdkDNDSTNykZsS+S2mDReLxBsbq6GcuT9IHjJhlWPHhXgu1bnmNE4lHxKDwKeOAKP+tMKL Osou584xawc3Ueacq2QlEDQuj4vtXO0L72fBIcABYjyQ+WyRel8qTzHRS01goXF2on+8ZrzU H11yjCoomzufCyzRHRk0fV8pRtgdPkjvdTGcCWjcARCzP0ziKlfp5oVbGutC085Muv9FEput /RpApIBbU711rhOkWO5Tf90Qjp1zgjr1fk1F+jmHPm5ej0XigzBcZtjZ9QNkKx0TtXgPhMlI Zwm06JvZteCh3N2Az7+tjzThlv0m65u2Arn+I/h2FWFaEedLhSh4oC+149KuZ2IAvKrKQcVM V+BsDV4/hbNXuccnDip2FqhOehW3widy32MXQqi4iw6Xx7jXp5x0wXyIg0hXEb7q8wTJFC+q DtLrlovKsmdL5bUYtNQMM6BeenAG3ERhzBdEiIJ078Ka0BM3XR77bq/bQO4v2wcpBg9up+pH 34aiIXiYcOQTOuNSXXt6c7siwlAV/NFwgF8/suqKSQ4dbHNfnW2S7qciFfryLvmYRcPiThYY fDBHtnOY6dEYLQI/c24+TfYeghFZBMarxhhj98YSPEnv72
- Ironport-phdr: A9a23:c4NuIBEnmbKGe/SLHTF9Mp1GfxxGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k21xmRBc6GtagMy7KP9fy7AypYudfJmUtBWaIPfidGs/lepxYnDs+BBB+zB9/RRAt+I v5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vI BmsogjcuMcbjZF+JqotxRfEonpFd/pLzm9sOV6fggzw68i+8ZJ96Shcp+4t+8tdWqjmYqo0S qBVAzshP20p/sPnsgXNQxWS7XUGSGUWlRRIAwnB7B7kW5r6rzX3uOlg1iSEJMP6Vb87Vyis4 KdtUx/olTwINyUl/2HNi8x/l7xUrRS8rBFi2YHUYYWVNP1jfqPBeN4RWGRMUtpNWyFHH4ixa ZYEAegcMuZCt4TzpFUAohW+CwexGu3g1jBGiXDt0K0m0OksCx3K0BA+E98MtnnfsdX7NL0VU eCw1KTF0C/Mb+hX2Tf59ofDbwovru+XXbJxd8ra1E4iGBjfgVWLqIzlOy2a2v4Vs2eF9OpgV OSvhnU5pAF3uDeg2t0giofTho8MzF3P6Cp2zpovK9KiVE57fcCrEIFWtyyCKYZ7TMEvT310t Ssm1LAKpJC2cTUKxZkj2hPTdvyJfoeL7x//W+ucPyl1iXBhdb+wiBu/8EetxvDyW8Wq0FhEr ixImcTCuHAK0hzc8MmHSv1l80i/3zaAzRzc5vtKIUAuk6fQNp0vwqYom5YOtUnOHjX6lFvog KOKbEko5+il5uD9brjop5KQL5F4hwDiPqkgn8GzHPg0PRIPUmWe5OiwyKPv8EjkTLpRgfA7l 6zUvZPcKM8GuKO5BxJV0p0/6xmhFTeozdUYnHgZI19dZB6KiZXiNUvUL/DiF/i/hkyhkDd1y PDCOb3sGpTNLn3YkLf6ZLpx9lRQxxQ1zd9F+51YEL8BIOjrVk/wstzXEAM5PhSpz+vjCNhxz J0SVXyTDqODLa/fsVuF6vghLuSNfIMVvSzyK/kh5/7gl385nlodcLGy0pQNc3C4H/BmLFuDb Xr0nNgBCmYKvgwlQeP0jl2NSyJca2y8X6Im/j07DpmpAp/ZRo+xmLyBwDu7HppOa2xbElyMC 2vnd52YW/cQbyKfOtNukjsdVbS4V4Ah0QyuuxThxrp8LuvU/zUYuoj52Nh04e3TjxAy+iZuA 8STyWHeB11zy2wEXXk5xKRXoEl0xRGNy+wwiPtBUNdX+vlhUwEgNJeawfY+Q9/+QEfAcNKhR 1q8B9SoBHc/VIEf2dgLNmx0ANSmg1j70jGrBfdBnbWQBZg5tLrRxHn3D8t7wn2A2rN33Apue ddGKWDz3v03zAPUHYOcyy1x9o6vfKUYhmvW8XubiHCJtwdeWRJxVqPMWTYeYFHXpJL3/BCKV KegXJIgNAYJ0sueMu1ScNS8h1xdRfPufszTeGO3s2q2DB3OyKnfJJHydTAl1T7GQFMBjxhV+ H+HMQYkASL0qWvFDThjU0rieELq2eR4oXj9QFVnhxqSYRhH0Ly4sgUQmeTaS/4X2eccvzw9r jxvAFun99PTEMHF/kxseqxXJ90niLte/UTesQE1fpmpLqQ4w0UbbxwypUTlkRN+FoRHl8Eu6 nIs1gt7b6yCghtHcHuD0Jb8N6eySCG69Q2za6PQxlDV0cqHsqYJ5vMirlz/vQavXkM8+nRj2 tNR3jOS/JLPRAYVVJvwVA4w+X0Y7/nQazI8446SzXB3MK+cvznL0JQnHqptyxqtecteLLLRD BX7QIURA8mjLvBvmkD8N0NZeroIrOhtYpLgLKXVvczjdPxtlz+nk2ldtYV000bWsjF5VvaNx ZEOhfeRwgqAUT74ylanqMH+345eNlRwViKyzzbpAIlJa+h8Z4EOXC2kKta2wtg4n5P2Wnhw+ ViqDBUIwoX6HHjaJ0y4xgBW2UkN9DatkDC5yzEyizwyr6y30SrHyKLsblBUXwwDDHknhlDqL 4+uitkcV0X9dAklmiyu4kPizrRarqByR4XKaX9BZDO+b2RrU6/q86GHf9YK8pQj9yNeTOW7Z 1meDL/7uRoTlS35TSNSwzUydjfivZuc/VQygmuGLXJ+6mLUYsB27RrZ7deaS+QZ0jcdRSZ+g CXaHRDlboTvp4/M0c6e46blCSqoTdVLfDPuzJ+cuSfehyUiGhC5k/2p25XmHQU8zS7nxoxvX CTMogz7Z9qj3KC7POR7O0hwUQattowgQNk4y9ZhwspOih14zt2P8HEKkHn+K4Be0KP6Nj8WQ CIThsTS607j0VFiKXSAw8T4UG+cy41vfYrfACte1yQj4sRNEKrR4qZDmH4/qFOjrAbcJ+Bwh TYb4fYo4XVcjftD629Phm2NR6sfG0VVJ3mmnR2T7tSz6r1af2epWbW23UE4k8rrX9Tg6klMH X3+fJklByp56M5yZUnN3HPE4YbhYNDMbNgXu07cg1LaguNSMp50iusSiH8tJzfmpXN8gb1e7 1QmzdSgsYOAMWko4K+pHksSKGjuf81KsjD10fQHz5vQhdr3WMw8S3NQAtPpVa76SWNP8669b 0DXTWx68ynFfNiXVQ6HtBU//i+JScrzcSjKdT9InZ1jXEXPfR0CxlpOBHNjw89/R1HixdS9I h4lvXZItwC+80AUjLgwbnydGi/evFv6M2tvDsHOclwPtVkEvhaEeYmX6uY5d81B1rumqgHFa mmSZgASSHoMRlTBHVfoeL+n+djH9eGcQOu4NfrHJ7uU+6RYUL+TyJSj35EDnX7EP9iTPnRkE /ww21ZSFXF/FcPDnjwTSisR3yvTZs+frR2492V5tMe6uPjsXQvu48OIBd4weZ13/AuqhK6YK +OKrCd8Mi0dj9UBw3bDjrYFnRYThyxoazixAOEAuCrKH8ey0udcCx8WbT82NdMdtvNhmFMXY YiC14KzjeAr65x9Q01IXlHghMyzMMkDImXncUjCGF7OLrONYzvC38DwZ6q4D7xWluRd8ROq6 lP5WwfuOCqOkz7xWlWhK+ZJ2WuRNQdfvIz7aht2CG7LQdTvYVu1KpUk6F9+ia1xnX7MOWMGZ HJkdFhRq7SL8S5CqvR6AHcEtzxoK+CP3SiDpbq9SN5eob5gBSJ6kPhf6XIxxu5O7S1Kc/dyn TPbst9kp1zOeganxzxuW1xAsGQS7GpulUhkMK6f+IMSAR4sHToM6H6LTk1Mqt1sAZvhofIIo uU=
- Ironport-sdr: 682ef267_K2K8/xIcC/nY6jdWgWu5Pt/O77J2HXJFbdqAQ7vUZeOHGaj gKfpHv0QPB2w13OMBIPzF+LGjAwRRqIqyJRmu4A==
[English version below]
Bonjour,
Nous cherchons un candidat pour une thèse autour de la compilation vérifiée d'un langage pour la programmation de programmes interactifs (Smala) dans l'assistant de preuve Rocq. La thèse se déroulera dans l'équipe LII de l’École Nationale de l'Aviation Civile, à Toulouse. Le sujet détaillé est accessible ici:
https://cloud.recherche.enac.fr/index.php/s/3W6SNLX4QKr6idf
Pour plus d'information, contacter basile.pesin AT enac.fr, stephane.conversy AT enac.fr et celia.picard AT enac.fr. N'hésitez pas à diffuser largement cette offre autour de vous.
La date limite pour les demandes de bourse état très proche, la date limite de candidature est fixée au 26 mai.
Cordialement,
Basile Pesin
============================================================================================
Dear all,
We are currently looking for a candidate for a thesis on verified compilation of a programming language for interactive programs (Smala) in the Rocq prover. The thesis will occur in the LII team at École Nationale de l'Aviation Civile, in Toulouse. The detailed subject is linked below.
https://cloud.recherche.enac.fr/index.php/s/3W6SNLX4QKr6idf
For more information, please contact basile.pesin AT enac.fr, stephane.conversy AT enac.fr et celia.picard AT enac.fr. Don't hesitate to disseminate.
The deadline for PhD grants being quite short, the deadline for application is the 26th of May.
Best regards,
Basile Pesin
- [Coq-Club] PhD Offer / Formally Verified Compilation of Interactive Software, Basile Pesin, 05/22/2025
Archive powered by MHonArc 2.6.19+.