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: coq-club AT inria.fr
Subject: [Coq-Club] Autumn school "Proof and Computation", Fischbachau (Germany), 15-21 Sep 2024
Date: Tue, 12 Mar 2024 06:01:04 +0100
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:xgVnoqBp6LhUlxVW/+rnw5YqxClBgxIJ4kV8jS/XYbTApDsmhjNWz zZJDWuCPPuLNDamfop3PoW090MO68CHz4c3OVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuHZzdJ5xYuajhIs/na8ks21BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc5xDsNCHe2uhWNUA/M6EK2vp2Xjpr8 fNNfVjhbjjb7w636LeyS+0034ImJdXreocapzdswFk1D95/G8GFGvWVo4YBhXFr3KiiHt6GD yYdQSpyRBHJfx0JPlIKTp4z9AutrimmI2MH9gzLzUYxy0PjlCVsiKTtCfTYYd6tWPR23WOx/ G2TqgwVBTlAbo3Bl2vbmp62vcfEmjq+U4YPHpWj5/tyiRuSwHYSAVsYTzOGTeKRj0e/X4oGb Ukd5ipoqa0vskCmJjXgY/GmiCOu+UQuQsdoKuwz5i2f6rbVvF28AmdRG1atd+canMMxQDUr0 HqAkNXoGSFjvdWppZS1re/8QdSaYnN9EIMSWRLoWzfp9PHPjekOYv/nS99iFPbsyNj8BTG2x zWX6iQz71nysSLp//vllbwkq2vyznQscuLSzl+PNl9JFisjOOaYi3WAsDA3F8poIoeDVUWmt 3MZgcWY5+1mJcjSzXTUELxdTOv4u6nt3NjgbbhHQ8hJG9OFpibLQGysyGguTKuUGphaKWa3C KMtkVoJtfe/w0dGnYctOdPvVZV0pUQRPdDoV/rSb8gLeJV6dAKB7ixoeVSN2gjQfLsEz8kC1 WOgWZ/0Vx4yUP03pAdass9BidfHMAhinzKMLX06pjz7uYejiIm9EOZVbwvTP75hvMtpYmz9q r5iCidD8D0HOMWWX8Ud2dd7wYkifChhV6Pl4ddabPCCKQdAEWQsQa2Zi7A4doAv2+wfmu7U9 zvvEgVV2Xjut03hcA+qU3FEbK+wfJBdqXlgAzcgE2z10FceYKGuzpwlSb0JQZcd+tdO89tIX tgeWsDZAv1wWjXNoDscSp/mrb1dTheghCPQHi/8YDEAYIFFfFHVy+/eeS/q5DUCNXe0h/Afu Jyl7BvQGrAYdjRhDeHXSfOh9Eywtn4jg9BPX1PED91QWUf0+q14AnTVot5tBu9UMjTF5D+R9 zjOMCciveOX/rMEqojYt56Lv6KCMrVYHHMDO0L58LzvFy3R3lT78L96SOzSIAzsDjLlyp6DO 9dQ4er3asAcvVBwtIF5LbZn4IQ+6/brpJ5Y1g5UJ2rKXXv6FoJfJmS64ucXup1v3rN5vS6Ea nCL8PReOpSLP5rBO3wVLwwHcO+C9K81nh//0PcLG3j5tRRHpOe/bUZvPhe3mHN8KplxO9gb2 usPgpMdxDG+rRsICey4qB5o2V6CFEFdbJV/hKomWNfqriEJ1mB9ZYftD36qwZOXNPRJHEoYA h6Vo6vgm4Vs/E3mdmovGUOQ3thmpI8vvSpSxwQoPGW5mdvih9420iZO8D8xcB9n8xVf3893O UlpL0dQN4zW2xtJ3u1tB3uNHSNFDz2non3B8UMDzjDlfhP5R17zI30YEsfT2kIgqkZ3XCVRp ZOcw0bbCQfaRtn7hHYOaBQ0us7YbIJD8yPZk5qaBOWDJZ4xZATljoKIZWYlrxjGA9s7tHbYp NtFrfpBVqnmCRE++6ELKZGW9bA1eiC2IGZvRfJA/qRQOUr+fDq0+yaFKmHvW8drCsHJz3SFC J1VFpoSbyi96SeAlSBEJKguJ7QvouUlyuBfcZzWJEkHkYClkBxXjLzq+BPTvlQbG+dVrZ5lK 6f6VS6zLWiLtH4Fx07PtJZlP0S7U/klZSr9/vyEwN8OM5cTrO1XLEIA6ZqvnnCvKAA81Qmlj ADCQK73zuJZ1oVnmbX3IJhDHwmZLdDSVvyC1RKa6/BiTInqH5/VlgU3rlLHAVxnDYEJUY4qq YXX4c/F4kzVmZ0XDUbbosClPItU75yQWOF3DJrGHENCl3HfZP62sgoxwEHmG5lni9gH29KGQ TG/Y86OddI4fddR6XlWSipGGSYmFKXFQfb8lBy5ssizJEAR4S7fIPOj0E3ZX2VRWysLGp/5U yvfmfKl4PJGp4VtWj4AIdxbAKFDHVyyYpt+KuXNtgSZAFfx0xnG8vHnmAE74D7GNmicHYyoq djZTxz5b1KptLuO0NhdtJdoswYKCGpmx9M9ZV8Z58U8ngXS4LTq9gjBGc5u5lBofi3OOFXQY TjMaDN7TyD0QTQCdRDhptjuNuta6iriJf+hTgHFPWvNA8t1OG9EKL5o6icm53JrPDfupA1iA c9L4WX+Z3Bd3bkwLdv+JZWHbSNPw/rGxjQM/F27n8Ga79Pyx1kV/CQJITehnhAr3y0AeIsn6 IT1qa15rJmHdHPM
Ironport-hdrordr: A9a23:AIooeq293YPXHo33fd8KfQqjBKEkLtp133Aq2lEZdPVwSL38qy nIpoV+6faUskdzZJhOo7290cW7Lk80lqQFg7X5X43PYOCOggLBR+tfBODZogEIdReRygcQ78 ddT5Q=
Ironport-phdr: A9a23:879z/x/poS0eWP9uWda3ngc9DxPPW53KNwIYoqAql6hJOvz6uci4b QqAv74y0xeJBdydt6gUzbKO8ujJYi8p39WoiDM4TNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB 89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9sK Bi6twfcutcZjYZgKKs61x/FrmdVd+hMym5kO1Gekwzg6sus+ZJo7jhdte8m+8NcXqr2eLg1Q 6ZfADo6LW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59 KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8Y pMPAeQfIOhXoZXyqFQTohWxHgSsGODixiNUinPqx6A30eIsGhzG0gw6GNIOtWzZrdroNKoJV OC61rXIzTXZY/NS3Df99ZLEfQ0/rvyKQLl/ftbfx1M1GAPZklWft5blPzWN2+kOr2SX8eRuW fyuhmM5tQ1/ojiiy8Qoh4fJmI8YyF7J+DhkzIorONC1R051b965HJZSuCyXOIt4Tt8mTmxmp io3zKANt5C8fCgP0psnxhjfZuSac4iO4xLvTeORISpmi3JjZL2/hwi98U66xuLhSMa51ktBo CldktTUq3wByRje5tKaRvZ+/EqtwyuD2x3O5u1eL004i7LXJpEgz7Iqi5YfrEvOEjXqlEnsg qKbd0Mp8fW25uTjf7XmvYOcOJFuig/jM6Qvm9KwDPwkPgUIQmOV4/6z1Kf58k38WLhKjuM5k q3esJ3CIMQUvK+5AwtJ3oo+8Rq/Ci2p0MgYnXUdKFJFfQ+Hg5L0NF7QOPz4DPG/jEqwkDpz2 vzKILnsDo/QInXAkrrtZ6tx51NBxAYpw91T+YpYCrQbL/LyXk/xusbYDhg8MwGszOfnFc5w1 oYEVmKTAq+VKqfSsVqV5u41PuaDepcZuDDmJPc9/f7hkWc5mUMBfamuxZYbdWi0Hu56LEWBf XrsntABHH8WsQo5VezmkUGNUTpOZ3mpRK88/TE6CIe+DYjZXIytgbqB3D26HpJMfGxGBEqMQ j/UcNCPXO5JYyaPKOdglCYFXP6vUdwPzxar4R/n479uMuqS/igF857uh4s93PHaiRxnrW88N M+ayWzYFwmc/0sNTj4yh+VkpFBlj0yEye5+iuBZEtpa47VIVB07PNjS1b8yEMj8DyTGeNrBU 1O6WpO+GzhkXs8ZxtYSYwB5Hsjkgh2QlzGyDeotnqeQTIcx7rqa2nHwI8hnzHOTxLQJilA6Q o1LMHDgiqMsvxPLCdvvlEOU372vabxa3CPJ8zKbynGSuUhDTANqeaDMXHRHPw3TpMj5oEfHU vmiBNzLKyNnzsiPYutPY9zt1hBdQev7fc/ZeyS3knuxAhCBwvWNapDrciMTxneVDk9MiA0V8 XucUGp2Ti68v2LTCiBvHlPzcgvt9+d5snayUk4zyUmDcURg07O//hNdi+abTrsf2bcNuSFpr DsRfh71z8/+DtOcp0xlebgabd58qFZL2GTFthBsa4S6JvMqjVoffgJr+kL2gkwtW8MZwZds9 SpzilEoesf6mBtbejiV3I79IOjSI2j2p1W0brLOn0rZyJCQ87sO7/IxrxPiuhuoHwws6SYCs ZEd3n2C65HNFAdXX4j2VxN95wVSorjGYm854p6S2XAmYuGk9yTP3d4kHr5v2guIet5DMOWAE RK0H8BQVK3MYKQ63lOuaBwDJuVb8qU5atine/Wx06muJO98nTiigAyr+ahF21mXv2p5Q+/Mh NMexu2AmxCAT3H6hUugtcb+ncZFYysTFyyx03qsCIlUb6x0NYEFbAXma92q7tB3m56rX3tFs lKuT18Lw86mfxOOYke1hFcBkx1H/jr+wHL+lGY8miphtqeF2S3S3+nuPAEKPGJGXigH7x+kI IS5icwbQFn9agEokBW/4kOpj6Nfpal5MyzSWRIRJXmwdjE9FPLp7/zZOZ0qittgqyhcXeWib ErPT7f8p0BfyCb/By5Fwyh9cTi2u5L/lhg8iWSHLX81omCKHKM4jRrZ+tHYQuZcmzQcQywtw ynKLl21I9nv+dCJ0ZvO+LP2Rye6W5tffDO+h5OdnC6y+W0sBRii2fy+0I6Cc0BywWrw0N9kU j/NpRD3b9zw1qi0Bulge1FhGF7278cpUpE7iIY7g4scnGQLnpjAt2RSin/9aJ8IvMC2JGpIX zMAxMTZpRToyFE2ZGzc3Jr3Dz2UkNBke8H8Z2oK2mQ56t0MBKrxjvQMlHlqq0K9pAPVJ/10g jdbzf4zrnIXy+hBuQwmyjiRD+IlBlFWeynllhDO68qs6qlaLHCmdbz6vKZntfamCrzK4gRVW XKiP4wnATc19cJndlTFzHz07IjgPtjWd9Ma8BOOwV/GiKBOJZQ9m+Bv52IvMH/hvXAj1+8wj AB/lZC8so+dLmxx/aW/ShdGPzzxbskX93njl6Fb1sqR2omuGN1mFFBpFNPwSum0FTsJqfn9H wOHETlk8zGeEKbfWwua9QFqojOHEpymMW2WOGhMzdhmQ0r4RgQXiwQVUTMm258hQ1nwlYq4I Bg/v2lIoAWi+X4ugqpyOhLyU3nSvlKtYzYwE92EKQZOqxpF/wHTONCf6eR6G2dZ+IegpUqDM D/+BUwAAGcXV0iDH12mMKOp4IyK4/WwA+OiL73KZKjIpeEUBJLqjdq/l5Br+TqBLJDFJn55E /gywVZOR1h8EsXdw2xJTiULl2TJatPdqBr2qUgV5oivtf/sXgzo/46GDbBfZM5u9x6BiqCGL +eMhSx9JF6wM7sJzGPIjrwawRgehnM2H9FCObEJqS6LSKfN3KNaXUdzg8JbMcJJ6/plmAxEJ c6djtbokLJ13KZdNg==
Ironport-sdr: 65efe191_Xvf0KRT71JSfhxCH7eroS4ArOS2rCvpIMiGLvqQ6nKoTE4u kezaI2gBowhy0wXsp8/3yzkNzAWaMCgVToK8DdQ==

[Apologies for multiple postings.]

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 (Padua): 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 (approximately
116 Euros per day). Please note that there are no funds available for the
reimbursement of travel or additional expenses, which successful applicants
will need to cover independently.

The workshop is supported by the Udo Keller Stiftung (Hamburg) and the COST
Action EuroProofNet.

Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg

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