coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Autumn school "Proof and Computation", Herrsching (Germany), 10-16 Sep 2023
Chronological Thread
- From: xu AT math.lmu.de
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Autumn school "Proof and Computation", Herrsching (Germany), 10-16 Sep 2023
- Date: Mon, 03 Apr 2023 22:55:45 +0200
- Authentication-results: mail2-smtp-roc.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:7EmpH63TleGivwlUavbD5fB1kn2cJEfYwER7XKvMYLTBsI5bpzEGy GYcUT/UbP3bYGv1L4hxPYi/oBsO6JDVztNiSgZl3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/vOHNIQMcacUghpXwhoVSw9vhxqnu89k+ZAjMOwa++3k YqaT/b3ZRn0i1aYDkpOs/jY8E8356yo0N8llgVWic5j7Ae2e0Y9V8p3yZGZdxPQXoRSF+imc OfPpJnRErTxon/Bovv8+lrKWhViroz6ZWBiuVIKM0SWuSWukwRpukoN2FXwXm8M49mBt4gZJ NygLvVcQy9xVkHHsLx1vxW1j0iSlECJkVPKCSHXjCCd86HJW1vF//VoLGAJBJ8Bqt5JLFtyy +4bNj9YO3hvh8ruqF66Yuxlh8B7dY/uNZ8f/HVl0HfVAJ7KQ7iaGfSMvI8Hmm5p34YVR54yZ OJBAdZrRATdSxhGJldRDJcj2uul7pX6W2QA8A/O/fJmvgA/yiRM3pPvatT3ZubSSMBExF/B/ Hn3olbmV0Ry2Nu3k2DUrCz92IcjhxjTU4ULUba86/RCm0yW3mVVCRsMVFL9r+PRt6Klc9dWK khMo2wrpLQyskiuU5/xUnVUvUJooDY8cuZQFc0b1zif0/rs3SujOlYWTSBOPYlOWNANeRQm0 VqAntXMDDNpsaGIRX/1yop4vQ9eKgBJfTZSPnFsoR8tuoC+/9xv5v7aZo87SPbdszHjJd3n6 xynxMTUr5AOi88A181XFniX22L0+fAloiYf7xveRGOshj6Viaagbo2ssQGd6P9cLMCdS0THs HVsdymiAAImU8rleM+lGbtl8FSVCxCtama0bblHRcJJythV0yT/Fb28GRknTKuTDu4KeCXyf GjYsh5L6ZlYMROCNPEnO9/tVZpxkvO7SLwJs8w4iPITOPCdkyfapklTibK4hjyFfLUEyvBiY c/LGSpSJStKU8yLMwZat89Hi+51mHFgrY8ibZT2zh6h0KjbfnOeSboDIlaIcvok6cu5TPb9r b5i2z+x40wHCoXWO3CHmaZOcwxiBSVlVPjLRzl/KrbrzvxORDtwVJc8ANoJJ+RYokiivr2Wo ivnCx4AmAKXaL+uAVziV02PoYjHBf5XxU/X9wR2Vbpx8yhzP9Sc/+0EeoEpfLIq0uVmwLQmB 7MGYsiMSLAHADjO5z1XP9G3oZ1AZSabo1uEHxOkRzwjIL9mZQjCoeH/ciXVqSIhMyuQtOkFm YOG6D/1e5Q5elldPJ7kU873l1KVlloBqd12RHrNc4Vyel2z0Y1EKB7Rr/4QIuMQGCX5wR+fx xqaOkobl9LsuK4wysHC3oqfnreqEsx/P0tUJHba5rCILhvn/nKv7ItDceSQdxXPfTvQ1IT4Q MsN1ND6EvkMvGgSgrpGC7wxkJ4PvYr+lYFV3iFPPSvtbW3yLphCP3Pf/81ElpMV949joQHsB 36+oIhLC46oZvHgPkUafjc+T+K50voRpDnewNI1LGj+5w515LC3alpTDTbdlB1iKKZJD619z dcDoMI27ymNuiguOPuCjQFW8D2CFWxfcqMFsppBPpTnpDB2wX5/YLvdKBTM3rexV/t2PHIHG ASk3Jj5u+wEx27pUWYCKnzW7O8M2bUMoE9ryXEBFXSom/3EpOMG7CdW1TEnUghukxZ16MNoG 21RL0YuD76/zzRpo8liXm6XBABKAiOCyHHx01ckkG74TVGic37kdEkRGLyo0hgC0mR+ejN7w ump+Fz9W2y3QPCrjzoAZ0F1jtfCE/pzz1Tms+K6FZ2nG5IaX2LUspW2bzBVlyq9UNIDv2yZl +xE5+0qVLbaMxQXqKgFC4W387QcZRSHBW5aS8Fa46I7MjDASQ62xASxBRi9SuFVK9zO1H2IO chkC8ZMdha5jSi1vm86A4wIKORKh/IH3ocJVY7qAm8kiIGhiARVnqjezQXAoVM6Ys5PlJ89I 7zBdjjZHW23g2BVqlD3r8JFGzSZZIAEbTLjw8WOrfk4J6gElOR8bU0Jj7iGhFSOEQ5d5xnPl hjyV6zX6O1DyIpXgIrnFJtYNTi0Md/eUOep8hi5lsZnNffjEJ3rmVsOi1/FOw92A+Mga+5vn +7QjO+tjVL3grkmdkv4xb+DLvBtzuevVrN1NsnXEiFrrRGaUpWx3ypZqnGKEr0XotZz/cL9e hCZbvG3ftsrW9tw4n1ZRixdMhQFAZTMcabSinKhnsuIFyQi/1TLHPG/+V/tSFNrRCsCFpn9K w3z4viQv4ES6MwGARIfHPhpDqNpOFKpC+Nsa9T1siLeFWWyxE+Lvrz5jxc79DXXET++Hd3n5 Y7eDA3LHPhoVHokEPkC22CzgvEWMJq5qew5f0ZFophzgiy6SmoDMKIRPP3qz32SfjPajPnFi PPlNQPOyhkRmRxBeAn8ptDmQ0GTC4Ti///ncycx8Rr8hzieXeu97XgIysuky3J/ZjulyOS6b 90TkpE10t5d3bkxLdsuCjeHbSuLCx8UKr/kOawwriAqPysjPA==
- Ironport-hdrordr: A9a23:8XVoK6r8xBeJKgo2T3MKwPEaV5pEeYIsimQD101hICG9E/b5qy nAppomPHPP5Qr5O0tApTnjAsO9qBrnnPYf3WB7B9iftWfd1FeVEA==
- Ironport-phdr: A9a23:HovYFByujVheWcPXCzLrwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hGZv6syxwaUAc3y0LFttan/i+jYQ2sO4JKM4jgpUadncFs7s/gQhBEqG8WfCEf2f7bAZi0+G 9leBhc+pynoeUdaF9zjaFLMv3a88SAdGgnlNQpyO+/5BpPeg9642uys+5DfeRtEiTu/bL99M Rm7rQrcvdQKjIV/Lao81hTGrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02Q aRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+8 6tmTgLjhSEaPDA77W7XkNR9gqJFrhy8qRNw34Hbb5yOOfpiYq/RYc8WSXZbU8tTUSFKH4Oyb 5EID+oEJetZoJT9qkALrRSkGQmsBPnjyjtNhn/rx6E1zvouHAfb1wMvA9wAqm7brMnpNKgMS +C1yrHFwzvdY/5UxDvz55XEfxEhrP2QU799bMncx0YxGw/bj1idpo/oMy+U2+kOr2WW7+puW P6vhWI7pA98rTmiy8Qjh4TPm4kbxFfE9SBjz4Y0I921UFN7YdilEJdJsiGaKpV5QsU+TGFop ik6zKcKtoOlcyUM1Z8pxAbfZuSaf4SW5h/vTvudLDR6iX5/Zb6zmgu+/VKux+HiTsW531dHo jBYntXRuX0BzQHf58mGR/dn40us2TiC2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmErsj a+Wclko9vWy5+TieLrmup+cO5VwigH7L6QigNGwDvogPggPWWiU5/i82aX+8UHnRLhGlOA6n 6rbvZzAOMgXu7O1DxVb34o98xq/Ci2p0NUcnXkJNlJFfxeHgpDmOlHTO/34CO2wg0iskDtxw /DGO6DhDo/QIXfdiLvhe61y5FZGyAUv1dBf+45UCrYZLf7uQkPxrsDXDgclMwyoxObqEMly1 oQHWW6WHqCZNL7SvkST6+I0I+iMYZcVtyznJ/gk4f7ul345lkUHcamnx5tEIEy/S/9hOgCSZ WfmqtYHC2YD+AQkH8Lwj1jXQSN7Yn+uX+Q44yx9BI/1Xs/4WomxjenZj2+AFZpMazUeYrjtO XLhdoHeHuwJdDrXOMhq1DoNSbmmTYYlkxCorg7zjbR9faLP4iNNk5Xl2ZBu4vHL0wko/GlkE uyY2n2NCWVxgyUESmx+x7hx9HR00UzLyq1km7pdHN1X6elOV1IqKLbZxvB6TdT3R0TNc4TBU 06oF/OhBzx5Vdct25kObkJ6Ts2llQzG1jG2DqU9krWKAMRttKfVw3i3I8NgjXrLvEU4p38hR MYHdWivh6olshPWG5aMiUKS0aCjaaUb2ifJsmaF12uH+k9CAkZ2Vu3eUHYTa1Gzz5yx717eT 7KoFbUsMxdQgc+EJKxQb9T1jFJADP79MdXaami1li++HxGNjr+LaYPrfS0a0kC/QAAUjigW9 GqGcww7G2GtriOWDTBjE07uf1K56fN3+zuwSk45yR3PblU0juDkvEdF2rrFEqpVhehX3UVp4 y95F1u8wd/MXt+Jpg47Ob5Zfct4+lBMk2TQqw16OJWkaaFknF8XNQpt7CaMn116DJtNlc8yo TYk1g13fOiIzXtEfi+Ym5T1J/vbJyOhtADqcKPQ1lzEhZyG548K4eg47VHmoUelGwBxlhcvm 8kQ2Hya6JLQCQMUWp+kSUc7+S9xoLTCazU87YfZvZF1GZG9qSSKm9cgBe9/jw2lY88aKqSPU gn7D8wdAcGqbu0sgVmgKBwebqhe86s9PsXucPXjuubjLPtImTu6jSJD5Z073k/E+ydnS+HO1 ooI2LnBhFrBDmejyg7464asw8hNfnkKE3C6yDT4CYIZfaB0cYsRSALMa4W2yth4m5/xSitd/ V+nCUkB3Zzhch6TYlrhmAxIgB1N8Dr+yXT+lmUt1Wpz/c/9lGTUzu/vdQQKIDtOTWhm1xL3J JSsysodVw6uZhQokx2s4QD7wbJareJxNTq2Iw8Aci7oImVlSqb1uKCFZpsF+I4AtCxLUKK4Z E3cRrO38FMKljjuGWdT3mVxZyyCv5zln1p+jX/bIHs5/x+7MYlggBzY4tLbX/tY2DELETJ5h TfgDV+5J9C1/N+QmsSLoqWkWmmmTJEWbTjzwNbKqn6g/WMzS07a/bj7ipj9HAM9yyO+y9R6S XCCskPneoeyn63oKud7Zg9tDUP8rc5/B8dyn+5SzNkZi2cTnpCc/H5BlG7vMZNf3L+4YHdFT HYKxdXR/QToinp4NnzPwov4UjOZ2Nkna9TydGoS3mhVA9liLqCS4fQEmCJ0pgD9tgfNeb1nm Txbz/Iy6XkciuVPuQw3zyzbDKpAVU9fdTfhkRiF9bXc5O1eeXqvfL6s1UF/gcHpDbeMpRtZU Wr4fZFqFDF578F2OlbBmHPp7YSsdN7VZNMV/hqa9nWIx/BSM440n+EWiDBPPGv8uSV8jesyk Rwo2ZSn+oSKai1s8K+/Hh9EJ2j1ascUqVSPxe5Vmseb2ZzqH400Q29aGsK4ErTxSWtU7q60U mTGWCcxoXqaB7fFSAqW6UM86mnKD4juLXacYn8Q0dRlQhCZYk1ZmgEdGjsgzftbXkinwtLsd EBh63Uf/Fn9/1Fc18ptPgX/FGPauUGkZ31nLfrXZAoT9QxE60rPZIaG6flvGihD4pC7hAmEK 2jDPkJNBH0JHEiBGhbvM/P9gLuIu/jdDe24IfzUZLyIouELTPaEy6Wk1Y5+9iqNPMGCVpGHJ /gyxkoFWXVkXcjUyW1no8M/kivRb4ifoQr69iAl96hXEdzuUQPrvdLJDrJOMZNr/g3wjarRb 4at
- Ironport-sdr: 642b3d53_vaxFxO4OeBYnbezW/kWnmTTuALW3t5xmTDBWE73iIXZcJyq uXAg1cOrkmMcNTY/QO6OwSLyiP7mLoifeAxDAjg==
[Apologies for multiple postings.]
Autumn school "Proof and Computation"
Herrsching, Germany, 10th to 16th September 2023
http://www.mathematik.uni-muenchen.de/~schwicht/pc23.php
This year's international autumn school "Proof and Computation" will be held
from 10th to 16th September 2023 in Herrsching 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
--------------------
- Stefania Centrone: Husserl on the Totality of all Conceivable Arithmetical Operations
- Yannik Forster: MetaCoq
- Hugo Herbelin: The logical structure and computational contents of choice, barinduction and related principles
- Martin Hutzler: TBA
- Georg Moser: Cichon's conjecture on the slow growing hierarchy
- Andrea Rechenberger: Philosophy and history of computation: Turing machine
- Monika Seisenberger: Extraction of programs from proofs
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.
Deadline for applications: **31st May 2023**.
Applicants will be notified by 28th June 2023.
FINANCIAL SUPPORT
--------------------
Successful applicants will be offered **full-board accommodation** for
the days of the autumn school. There are NO funds, however, to reimburse
travel or further expenses, which successful applicants will have to
cover otherwise.
The workshop is supported by the Udo Keller Stiftung (Hamburg), the
CID (Computing with Infinite Data) programme of the European Commission
and a JSPS core-to-core project.
Klaus Mainzer
Peter Schuster
Helmut Schwichtenberg
- [Coq-Club] Autumn school "Proof and Computation", Herrsching (Germany), 10-16 Sep 2023, xu, 04/03/2023
Archive powered by MHonArc 2.6.19+.