coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024

From: xu AT math.lmu.de
To: agda AT lists.chalmers.se, coq-club AT inria.fr, types-announce AT lists.seas.upenn.edu, eutypes AT cs.ru.nl
Subject: [Coq-Club] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024
Date: Mon, 27 May 2024 22:41:49 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xu AT math.lmu.de; spf=Pass smtp.mailfrom=xu AT math.lmu.de; spf=None smtp.helo=postmaster AT mail01.math.lmu.de
Ironport-data: A9a23:abpSUaJtUxAp3IJmFE+RGJElxSXFcZb7ZxGr2PjKsXjdYENS1TUCn WVOWG+DbKzYazamLYxwat++8kkP6JGHytIyHQMd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf1s9JIGjhMsf7b9Ukw5K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LubUbOyd5XI2EKGYgn5cFOM1Ns3 /sCEWVYBvyDr7reLLOTT+Btgpx6asziIINZvnR9iz3UZRokacmZEuOTtYAehW5pwJsUdRrdT 5JxhT5HfAnoZhRTOhETDY94kOrAanzXI20B8AvO/vNfD2770VQ28obNAdnvcZ+sSOpamVe3n GiexjGsav0dHIbFmGTboyzEavX0tSj8QccZEKCy3uV7hUWagG0VEhwfE1WhycRVkWa7UtNbc xVS/yMyre428VHtQtSVswCETGCsoCM+UfFpPM0GzASy1Y3t0TS7LG8ed2sUADA5j/MeSTsv3 16PutrmAz1zrbGYIU5xEJ/I9Vte3gBOcwc/iT84cOcT3zX0iK0e5i8jo/5mGa+x1oSzHDjsw 3aOqTV4i7h7YS83O0eTow6vb9GE/8ahousJCuP/BTjNAuRRPtLNWmBQwQKHhcus1a7AJrV7g FAKmtKF8McFBoyXmSqGTY0lRe7wuabebGOM3QY1TvHNEghBHVb+Jui8BxkjfS9U3josI2WBj LL7510BvcE70IWCN/crC25ONyja5fK6RIq7B668gitmZpVwfgmG7mR0aEWQ0mb/nU4wi7w6U ap3gu7yZUv2/Z9PlWLsL89EiO9D+8zL7T+LLXwN50j9gOX2ib/8YettDWZimchisfnf+12Mq 48DXyZIoj0GONDDjuDs2dZ7BTg3wbITXPgacuQGJrTRERksA2w7Ff7azJUofoEvzewflf7F8 jv5EgVUwUb2zy+PYwibSGFRWJW2V7ZGrFU/IXMNO3Ss0CMdeoqB1voUWKY2WrgFz9Zd68BIY cMLQfjdPcQXeA/7o2wcSbLfsL1dcA+agFPSHii9Pxk6UZ1SZy3I3d7GYjrfzi4qCzqrufBjo I+b9xj6RKAbTF9IF/fma/OIznKws0MCmel0YVD6H9lLdGjo86loMybUnNZvB+0tczDtniC70 SSSCjcm/dj9mZc/qoT1tPrVvrWXHPtbNWsEOWvitJKdFzTQp0inyq9+CNe4RyjXDj7Iyf/zd Ndu7q/ONdMclwx3qKt6KbFgyJw+6/bJp7N3ygdFHm3BX2+0C4FPc2W34s1SipJjnrNpmxO6e kaqyOloPb+kPMDEEllIACEHau+F9+8fmxiMzPATDXj52hRK/+u8YR0PByWPtS1TF6sqEYUHx ex6htUaxTbigTUXM/GHrBtuyUKyElI6XZ4KiLQmEa7wqw9yylh9cZ3WUSD3x5eUauRzCEohI x7Kpa+bh71j2VXnSCcvJEj32s5YlYgCg01J/mQjPHWMoMLO3dUs7S1S8BM2bwVb9QpG2ORNI VpWN1V5CKGN3jVwju1RdjiINyAbITPB4W336V8CtFOBfnmSTmaXcVEMY7eczn4W40d3X2Z9/ ojB7E3HTDyzXsX6/hVqaH5fs/a5EOBArFzTqvuGQfaAMYIxOwf+o6mUYmENlRvrLOUxiGDDp sho5OxAUrL6BwFBv5wED5Sm6ppIRCCmPGBiRdRTzJENF0zYexCw3mGqAGK1ccVvOffL0BGZD +pDG8FxbCm9hR2+9m0jOa0xIrFPjKEI4vgGcejVPmIoieaUgQdol5PyzRLAolEXbe9gqusHE bOJRQm+SjSRoVB2h17yqNJ1PzvkQNscOyz58uOH0MQIMJMhrNBcS0YW16uos07IMzlc3gm1u TnbbPT81N1SyoVLnqrtHJ5cBg6yF8jBaeSQ/C23sPVMddnqI+6Wky808HzJZx93O5kVUPRJz YW9isb9hh75jexnQlLnlImkPIgXw8eLBc58EN/9dVtelgu8AP7c2QMJoT2EGMYYgeFmx5eVQ iWjY5GNbv8TYdBWwUNVZwV4ExowD6fWbL/qlRiirsajWwQs7gjaEOyJrXPZT3lXVistCa3MD gXZv/WP5NcBiK9uABQCJe9tAr4mAVvFdJYlSebMtmijPjH1um+Bh7rsq0Nxo3WDQHyJC93z7 p/5VwDzPkb68r3ByNZC9Zd+pFsLBXJ6mvM9ZV8Z58UwsT2hEWoaNq4IBP3q0H2PfvDaj/kUp Q0hbVfOzQ34VDVAKUy65d3/XkGbA/FINtqRyvnFOa+LQ3/eOW9CKOIJGuRcD7NefzL/zKejL MxY9nCY0t2Z3MRyXehKjhCkqb4P+x4Zr07kPWj4mtDyRRIbHPMG2RSN2eaLuTPvS6nwqakAG YT5qa2ojq12pY4d3PuMo0JoJSw=
Ironport-hdrordr: A9a23:RS1lsa2op/zJOhR4P4iQPAqjBKEkLtp133Aq2lEZdPVwSL38qy nIpoV+6faUskdzZJhOo7290cW7Lk80lqQFg7X5X43PYOCOggLBR+tfBODZogEIdReRygcQ78 ddT5Q=
Ironport-phdr: A9a23:4HJ78x3DMu+Rr3qfsmDOzg4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaOo68y0BSQAdqTwskHotSVmpijY1BI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQFFiCCjbb5wI xi6ohjdu8YUjIB/Nqs/1xzFr2dHdOhR2W5mP1WfkQri6Myt5pBj6SNQu/wg985ET6r3erkzQ KJbAjo7LW07/dXnuhbfQwSB4HscSXgWnQFTAwfZ9hH6X4z+vTX8u+FgxSSVJ8z2TbQzWTS/8 6dmTQLjhSkbOzIl9mzcl8t/gr9GoBK6vxxw3ZLbYJ2bOvp5e6PSZ9IaRWxcVcpVWCFMBoawY o0SBOQDIOlYtZHwqVsQoxWjCwajGOzgxSJHiHLtwa030PgtHR3a0AE6Hd8DtmnfotXvNKcVV OC41KbJzSjYYvNTwzj99IjIfgolofGJQLJ8a9fexlcpGgjYgVqetZbrMCmJ1uQRrWeb9exgW PqrhmM7qwx8vzeiytssh4fJiIwZ1k7I+CtlzIs6KtC2R012bMOgHZVQqS2UOZd7T8ciTmxop So216ALtYC5cSYKzpks2hDRa/uCc4eS4xLjUv6cISp+hHJkYb6/gguy/lamyuLgVsm7zlBKo jBYndbSrnwN2B3T6tSHSvtg5UitwzeP1wfV5+pZIk40jbLWJ4M/zrM0jJYfrEfOEy3slEnrk aOaa18o9+a25+j/bbjrp4WQO5JphgzxKKgih82yDOYiPgQTXWWW/eKx36D98E39XbVKleE2n bfDsJ7HJMQap7C2DhdJ3osl9h2xFS2p0M4CknkCNF9FeAyIj4zuO1zWJfD3F/a/g1CwnDt23 fzGO6fuAonNLnTZlLfheKt951RBxwUt1dxf5pRUBa8dIP/rR0P9qtjVAgUkPwG3wevrEshx2 p4DVW6VDKKVLrvesVqS6eIuJ+mMapUVuDH4K/U96P/ukGQ0mVoHcqm13ZsbcnS4HvF7I0mDf HXjnM8NEWERsQUmVuzllEWCUSJPZ3a1R68w+yk3CJi6AofbWoCtnLuB0T+nEZ1Rf2BKE0yDE XP1d4qfQPoMcyKTIsp5kjMeT7ShSokh1QuvtADg0bZnIPDUqWUkssfq29R8z+nSjg0pszd0B sCY3nuWCXp52isDQCZz16Riq2R8zE2C2O52mbgQCc1L6ugMWwE8MoPaxOFSD9HpRhmHZdqAU xC7WtigB3c8Qs91i9ITf1dlFs6KhQuFxTfsBbtGuaaMAckk74rZ1mTxYcJ41jDK2fpyx2I6S 9dCYDX1zpV08BLeUtKY+634v6OjdKBHmTXI6H/G1m2W+kdRTA93V6zBG3EZfErf69rjtQvZV 7H7L7MhP0NazNKabLNQY4j5kH1DTevjftDbfiS9ljT4Hg6Gk4uFd5GiYGABxGPYAUkAnRoU+ COWKCA7Dzuh5WbbEXpiGAGneFvipM95rn7zVUoo10eKYklmgqKy4QIQjOeARuk727sFvH947 TB9AFb729fLTdaNz+Z4VINbZ951oFJO1GaC8hd4IoTlNKd6wFgXbwVwuUrqkRRxEIRJ18Yw/ jssy0JpJKSU3UkkFXvQ1I3sOrDRNmj5/Qy+I6/Q1FbE1d+K+6AJoP0molTntQutGwIs6XJim 9VS1nKd4N3NAm9wGdrhT24y/gR64bXff28x6sKc1HFhN7W1ri6Xw8ggV6MuzhetecsaMbvRT VWjVZRKWI73cbVswAL6C3BMdPpf/6M1Ic68Iv6P2arwef1lgCrjlmNfpoZ0zkOL8SN4DO/Ox ZcMhf+CjW7lH3/xikmstsfvlMVKfzYXSyCv1ADhDZJRIKl3YMAHBC39a93y3dh4i5P3DjRI6 XamDk8GnsusZFyeYhauuG8YnVRSqnuhlyyiyjVymDx8tauT0hvFxOH6fQYGMGpGLIV7pW/lO pP8z9UTXUzzKhMsiAPg/kHiga5SuKV4KWDXB0ZOZSn/aW94AOO8sb+LYsgH751N020fQPmUZ FmGSvj5pgZc3y6rE2ZFxT89fi2nod2gxU080TLCai8q9TyCI4l53l/H6cbZROJN0zZOXyR+h TTNRz3ed5Go8diSi5bfo7W7XmOlWIdUdHqjxoeBuS2noGxyVETlzrbqyoKhSFFjl3ShhLwIH W3SoR3xY5fmzfG/OONjJQxzAUPkrtF9Asd4m5cxg5cZ3T4bgI+U9DwJizSWU50T1KTgYX4KX TNOzcTS5V2vyFBLK3uVx8T9U2jbzsYrNJGqJ3gb3C4w9ZUAGLq86bVYnW1xp0f+oQ+bMp0f1 n8NjPAp7nAdmeQAvgEgmz6cDr4lFk5dJSXwlh6M4oP2vOBNaW2oa7T1yFtmkIXrEuSZug8FE iWcGN9qDWpq4854Kl6JzHDj9tSuZozLddxK/hTGiBLcl65QIY4x0P4PmGxrNAef9TUsmfEyl Rln3JX8uYGbKyNp+b//DhMQP3X0YcgX5z3g35FFhsjQ2omuGtNlACdNUJagW/usFHh6We3PE QGIHXV8r36aHeGaBgqD8AJ9qGqJFZm3NnaRLX1fzNN4RRDbKlYNyAYTFC43mJI0DGXIjITob Vt56zYN51X5tgoEy+RmMAP6W3veowHgYyk9SZyWJh5bpg9Y4EKdPcub5+N1VyZWm//p5BSKM XCebh9UAHshX0WFAwi6eLyn+dmG9+2FQOazbrPPbbiIte1CRqKIyJaoge4Et36HMsSCOGUnD uVugxASGykpRIKAwmxJEHZE8kCFJ9SWrxq95CBt+8W28fCwHRnq+ZPKELxKd9Nm5xGxh66Hc e+WnidwbzhChfZujTfFzqYS2FkKhmRgbT6oRP4QqAbIRb7Q3KtSElgXZmkgUakAp7J5xQRLN cPB35nt0aVki/cuF1pffVnom8XxPIoPKn29clfCGQCHOf7VQF+Di9GyaqS6R7pKiexSvBDlo jeXHXjoOTGbniXoXRSiWQmppCSSIBwYvISgNBpgWzCLpD3ObxSnMJlziCBwzbBm3xsi1EYZO Dl4KxoLq7SM7WVch+g5F2ETthJY
Ironport-sdr: 6654f010_wxAbyMWAZzarK2byG15vMODU2L9is5MJiPsZpnnSyg0U/0h x+J5zOlc30KpC8BzDDjrX6rD2g3tY85JJy3gNeA==

