Deadline extension for FICS Workshop (new deadline: 6/12/2023)

Alexis Saurin <[email protected]> Fri, 01 Dec 2023 12:06:04 +0100
Newsgroups gmane.comp.lang.agda,gmane.comp.science.types.announce,gmane.science.mathematics.prooftheory,gmane.science.mathematics.categories,gmane.science.mathematics.logic.coq.club,gmane.comp.lang.caml.inria
Message-ID <[email protected]>
CgooQXBvbG9naWVzIGZvciBtdWx0aXBsZSBwb3N0aW5ncykKCkR1ZSB0byBzZXZlcmFsIHJlcXVl
c3RzLCB3ZSB3aWxsIGV4dGVuZCB0aGUgZGVhZGxpbmUgZm9yIHN1Ym1pc3Npb25zIHRvIApGSUNT
IHdvcmtzaG9wIGFzIGZvbGxvd3MsIGFza2luZyBhdXRob3JzIG9mIGNvbnRyaWJ1dGlvbnMgdG8g
cmVnaXN0ZXIgCnRoZWlyIHBhcGVyIHNvb246CgotIFBhcGVyIHJlZ2lzdHJhdGlvbiBkZWFkbGlu
ZSAodGl0bGUgYW5kIGFic3RyYWN0KSA6IFN1bmRheSAzLzEyICgyMzo1OSAKQW9FKS4KLSBQYXBl
ciBzdWJtaXNzaW9uIGRlYWRsaW5lIDogV2VkbmVzZGF5IDYvMTIgKDIzOjU5IEFvRSkuCgpNb3Jl
IGluZm8gYmVsb3cgd2l0aCB0aGUgdXBkYXRlZCBjZnAuCgpCZXN0LAoKQWxleGlzIFNhdXJpbgpJ
UklGIC0tIENOUlMsIFVuaXZlcnNpdMOpIFBhcmlzIENpdMOpICYgSU5SSUEgUGljdWJlCmh0dHBz
Oi8vd3d3LmlyaWYuZnIvdXNlcnMvc2F1cmluL2ZpY3MyMDI0L2luZGV4Lmh0bWwKCgo9PT0gVGhp
cmQgQ2FsbCBmb3IgQ29udHJpYnV0aW9ucyA9PT0KCjEydGggSW50ZXJuYXRpb25hbCBXb3Jrc2hv
cCBvbiBGaXhlZCBQb2ludHMgaW4gQ29tcHV0ZXIgU2NpZW5jZQoxOSAmIDIwIEZlYnJ1YXJ5IDIw
MjQsIE5hcGxlcywgSXRhbHkKaHR0cHM6Ly93d3cuaXJpZi5mci91c2Vycy9zYXVyaW4vZmljczIw
MjQvaW5kZXguaHRtbAoKTmV4dCBlZGl0aW9uIG9mIEZJQ1Mgd29ya3Nob3AgKDEydGggV29ya3No
b3Agb24gRml4ZWQgUG9pbnRzIGluIENvbXB1dGVyIApTY2llbmNlKSB3aWxsIHRha2UgcGxhY2Ug
aW4gTmFwbGVzIG9uIHRoZSAxOXRoIGFuZCAyMHRoIG9mIEZlYnJ1YXJ5LCAKMjAyNCwgYWZmaWxp
YXRlZCB3aXRoIENTTCAyMDI0IChodHRwczovL2NzbDIwMjQuZ2l0aHViLmlvL0hvbWUvKS4KCgo9
PSBJbXBvcnRhbnQgZGF0ZXMgYW5kIHByYWN0aWNhbCBkZXRhaWxzPT0KCgotIChORVcpIFBhcGVy
IHJlZ2lzdHJhdGlvbiBkZWFkbGluZSAodGl0bGUgYW5kIGFic3RyYWN0KSA6ICoqU3VuZGF5IDMg
CkRlY2VtYmVyICgyMzo1OSBBb0UpKio7Ci0gKE5FVykgU3VibWlzc2lvbiBkZWFkbGluZSBmb3Ig
c2hvcnQgYW5kIGV4dGVuZGVkIGFic3RyYWN0czogCioqV2VkbmVzZGF5IDYgRGVjZW1iZXIgKDIz
OjU5IEFvRSkqKjsKLSBOb3RpZmljYXRpb246IDIxIERlY2VtYmVyIDIwMjM7Ci0gV29ya3Nob3A6
IDE5IGFuZCAyMCBGZWJydWFyeSAyMDI0LgoKU3VibWlzc2lvbiB1cmw6IGh0dHBzOi8vZWFzeWNo
YWlyLm9yZy9jb25mZXJlbmNlcy8/Y29uZj1maWNzMjAyNAoKUmVnaXN0cmF0aW9uIHRvIHRoZSB3
b3Jrc2hvcCB3aWxsIGJlIGhhbmRsZWQgYnkgQ1NMIDIwMjQgKGRldGFpbHMgdG8gCmNvbWUpLiBP
bmxpbmUgcGFydGljaXBhdGlvbiB3aWxsIGJlIHBvc3NpYmxlIHdpdGggYSByZWR1Y2VkIHJlZ2lz
dHJhdGlvbiAKZmVlcywgYnV0IGF0IGxlYXN0IGFuIGF1dGhvciBvZiBlYWNoIGFic3RyYWN0IHdp
bGwgaGF2ZSB0byByZWdpc3RlciB3aXRoIApvbi1zaXRlIGZlZXMuCgoKPT0gQWJvdXQgRklDUyB3
b3Jrc2hvcCBzZXJpZXMgPT0KClRoZSBnb2FsIGlzIHRvIGJyaW5nIHRvZ2V0aGVyIHBlb3BsZSBm
cm9tIGRpZmZlcmVudCBzdWJmaWVsZHMgc3VjaCBhcyAKYWxnZWJyYS9jb2FsZ2VicmEsIHZlcmlm
aWNhdGlvbiwgbG9naWMsIGFyb3VuZCB0aGUgdGhlbWF0aWMgb2YgZml4ZWQgCnBvaW50cy4gRml4
ZWQgcG9pbnRzIHBsYXkgYSBmdW5kYW1lbnRhbCByb2xlIGluIHNldmVyYWwgYXJlYXMgb2YgCmNv
bXB1dGVyIHNjaWVuY2UuIFRoZXkgYXJlIHVzZWQgdG8ganVzdGlmeSAoY28pcmVjdXJzaXZlIGRl
ZmluaXRpb25zIGFuZCAKYXNzb2NpYXRlZCByZWFzb25pbmcgdGVjaG5pcXVlcy4gVGhlIGNvbnN0
cnVjdGlvbiBhbmQgcHJvcGVydGllcyBvZiAKZml4ZWQgcG9pbnRzIGhhdmUgYmVlbiBpbnZlc3Rp
Z2F0ZWQgaW4gbWFueSBkaWZmZXJlbnQgc2V0dGluZ3Mgc3VjaCBhczogCmRlc2lnbiBhbmQgaW1w
bGVtZW50YXRpb24gb2YgcHJvZ3JhbW1pbmcgbGFuZ3VhZ2VzLCBsb2dpY3MsIAp2ZXJpZmljYXRp
b24sIGRhdGFiYXNlcy4KVG9waWNzIGluY2x1ZGUsIGJ1dCBhcmUgbm90IHJlc3RyaWN0ZWQgdG86
Ci0gZml4ZWQgcG9pbnRzIGluIGFsZ2VicmEgYW5kIGNvYWxnZWJyYQotIGZpeGVkIHBvaW50cyBp
biBmb3JtYWwgbGFuZ3VhZ2VzIGFuZCBhdXRvbWF0YQotIGZpeGVkIHBvaW50cyBpbiBnYW1lIHRo
ZW9yeQotIGZpeGVkIHBvaW50cyBpbiBwcm9ncmFtbWluZyBsYW5ndWFnZSBzZW1hbnRpY3MKLSBm
aXhlZCBwb2ludHMgaW4gcHJvb2ZzCi0gZml4ZWQgcG9pbnRzIGluIHRoZSBtdS1jYWxjdWx1cyBh
bmQgbW9kYWwgbG9naWNzCi0gZml4ZWQgcG9pbnRzIGluIHByb2Nlc3MgYWxnZWJyYXMgYW5kIHBy
b2Nlc3MgY2FsY3VsaQotIGZpeGVkIHBvaW50cyBpbiBmdW5jdGlvbmFsIHByb2dyYW1taW5nIGFu
ZCB0eXBlIHRoZW9yeQotIGZpeGVkIHBvaW50cyBpbiByZWxhdGlvbiB0byBkYXRhZmxvdyBhbmQg
Y2lyY3VpdHMKLSBmaXhlZCBwb2ludHMgaW4gYXV0b21hdGVkIHRoZW9yZW0gcHJvdmluZywgaW50
ZXJhY3RpdmUgdGhlb3JlbSBwcm92aW5nIAphbmQgbG9naWMgcHJvZ3JhbW1pbmcKLSBmaXhlZCBw
b2ludHMgaW4gZmluaXRlIG1vZGVsIHRoZW9yeSwgZGVzY3JpcHRpdmUgY29tcGxleGl0eSB0aGVv
cnksIAphbmQgZGF0YWJhc2VzCi0gZml4ZWQgcG9pbnRzIGluIGNhdGVnb3J5IHRoZW9yeSBmb3Ig
bG9naWMgaW4gY29tcHV0ZXIgc2NpZW5jZQoKCj09IFR5cGVzIG9mIHN1Ym1pc3Npb25zID09CgpU
aGlzIHllYXIsIHdlIHdlbGNvbWUgdHdvIGNhdGVnb3JpZXMgb2Ygc3VibWlzc2lvbnMsIHNob3J0
IGFic3RyYWN0cyBhcyAKd2VsbCBhcyBleHRlbmRlZCBhYnN0cmFjdHM6CgotIEJvdGggdHlwZXMg
b2Ygc3VibWlzc2lvbnMgd2lsbCBiZSBoYW5kbGVkIHZpYSBFYXN5Y2hhaXIgYW5kIHdpbGwgYmUg
CnBlZXItcmV2aWV3ZWQgYnkgdGhlIFBDLgotIEluIG9yZGVyIHRvIHN1Ym1pdCBhIHNob3J0IG9y
IGV4dGVuZGVkIGFic3RyYWN0IHRvIEZJQ1MsIHBsZWFzZSB2aXNpdCAKdGhlIGZvbGxvd2luZyBs
aW5rOgogICAgICAgICBodHRwczovL2Vhc3ljaGFpci5vcmcvY29uZmVyZW5jZXMvP2NvbmY9Zmlj
czIwMjQKLSBBIHByb2NlZWRpbmdzIHZvbHVtZSBnYXRoZXJpbmcgdGhlIGV4dGVuZGVkIGFic3Ry
YWN0cyB3aWxsIGJlIApwdWJsaXNoZWQgYnkgRVBUQ1Mgc2hvcnRseSBhZnRlciB0aGUgd29ya3No
b3AgKHNlZSBkZXRhaWxzIGJlbG93KS4KCkhlcmUgYXJlIGRldGFpbHMgb24gZWFjaCB0eXBlIG9m
IHN1Ym1pc3Npb246CgotICoqc2hvcnQgYWJzdHJhY3RzKiogYXJlIGFic3RyYWN0cyBvZiAqKjMg
dG8gNSBwYWdlcywgcmVmZXJlbmNlcyAKaW5jbHVkZWQqKiwgZGVzY3JpYmluZyB0aGUgdG9waWMg
b2YgdGhlIHByb3Bvc2VkIGNvbnRyaWJ1dGVkIHRhbGsuIFRoZXkgCm1heSBjb250YWluIChpKSBu
ZXcgY29tcGxldGVkIHJlc3VsdHMsIChpaSkgd29yayBpbiBwcm9ncmVzcyBvciAoaWlpKSAKYWxy
ZWFkeSAocmVjZW50bHkpIHB1Ymxpc2hlZCBvciBzdWJtaXR0ZWQgd29ya3MuIFRoZSBzdWJtaXNz
aW9uIGNhbiAKcmVmZXIgdG8gYSBwdWJsaXNoZWQgcGFwZXIgb3IgYSBwcmVwcmludCBidXQgdGhl
IGRlc2NyaXB0aW9uIGdpdmVuIGluIAp0aGUgc2hvcnQgYWJzdHJhY3Qgc2hvdWxkIGJlIHN1ZmZp
Y2llbnRseSBkZXRhaWxlZCBmb3IgdGhlIFBDIHRvIGp1ZGdlIAp0aGUgcmVsZXZhbmNlIG9mIHRo
ZSBwcm9wb3NlZCB0YWxrIHRvIHRoZSB3b3Jrc2hvcCBwcm9ncmFtLgoKLSAqKmV4dGVuZGVkIGFi
c3RyYWN0cyoqIGFyZSBwYXBlcnMgb2YgKio2IHRvIDEwIHBhZ2VzLCByZWZlcmVuY2VzIApleGNs
dWRlZCoqLCBkZXNjcmliaW5nIG9yaWdpbmFsIHJlc3VsdHMgd2hpY2ggaGF2ZSBub3QgYmVlbiBw
dWJsaXNoZWQgCm5vciBhcmUgY3VycmVudGx5IHN1Ym1pdHRlZCBlbHNld2hlcmUuIFRoZSByZXN1
bHRzIG11c3QgYmUgcHJlc2VudGVkIGluIApzdWZmaWNpZW50IGRldGFpbHMgdG8gY29uc3RpdHV0
ZSBhIHNjaWVudGlmaWMgcHVibGljYXRpb24uIEFuIGFwcGVuZGl4IApjYW4gcHJvdmlkZSBhZGRp
dGlvbmFsIGRldGFpbHMgZm9yIHRoZSByZXZpZXdlciBidXQgd2lsbCBiZSByZWFkIGF0IHRoZSAK
ZGlzY3JldGlvbiBvZiB0aGUgcmV2aWV3ZXJzLgpBIHZvbHVtZSBvZiBwcm9jZWVkaW5ncyBjb250
YWluaW5nIHRoZSAqKmV4dGVuZGVkIGFic3RyYWN0cyoqIHdpbGwgYmUgCnB1Ymxpc2hlZCBzb29u
IGFmdGVyIHRoZSB3b3Jrc2hvcCBieSBFUFRDUzogdGhlIGF1dGhvcnMgb2YgZXh0ZW5kZWQgCmFi
c3RyYWN0cyB3aWxsIGJlIGFza2VkIHRvIHN1Ym1pdCBhIHJldmlzZWQgdmVyc2lvbiBmZXcgd2Vl
a3MgYWZ0ZXIgdGhlIApldmVudCwgYWxsb3dpbmcgdGhlbSB0byB0YWtlIGludG8gYWNjb3VudCB0
aGUgd29ya3Nob3AgZGlzY3Vzc2lvbnMuIApEZXRhaWxzIHdpbGwgYmUgcmVsZWFzZWQgbGF0ZXIu
CgoKPT0gSW52aXRlZCBzcGVha2VycwoKLSBBbnVwYW0gRGFzLCBVbml2ZXJzaXR5IG9mIEJpcm1p
bmdoYW0KLSBCYXJiYXJhIEvDtm5pZywgVW5pdmVyc2l0w6R0IER1aXNidXJnLUVzc2VuIChqb2lu
dCBDU0wgJiBGSUNTIGludml0ZWQgCnNwZWFrZXIpCgoKPT0gUHJvZ3JhbSBDb21taXR0ZWUgPT0K
Ci0gWmVuYSBBcmlvbGEgKFVuaXZlcnNpdHkgb2YgT3JlZ29uLCBVU0EpCi0gQWJoaXNoZWsgRGUg
KFVuaXZlcnNpdHkgb2YgQmlybWluZ2hhbSwgVUspCi0gWmVpbmFiIEdhbGFsIChVbml2ZXJzaXTD
oCBkZWdsaSBzdXRkaSBkaSBCb2xvZ25hLCBJdGFseSkKLSBHdWlsaGVtIEphYmVyIChVbml2ZXJz
aXTDqSBkZSBOYW50ZXMsIEZyYW5jZSkKLSBFa2F0ZXJpbmEgS29tZW5kYW50c2theWEgKEhlcmlv
dC1XYXR0IFVuaXZlcnNpdHksIFVLKQotIERlbmlzIEt1cGVyYmVyZyAoQ05SUyAmIEVOUyBMeW9u
LCBGcmFuY2UpCi0gTWFydGluIExhbmdlIChVbml2ZXJzaXR5IG9mIEthc3NlbCwgR2VybWFueSkK
LSBDaHJpc3RpbmUgUGF1bGluLU1vaHJpbmcgKFVuaXZlcnNpdMOpIFBhcmlzIFNhY2xheSwgRnJh
bmNlKQotIERhbmllbGEgUGV0cmlzYW4gKFVuaXZlcnNpdMOpIFBhcmlzIENpdMOpLCBGcmFuY2Up
Ci0gQWxleGlzIFNhdXJpbiAoQ05SUyAmIFVuaXZlcnNpdMOpIFBhcmlzIENpdMOpLCBGcmFuY2Up
LCBQQyBDaGFpcgotIFRob21hcyBTdHVkZXIgKFVuaXZlcnNpdHkgb2YgQmVybiwgU3dpdHplcmxh
bmQpCi0gVGFybW8gVXVzdGFsdSAoUmV5a2phdmlrIFVuaXZlcnNpdHksIEljZWxhbmQpCi0gWWRl
IFZlbmVtYSAoVW5pdmVyc2l0eSBvZiBBbXN0ZXJkYW0sIE5ldGhlcmxhbmQpCgoKPT0gSm91cm5h
bCBwdWJsaWNhdGlvbiA9PQoKRGVwZW5kaW5nIG9uIHRoZSBudW1iZXIgYW5kIHF1YWxpdHkgb2Yg
c3VibWlzc2lvbnMsIHdlIHdpbGwgcGxhbiBhIApzdWJzZXF1ZW50IHNwZWNpYWwgaXNzdWUgb2Yg
YSBqb3VybmFsLCBhcyBvZnRlbiBkb25lIGZvciBwcmV2aW91cyAKZWRpdGlvbnMgb2YgdGhlIHdv
cmtzaG9wLgoKCj09IENvbnRhY3QgPT0KCkFsZXhpcyBTYXVyaW4sIGFsZXhpcy5zYXVyaW5AaXJp
Zi5mcgpodHRwczovL3d3dy5pcmlmLmZyL3VzZXJzL3NhdXJpbi9pbmRleApfX19fX19fX19fX19f
X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fXwpBZ2RhIG1haWxpbmcgbGlzdApBZ2Rh
QGxpc3RzLmNoYWxtZXJzLnNlCmh0dHBzOi8vbGlzdHMuY2hhbG1lcnMuc2UvbWFpbG1hbi9saXN0
aW5mby9hZ2RhCg==