coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrei Popescu <andrei.h.popescu AT gmail.com>
- To: cl-isabelle-users AT lists.cam.ac.uk, coq-club AT inria.fr, agda AT lists.chalmers.se, lean-user AT googlegroups.com, hol-info AT lists.sourceforge.net, acl2 AT utlists.utexas.edu
- Cc: Andrei Popescu <a.popescu AT sheffield.ac.uk>
- Subject: Re: [Coq-Club] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024
- Date: Mon, 8 Jan 2024 12:46:44 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andrei.h.popescu AT gmail.com; spf=Pass smtp.mailfrom=andrei.h.popescu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f46.google.com
- Ironport-data: A9a23:9WSICqOurZsxQyrvrR1vksFynXyQoLVcMsEvi/4bfWQNrUokgzZUy mEfXWmFb6yNMWv2c9p/PN7j8UlTu5CAyoBmGXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYAPNNwJcaDpOt/ra8EM35ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGX8bnXV/NtcIH0bINEXweRKOWFU0 +QhfWVlghCr34pawZq+Q+how8kvdYzlYN1ZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JgeW6qAD yYaQWIHgBDoahtDIFoWTpJ4hOCwi2L0bhVXrVuUoew85G27IAlZieSwa4uEIYbULSlTthzbl GLX3W70ORtAatmO1BOKqS/9vsaayEsXX6pXTtVU7MVCi1qKg2cXFRc+Tkq+ufD/i0ikWtsZJ VZ8x8Y1ha079UjuQ9WkGhPk/jiLuRkTX9cWGOo/gO2Q9pfpD8+iLjBsZlZ8hBYO7afanBRzj gXXzeD6TydiqqOUQn+7/7KZ52H6cysMIGNIIWdOQQIZ6pOx6Ms+nzDefOZFSaSVt9zSHS2v4 jaoqCNlua4fo/RW3IqG/HfGoQmWmL73ciAP6D76YEeZ/yJiRYv8Z4WX+VnRtvlBC4CCT2i+h nsPmunAzeVXDZiyizC/f9wdOI6Yv9CEbTvW2w9pFbYc6gX3qmKCfJ9R0h56NkxGIsYJQh63Q U7x6Cd6xo5fA2uuVoBzO7mOMsUNybPyMPjUTdXWU4Z+WYdwfwq54y1eX06c8GTzmkwKk6tkG 5OkXeuzLHQdU4JL8SGXQroD7LoV2SwO/2PfapTlxRCB07DFRnq0S68AAWSefNIC86KIjwXEw elxb/LQ5U1kb9T/RS3L/ao4D1MAdyE7DK+rjf1nTLeIJw4+FVwxD/PU/6gaRLVkuKZojcbNw GC2Xx5J6Vj4hECfEz6wVFJYVOrNU6p8/FUBBg59GXaz2nMmX5Sj07dHSbszYosc1bJCydxac qA7XvuuU9V1ZBbJwTA/VaXGjZdDcU2rjD2ePiD+bzkYeYVhdjPz+dTlX1XO8SUSPxWzru87h aOq7SLAYJ85Xw85Jt3nWPGu6FKQvHYmh+N5WXXTEORTYEnB9ItLKTT7q/0Kf+UgDArl/STD8 Sq7GjIaqvvpj65v1eLWlIaWq4uNOMlvLHpwRmX0w+6/CnjHwzCF34RFbtetQRncc2HRo4CJe uRfyqDHAs0txVplndJ1LOd28PgY+dDqmr59yzZkFlXta3CAKOtpAluC7Pl1mpx9/J1rkiroZ RvX4fhfA6uDB+39Gl1IJAYFUPWK5ctJphbst8YKMGfIzw4p2oGYUHdiHQiG0w1cC7pXDLkL4 8kcvOwu1gjurSZyb/iniHhP+nWuP04wdfwtlqsnDb/BjispzVB/YqLgNBLm3aHXVfJyNhgFH zzFoovDmLVW+WTaeVURC3Xm/LRQlLYOij9w3X4AIFW7wIPFj8AowSwLoCgWTxtU/DpDwelcK mhmDGwrBKSsrhNDptlPYHCoIC5FXCamw03Wz0AYslHWVGy6fzXpAFBlHN2S7Wc11nl5fAlL2 J25k0HbCS3LeuP11QsMAX9VkeTpF4FNx1eTifKZENSgNLhkRCjunYuFR3cC8jnjCuMP3Hz3n /FgprtMWPeqJBwrgvMJDqeB3u4tUzGCHmtJRM9h8I4vHW3xfDKT2yCEG3uue/FiduD7zkulN /NAfs5/dQyy9CKrnAApAaQhJ7xVnvlwwPEgfrjtB3ANsprBjz5Pna/TyBPDhz4Qc40zqfo+F 4LfSWvTWCjYz35ZgHTEo8R4K3K1K4tMLhH12Oeutv4FDdQfueVrals/yaawo27TCgZ84haIp 0nWUsc6FQC5JVhExOMA05mvBjlY7fv2XeWMtQ2/6pFAMY2JPsDJuAcY7FLgOmy6+FfXt8tfz dywXBzfhSspf4ral0jWnpCAE+9C4sDasC9/LJfsNHcD9cedcJaE3vbAklxU7bRGldpc4o+sQ A7QhA5cszIKc481+UC5oBSy3/rQ52obo0sgSe6AQyywNyUg
- Ironport-hdrordr: A9a23:9VknEa3GJiv8Vu/75/F1iQqjBVVyeYIsimQD101hICG9Lfb0qy n+pp4mPEHP4wr5AEtQ/+xoS5PwOE80lKQFlrX5WI3PYOCIghrNEGgP1+rfKl7balvDH4xmpM BdmsFFYbWeY2SS5vyKgzVQZuxQpeVvh5rY59s2oU0McShaL4VbqytpAAeSFUN7ACNcA4AiKZ aa7s1b4xK9ZHU+dK2AdzE4dtmGg+eOuIPtYBYACRJiwhKJlymU5LnzFAXd9gsCUglI3awp/Q H+4kfED+SYwruGIy3npiPuBqdt6ZTcIxx4dYKxY/0uW3jRY8CTFcVcsvO5zXAISaqUmS4XeZ H30mwd1oJImjrslyiO0GHQ8hil3zA053D4z1iExXPlvMziXTo/T9FMnIRDb3LimjgdVfxHod J2NliixulqJAKFmD6468nDVhlsmEbxqX0+kfQLh3gaVYcFcrdeoYEW4UsQSf47bVbHwZFiFP MrANDX5f5Qf1/fZ3fFvnN3yNjpWngoBB+JTkULp8TQ2TlLm3JyyVce2aUk7wI93YN4T4MB6/ XPM6xumr0LRsgKbbhlDONEWsezAnyle2O8DItTGyWYKEgqAQOzl3es2sRJ2AiDQu118KcP
- Ironport-phdr: A9a23:C9frTBGg4ykyc5MFlUa1R51Gf9lFhN3EVzX9CrIZgr5DOp6u447ld BSGo6k33BmTANqQt6gMotGVmp6jcFRD26rJiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjmwbalsI Bi2rwjducYbjZV/Iast1xXFpWdFdOtRyW50P1yfmAry6Nmt95B56SRQvPwh989EUarkeqkzU KJVAjc7PW0r/cPnrRbMQxeB6XsaSWUWjwFHAxPZ4xHgX5f+qTX1u+xg0ySHJ8L2TLQ0WTO/7 6d3TRLjlSkKOyIl/GzRl8d9ir9QrhC8qBxl24Pbb4+VO/h+cK3Tft0UWHRPU9hNWCJOGY68c 5IPAvAdMepEs4XwpV0Dpga+Cwm2A+PvzydFi2Pw3aInyeQuDwDG1xE6EdIJqHTbss71O7sPU euoy6TH1zPDYO5M2Tjj6YjEaBAhreuUXbJ3acre11IvGB/YjliLpozlOima1uUJs2SB8+VgU uevhnchpgpsrTeh2t0ihZPVhoIJ1F/E7yN5zZ4pKNCkSkN3fdCpHIdQuSyeNYZ7Qs0sTm9nt iomzrALu4C2cTYUxJopxRPRZPKKfpaI7BzjVeucIil1iW95db+wgRu57Eauyur5Vsau0VZKq DJIncLQuXAWzRDT7dKHSvRl8ki9wzmP0hrf5ftYLkwuiKrbKIYtwro1lpoIq0jMBDP5lF/rj K+VcEgv5+um6/z/b7n4upORM5V4hwL+P6g0hMCzHec1PhIBUmWa/+m3yaPu/UnkQLVRkv05j LPZvo3bJcUauKG0GxNZ34A+4BilFTimys4XnXwfIVJFZh2Hi4/pNknLIP/iDPe/h02gnyl2y PzbJ7HhDJrAI3nZnLfuerZ97EFcyA4twtxF+51UDbQBLOryWk/3qtPYEgc0PxKoz+vjEtlw1 YMTVXiRDqOFM67eq1CF6+M3L+mJfoAVuTL9K/Y/5/7piH80gUUSfa+00psNdn+4H+5qI0WDb Xr0hdcBCXkFvhEiQ+z3k1CCXjtTaGyzX6I4/D00FIWmDYLbSoCrm7OOxD27EYFOZmBaFlCMF m/le5icV/cWdC2SOtNhkiADVbW5V4Ah0giuuBbmxLpjM+rb4TYVtYnj1dhw/+3cjws+9T1yD 8SH0mGCVXt4nm0SR2x+4Kcqqkg4y0yK26V8h/EdCMde/ehhVgYhKYWaxOV/Tdn5HB/COp+CT 0/jSdG7CxkwSMgwypkAeQI1EtquhzjH3jG2GPkel7WPAZEu6eTH0jy5I8t0zTPbz6Q7p1YhR cRLOGK8gbNn7E7YAIuN20Wek+Orc6ob9CrM73uYi3GJoVtTXQB3S6rIG3YSeg+epN/9vGvfU 7uvEqg8dBZdxN6LMe1HZsC6o09BQaLKPtjEbmP5o2CoCA2D2/vYZYzmYWgcmiWbEE8cnhsY4 F6JMAE/AmGqpGeIX28mLk7mf065qbo2k3i8VEJhl2liDmVk3ruxoFsOgOCEDukU1fQCsTsgr DN9GBC82cjXApyOvVkpZ71SNPU65loPzmfFr0plJJX1JqZunFMfNQQxp0T22g58F61PlMErq DUhyw8hYbmA3gZ5fiiDlYv1JqWRL2Dz+B61bKuD01fSytuXvKdJ8PMgpk7ooSmmE0Mj9zNs1 NwGm2CE6MDsCwwfGYn0Tl5x9xV+oOTCZTIh4orPyXB2Gay9szuH1t5wQeV5lFCveNBQNK7CH wj3eyEDL+6pLuFi212gbxZeeftX6LZxJcStMf2PxK+sOu9k2jOgl2VOpo5ngAqK8GJnR+jE0 oxgobnQ1xabVzr6kFaqs9zm0YFCazYIG2OjyC/iTIdPb6x2dIwPBC+gOcqyjtl5gpfsXTZf+ jvBTxsP3sOzdBvUbxrl2hVdzk8KiXOikCq8iTdzlnBhr6aS2jDP3/W3bAAOaQspDCFpiVbhJ 5TxjshPBhD5KVh00kH9tQCmmfs+xuw3NWTYTEZWcjKjKmhjVvH1rb+ee4tV75hutyxLUeO6a FTcS7jnohJc3TmwegkWjD09aTyuvY302hJgj2fIZn91oGDUeIdwgw/Y/NHHTuN50T8PRS0+g j7STAvZXZHh7ZCPmpHPv/rrHWunWodecG/ri5uHrCag7nBCDhi2nvT1kdriW1tfs2ezx5xhU iPGqwz5a4/g2vGhMO5pSUJvAUf198twHowWfpIYvJgLwjBag5yU+SBCimLvKZBB3qm4anMRR DkNytqT4Q7/2UQlIGjbj47+U3ycxINmabzYKisf3C4n4sEMCOGM66RJhiBoilW9pAPVJ/N6m 38RxOAv53gTn+wS8FB1n2PNX/ZIRRkeYXKkng/tjZj2tKhNYWezbbW8nFFzm9ysFvDKow1RX mr4ZoZ3GCZx6stlN1efmHb364ziZJzRdYdJ7kzSw0qG1bAFbs5vxZ9ozWJ9NGnwvGMo0bs+h B1qh9ShuZSfbn9q9+S/CwJZMTv8Y4US/CvshOBQhJXzvcjnE5N/FzEMRJatQ+ivFWdYvPLrL QuPVj16snCDFKHUACeQ7U5nqzTEFJXhZBT1bDEJiM5vQhWQPhkViQYYRjg72J5/Dgeyydfqb W924zkQ4hjzrR4GmYcKf1HvF2zYogmvcDI9TpOSeQFX4g917EDQKcWC7+h3EnIQ7ti7oQeKM GDeexVQADRDRBmfH166dOrLh5GI462CC+G5NfeLfbietbkUSaKT3Zz2mop+o2TXa4PWbyEkV aFknBIEBywxGtyFyWtTDXZMzGSUMZbd/FDlq0gV5oi+6Ki5BlypvNPVTeMUaZI1o1i3mfvRa bDW3noob2YAkMtLnyeAyaBDjgFIzXgyMWD8S/JY8nedKcCY0q5PU0xEN2UqbpYOt+RkmVATc c/D1oGsju4+16FqTQcDDRu7w4mofZBYej7mcgqWWADTcuzBfGOuoYm/YLvgG+cI3aME6lvp4 2bdSwi6YXyCj2W7DUnxd7wcynjKZloG/9jsOhd1VTq5FYygMEbqdoQty2VxmOxR5DuCI2cYN XIUn1pliLqW4GsYh/x+HzYE9X95NayenC3f6eDEK5EQuP8tAyJulusc7m5og71SpDpJQvB4g k6w5pZnvk2mn++TyzFmTAsGqzBFg5iOtFljPqOR/4dJWHLN9hYApWuKDBFCq9xgA9zp86der 7qH3Lr0MytH+snI8NE0AsHVLIeKPCNkP0a3XjHTCwQBQHigMmSez01RnfeO92GE+5g3rp+// fhGArRfVVEzCrYbEhE/RI1EcMoxBGt01+LF36tqrTKkoRLcRdtXpMXCX/OWW7D0LSqByKNDb F0OyK/5KoIaMsv63VZjYx90hteveQKYUNZTrylmdgJxrl9K9S00R2s/wU/kLAPr+HgLGOW/g zY5jwJ/ZaIm8zKmsDJVbhLa4TA9lkU8g4CvmTeKbDv4N7u9R6lTAivw8kU9a9b1H1gzYgq1k khpcjzDQvgC6tkoPXAugwjat5xVHPdaRqARex4cy8acYPAw2EhdoCGqraeizeTAAJpm0gAtd Mz0x5qh8wdqbdpwKKCJYaQVkB5fgaWBuiLu3ec0kld2z6kl/2abeSpOs0sNZOBOGg==
- Ironport-sdr: 659beec8_S15C+21qvip0l2AueEPFomEU4ueG1WKAUUR695nLlZ72ZYc MXeaSDhJupNLtv+PoYWZLcRzfBkxuqZqlSkL0eA==
Dear colleagues,
Another note: This talk will be recorded and made available on youtube
(I will come back with the link). I would like to apologise to those
of you attending CPP -- when scheduling this (which happened a while
ago) I lost sight of the overlap with CPP. :-(
Best wishes,
Andrei
On Mon, Jan 8, 2024 at 11:00 AM Andrei Popescu
<andrei.h.popescu AT gmail.com> wrote:
>
> Dear all,
>
> Next week there will be an online talk (via zoom) by Lawrence Paulson
> on a topic that is likely to be of interest to quite a few people on
> these lists. Please note the information about registration below.
>
> Best wishes,
> Andrei
>
> Information:
> https://www.bcs.org/events-calendar/2024/january/webinar-formalising-21st-century-mathematics/
>
> Date/Time: 15 January 2024, 4-6pm GMT
> Speaker: Lawrence C. Paulson FRS, University of Cambridge
> Web: https://www.cl.cam.ac.uk/~lp15/
>
> Registration: https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2024
>
> Title: Formalising 21st-Century Mathematics
>
> Abstract: The formalisation of mathematics is an ongoing process that
> arguably started as early as the 19th century, intensified with the
> foundational crisis at the start of the 20th century, and since the
> 1970s has been conducted with the help of computers. Recent decades
> have seen the machine formalisation of lengthy and technically
> complicated proofs, but some have argued that even these were not
> representative of modern mathematics. Recent achievements by a number
> of different groups are starting to challenge this scepticism. The
> speaker will outline some of these, while also noting some of the
> remaining trouble spots.
>
> Biography: Lawrence Paulson FRS is an American computer scientist. He
> is a Professor of Computational Logic at the University of Cambridge
> Computer Laboratory and a Fellow of Clare College, Cambridge. He is
> best known for the cornerstone text on the programming language ML, ML
> for the Working Programmer. His research is based around the
> interactive theorem prover Isabelle, which he introduced in 1986. He
> has worked on the verification of cryptographic protocols using
> inductive definitions, and he has also formalised the constructible
> universe of Kurt Gödel. Recently he has built a new theorem prover,
> MetiTarski, for real-valued special functions.
- [Coq-Club] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024, Andrei Popescu, 01/08/2024
- Re: [Coq-Club] LMS/BCS-FACS online talk by Lawrence Paulson, 15 January 2024, Andrei Popescu, 01/08/2024
Archive powered by MHonArc 2.6.19+.