Third Call for Contributions - FICS Workshop (submission deadline: 1st December 2023)
Alexis Saurin <[email protected]> Fri, 24 Nov 2023 16:39:28 +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]> |
CihBcG9sb2dpZXMgZm9yIG11bHRpcGxlIHBvc3RpbmdzKQoKUGxlYXNlIGZpbmQgYmVsb3cgYW4g dXBkYXRlZCBjYWxsIGZvciBjb250cmlidXRpb25zIGZvciBGSUNTIHdvcmtzaG9wLgpTb21lIG5l d3M6CiAgKiBTdWJtaXNzaW9uIGRlYWRsaW5lIGluIG9uZSB3ZWVrIGZyb20gbm93IQogICogSW52 aXRlZCBzcGVha2VycyBhbm5vdW5jZWQgYmVsb3c7CiAgKiBXb3Jrc2hvcCBwcm9jZWVkaW5ncyBj b250YWluaW5nIHRoZSBleHRlbmRlZCBhYnN0cmFjdHMgd2lsbCBiZSAKcHVibGlzaGVkIGFzIGFu IEVQVENTIHZvbHVtZS4KClNpbmNlcmVseSwKCkFsZXhpcyBTYXVyaW4KSVJJRiAtLSBDTlJTLCBV bml2ZXJzaXTDqSBQYXJpcyBDaXTDqSAmIElOUklBIFBpY3ViZQpodHRwczovL3d3dy5pcmlmLmZy L3VzZXJzL3NhdXJpbi9maWNzMjAyNC9pbmRleC5odG1sCgoKPT09IFRoaXJkIENhbGwgZm9yIENv bnRyaWJ1dGlvbnMgPT09CgoxMnRoIEludGVybmF0aW9uYWwgV29ya3Nob3Agb24gRml4ZWQgUG9p bnRzIGluIENvbXB1dGVyIFNjaWVuY2UKMTkgJiAyMCBGZWJydWFyeSAyMDI0LCBOYXBsZXMsIEl0 YWx5Cmh0dHBzOi8vd3d3LmlyaWYuZnIvdXNlcnMvc2F1cmluL2ZpY3MyMDI0L2luZGV4Lmh0bWwK Ck5leHQgZWRpdGlvbiBvZiBGSUNTIHdvcmtzaG9wICgxMnRoIFdvcmtzaG9wIG9uIEZpeGVkIFBv aW50cyBpbiBDb21wdXRlciAKU2NpZW5jZSkgd2lsbCB0YWtlIHBsYWNlIGluIE5hcGxlcyBvbiB0 aGUgMTl0aCBhbmQgMjB0aCBvZiBGZWJydWFyeSwgCjIwMjQsIGFmZmlsaWF0ZWQgd2l0aCBDU0wg MjAyNCAoaHR0cHM6Ly9jc2wyMDI0LmdpdGh1Yi5pby9Ib21lLykuCgoKPT0gSW1wb3J0YW50IGRh dGVzIGFuZCBwcmFjdGljYWwgZGV0YWlscz09CgotIFN1Ym1pc3Npb24gZGVhZGxpbmUgZm9yIHNo b3J0IGFuZCBleHRlbmRlZCBhYnN0cmFjdHM6ICoqMSBEZWNlbWJlciAKMjAyMyoqIChzdWJtaXNz aW9uIHVybDogCmh0dHBzOi8vZWFzeWNoYWlyLm9yZy9jb25mZXJlbmNlcy8/Y29uZj1maWNzMjAy NCk7Ci0gTm90aWZpY2F0aW9uOiAyMSBEZWNlbWJlciAyMDIzOwotIFdvcmtzaG9wOiAxOSBhbmQg MjAgRmVicnVhcnkgMjAyNC4KClJlZ2lzdHJhdGlvbiB0byB0aGUgd29ya3Nob3Agd2lsbCBiZSBo YW5kbGVkIGJ5IENTTCAyMDI0IChkZXRhaWxzIHRvIApjb21lKS4gT25saW5lIHBhcnRpY2lwYXRp b24gd2lsbCBiZSBwb3NzaWJsZSB3aXRoIGEgcmVkdWNlZCByZWdpc3RyYXRpb24gCmZlZXMsIGJ1 dCBhdCBsZWFzdCBhbiBhdXRob3Igb2YgZWFjaCBhYnN0cmFjdCB3aWxsIGhhdmUgdG8gcmVnaXN0 ZXIgd2l0aCAKb24tc2l0ZSBmZWVzLgoKCj09IEFib3V0IEZJQ1Mgd29ya3Nob3Agc2VyaWVzID09 CgpUaGUgZ29hbCBpcyB0byBicmluZyB0b2dldGhlciBwZW9wbGUgZnJvbSBkaWZmZXJlbnQgc3Vi ZmllbGRzIHN1Y2ggYXMgCmFsZ2VicmEvY29hbGdlYnJhLCB2ZXJpZmljYXRpb24sIGxvZ2ljLCBh cm91bmQgdGhlIHRoZW1hdGljIG9mIGZpeGVkIApwb2ludHMuIEZpeGVkIHBvaW50cyBwbGF5IGEg ZnVuZGFtZW50YWwgcm9sZSBpbiBzZXZlcmFsIGFyZWFzIG9mIApjb21wdXRlciBzY2llbmNlLiBU aGV5IGFyZSB1c2VkIHRvIGp1c3RpZnkgKGNvKXJlY3Vyc2l2ZSBkZWZpbml0aW9ucyBhbmQgCmFz c29jaWF0ZWQgcmVhc29uaW5nIHRlY2huaXF1ZXMuIFRoZSBjb25zdHJ1Y3Rpb24gYW5kIHByb3Bl cnRpZXMgb2YgCmZpeGVkIHBvaW50cyBoYXZlIGJlZW4gaW52ZXN0aWdhdGVkIGluIG1hbnkgZGlm ZmVyZW50IHNldHRpbmdzIHN1Y2ggYXM6IApkZXNpZ24gYW5kIGltcGxlbWVudGF0aW9uIG9mIHBy b2dyYW1taW5nIGxhbmd1YWdlcywgbG9naWNzLCAKdmVyaWZpY2F0aW9uLCBkYXRhYmFzZXMuClRv cGljcyBpbmNsdWRlLCBidXQgYXJlIG5vdCByZXN0cmljdGVkIHRvOgotIGZpeGVkIHBvaW50cyBp biBhbGdlYnJhIGFuZCBjb2FsZ2VicmEKLSBmaXhlZCBwb2ludHMgaW4gZm9ybWFsIGxhbmd1YWdl cyBhbmQgYXV0b21hdGEKLSBmaXhlZCBwb2ludHMgaW4gZ2FtZSB0aGVvcnkKLSBmaXhlZCBwb2lu dHMgaW4gcHJvZ3JhbW1pbmcgbGFuZ3VhZ2Ugc2VtYW50aWNzCi0gZml4ZWQgcG9pbnRzIGluIHBy b29mcwotIGZpeGVkIHBvaW50cyBpbiB0aGUgbXUtY2FsY3VsdXMgYW5kIG1vZGFsIGxvZ2ljcwot IGZpeGVkIHBvaW50cyBpbiBwcm9jZXNzIGFsZ2VicmFzIGFuZCBwcm9jZXNzIGNhbGN1bGkKLSBm aXhlZCBwb2ludHMgaW4gZnVuY3Rpb25hbCBwcm9ncmFtbWluZyBhbmQgdHlwZSB0aGVvcnkKLSBm aXhlZCBwb2ludHMgaW4gcmVsYXRpb24gdG8gZGF0YWZsb3cgYW5kIGNpcmN1aXRzCi0gZml4ZWQg cG9pbnRzIGluIGF1dG9tYXRlZCB0aGVvcmVtIHByb3ZpbmcsIGludGVyYWN0aXZlIHRoZW9yZW0g cHJvdmluZyAKYW5kIGxvZ2ljIHByb2dyYW1taW5nCi0gZml4ZWQgcG9pbnRzIGluIGZpbml0ZSBt b2RlbCB0aGVvcnksIGRlc2NyaXB0aXZlIGNvbXBsZXhpdHkgdGhlb3J5LCAKYW5kIGRhdGFiYXNl cwotIGZpeGVkIHBvaW50cyBpbiBjYXRlZ29yeSB0aGVvcnkgZm9yIGxvZ2ljIGluIGNvbXB1dGVy IHNjaWVuY2UKCgo9PSBUeXBlcyBvZiBzdWJtaXNzaW9ucyA9PQoKVGhpcyB5ZWFyLCB3ZSB3ZWxj b21lIHR3byBjYXRlZ29yaWVzIG9mIHN1Ym1pc3Npb25zLCBzaG9ydCBhYnN0cmFjdHMgYXMgCndl bGwgYXMgZXh0ZW5kZWQgYWJzdHJhY3RzOgoKLSBCb3RoIHR5cGVzIG9mIHN1Ym1pc3Npb25zIHdp bGwgYmUgaGFuZGxlZCB2aWEgRWFzeWNoYWlyIGFuZCB3aWxsIGJlIApwZWVyLXJldmlld2VkIGJ5 IHRoZSBQQy4KLSBJbiBvcmRlciB0byBzdWJtaXQgYSBzaG9ydCBvciBleHRlbmRlZCBhYnN0cmFj dCB0byBGSUNTLCBwbGVhc2UgdmlzaXQgCnRoZSBmb2xsb3dpbmcgbGluazoKICAgICAgICAgaHR0 cHM6Ly9lYXN5Y2hhaXIub3JnL2NvbmZlcmVuY2VzLz9jb25mPWZpY3MyMDI0Ci0gQSBwcm9jZWVk aW5ncyB2b2x1bWUgZ2F0aGVyaW5nIHRoZSBleHRlbmRlZCBhYnN0cmFjdHMgd2lsbCBiZSAKcHVi bGlzaGVkIGJ5IEVQVENTIHNob3J0bHkgYWZ0ZXIgdGhlIHdvcmtzaG9wIChzZWUgZGV0YWlscyBi ZWxvdykuCgpIZXJlIGFyZSBkZXRhaWxzIG9uIGVhY2ggdHlwZSBvZiBzdWJtaXNzaW9uOgoKLSAq KnNob3J0IGFic3RyYWN0cyoqIGFyZSBhYnN0cmFjdHMgb2YgKiozIHRvIDUgcGFnZXMsIHJlZmVy ZW5jZXMgCmluY2x1ZGVkKiosIGRlc2NyaWJpbmcgdGhlIHRvcGljIG9mIHRoZSBwcm9wb3NlZCBj b250cmlidXRlZCB0YWxrLiBUaGV5IAptYXkgY29udGFpbiAoaSkgbmV3IGNvbXBsZXRlZCByZXN1 bHRzLCAoaWkpIHdvcmsgaW4gcHJvZ3Jlc3Mgb3IgKGlpaSkgCmFscmVhZHkgKHJlY2VudGx5KSBw dWJsaXNoZWQgb3Igc3VibWl0dGVkIHdvcmtzLiBUaGUgc3VibWlzc2lvbiBjYW4gCnJlZmVyIHRv IGEgcHVibGlzaGVkIHBhcGVyIG9yIGEgcHJlcHJpbnQgYnV0IHRoZSBkZXNjcmlwdGlvbiBnaXZl biBpbiAKdGhlIHNob3J0IGFic3RyYWN0IHNob3VsZCBiZSBzdWZmaWNpZW50bHkgZGV0YWlsZWQg Zm9yIHRoZSBQQyB0byBqdWRnZSAKdGhlIHJlbGV2YW5jZSBvZiB0aGUgcHJvcG9zZWQgdGFsayB0 byB0aGUgd29ya3Nob3AgcHJvZ3JhbS4KCi0gKipleHRlbmRlZCBhYnN0cmFjdHMqKiBhcmUgcGFw ZXJzIG9mICoqNiB0byAxMCBwYWdlcywgcmVmZXJlbmNlcyAKZXhjbHVkZWQqKiwgZGVzY3JpYmlu ZyBvcmlnaW5hbCByZXN1bHRzIHdoaWNoIGhhdmUgbm90IGJlZW4gcHVibGlzaGVkIApub3IgYXJl IGN1cnJlbnRseSBzdWJtaXR0ZWQgZWxzZXdoZXJlLiBUaGUgcmVzdWx0cyBtdXN0IGJlIHByZXNl bnRlZCBpbiAKc3VmZmljaWVudCBkZXRhaWxzIHRvIGNvbnN0aXR1dGUgYSBzY2llbnRpZmljIHB1 YmxpY2F0aW9uLiBBbiBhcHBlbmRpeCAKY2FuIHByb3ZpZGUgYWRkaXRpb25hbCBkZXRhaWxzIGZv ciB0aGUgcmV2aWV3ZXIgYnV0IHdpbGwgYmUgcmVhZCBhdCB0aGUgCmRpc2NyZXRpb24gb2YgdGhl IHJldmlld2Vycy4KQSB2b2x1bWUgb2YgcHJvY2VlZGluZ3MgY29udGFpbmluZyB0aGUgKipleHRl bmRlZCBhYnN0cmFjdHMqKiB3aWxsIGJlIApwdWJsaXNoZWQgc29vbiBhZnRlciB0aGUgd29ya3No b3AgYnkgRVBUQ1M6IHRoZSBhdXRob3JzIG9mIGV4dGVuZGVkIAphYnN0cmFjdHMgd2lsbCBiZSBh c2tlZCB0byBzdWJtaXQgYSByZXZpc2VkIHZlcnNpb24gZmV3IHdlZWtzIGFmdGVyIHRoZSAKZXZl bnQsIGFsbG93aW5nIHRoZW0gdG8gdGFrZSBpbnRvIGFjY291bnQgdGhlIHdvcmtzaG9wIGRpc2N1 c3Npb25zLiAKRGV0YWlscyB3aWxsIGJlIHJlbGVhc2VkIGxhdGVyLgoKCj09IEludml0ZWQgc3Bl YWtlcnMKCi0gQW51cGFtIERhcywgVW5pdmVyc2l0eSBvZiBCaXJtaW5naGFtCi0gQmFyYmFyYSBL w7ZuaWcsIFVuaXZlcnNpdMOkdCBEdWlzYnVyZy1Fc3NlbiAoam9pbnQgQ1NMICYgRklDUyBpbnZp dGVkIApzcGVha2VyKQoKCj09IFByb2dyYW0gQ29tbWl0dGVlID09CgotIFplbmEgQXJpb2xhIChV bml2ZXJzaXR5IG9mIE9yZWdvbiwgVVNBKQotIEFiaGlzaGVrIERlIChVbml2ZXJzaXR5IG9mIEJp cm1pbmdoYW0sIFVLKQotIFplaW5hYiBHYWxhbCAoVW5pdmVyc2l0w6AgZGVnbGkgc3V0ZGkgZGkg Qm9sb2duYSwgSXRhbHkpCi0gR3VpbGhlbSBKYWJlciAoVW5pdmVyc2l0w6kgZGUgTmFudGVzLCBG cmFuY2UpCi0gRWthdGVyaW5hIEtvbWVuZGFudHNrYXlhIChIZXJpb3QtV2F0dCBVbml2ZXJzaXR5 LCBVSykKLSBEZW5pcyBLdXBlcmJlcmcgKENOUlMgJiBFTlMgTHlvbiwgRnJhbmNlKQotIE1hcnRp biBMYW5nZSAoVW5pdmVyc2l0eSBvZiBLYXNzZWwsIEdlcm1hbnkpCi0gQ2hyaXN0aW5lIFBhdWxp bi1Nb2hyaW5nIChVbml2ZXJzaXTDqSBQYXJpcyBTYWNsYXksIEZyYW5jZSkKLSBEYW5pZWxhIFBl dHJpc2FuIChVbml2ZXJzaXTDqSBQYXJpcyBDaXTDqSwgRnJhbmNlKQotIEFsZXhpcyBTYXVyaW4g KENOUlMgJiBVbml2ZXJzaXTDqSBQYXJpcyBDaXTDqSwgRnJhbmNlKSwgUEMgQ2hhaXIKLSBUaG9t YXMgU3R1ZGVyIChVbml2ZXJzaXR5IG9mIEJlcm4sIFN3aXR6ZXJsYW5kKQotIFRhcm1vIFV1c3Rh bHUgKFJleWtqYXZpayBVbml2ZXJzaXR5LCBJY2VsYW5kKQotIFlkZSBWZW5lbWEgKFVuaXZlcnNp dHkgb2YgQW1zdGVyZGFtLCBOZXRoZXJsYW5kKQoKCj09IEpvdXJuYWwgcHVibGljYXRpb24gPT0K CkRlcGVuZGluZyBvbiB0aGUgbnVtYmVyIGFuZCBxdWFsaXR5IG9mIHN1Ym1pc3Npb25zLCB3ZSB3 aWxsIHBsYW4gYSAKc3Vic2VxdWVudCBzcGVjaWFsIGlzc3VlIG9mIGEgam91cm5hbCwgYXMgb2Z0 ZW4gZG9uZSBmb3IgcHJldmlvdXMgCmVkaXRpb25zIG9mIHRoZSB3b3Jrc2hvcC4KCgo9PSBDb250 YWN0ID09CgpBbGV4aXMgU2F1cmluLCBhbGV4aXMuc2F1cmluQGlyaWYuZnIKaHR0cHM6Ly93d3cu aXJpZi5mci91c2Vycy9zYXVyaW4vaW5kZXgKX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f X19fX19fX19fX19fX19fX18KQWdkYSBtYWlsaW5nIGxpc3QKQWdkYUBsaXN0cy5jaGFsbWVycy5z ZQpodHRwczovL2xpc3RzLmNoYWxtZXJzLnNlL21haWxtYW4vbGlzdGluZm8vYWdkYQo=