[Second call for applications]

Autumn school "Proof and Computation"
Fischbachau, Germany, 15th to 21st September 2024
http://www.mathematik.uni-muenchen.de/~schwicht/pc24.php

This year's international autumn school "Proof and Computation" will be held
from 15th to 21st September 2024 in Fischbachau near Munich. Its aim is to bring
together young researchers in the field of Foundations of Mathematics, Computer
Science and Philosophy.

SCOPE
--------------------
- Predicative Foundations
- Constructive Mathematics and Type Theory
- Computation in Higher Types
- Extraction of Programs from Proofs

COURSES
--------------------
- Thierry Coquand (Gothenburg): Topos theory and constructive mathematics
- Klaus Mainzer (Munich): From Proof and Computation to AI - Logical, Mathematical, and Philosophical Foundations
- Gerhard Jäger (Bern): Foundations of explicit mathematics
- Sara Negri (Genoa): Enriched syntax for enhanced proof theory
- Monika Seisenberger (Swansea): Extraction of programs from proofs
- Holger Thies (Kyoto): Extracting efficient programs from proofs in analysis
- Freek Wiedijk (Nijmegen): The De Bruijn criterion versus the Poincare principle

WORKING GROUPS
--------------------
There will be an opportunity to form ad-hoc groups working on specific
projects, but also to discuss in more general terms the vision of
constructing correct programs from proofs.

APPLICATIONS
--------------------
Graduate or PhD students and young postdoctoral researchers are invited to
apply. Applications (e.g. a self-introduction including research interests
and motivation) should be sent to

Chuangjie Xu <xu AT math.lmu.de>.

Students are required to provide also a letter of recommendation, preferably
from the thesis adviser.

Please specify in your application whether you are interested in applying for
financial support (details provided below).

Deadline for applications: **7th June 2024**.

Applicants will be notified by 24th June 2024.

FINANCIAL SUPPORT
--------------------
Successful applicants are eligible to apply for financial support that covers
accommodation and meals for the duration of the autumn school. Information about
funding application will be provided to the selected candidates.

The workshop is supported by the Udo Keller Stiftung (Hamburg) and the COST
Action EuroProofNet <https://europroofnet.github.io>.

Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg

[Coq-Club] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024, xu, 05/27/2024