TYPES 2025: Call for Participation
Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg-3oVnsloLHoGFxr2TtlUqVg@public.gmane.org> Wed, 23 Apr 2025 15:46:33 +0100
| Newsgroups | gmane.comp.lang.agda,gmane.comp.science.types.announce,gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.prooftheory |
|---|---|
| Message-ID | <[email protected]> |
IMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIENhbGwgZm9yIFBhcnRpY2lwYXRpb24K CiDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgVFlQRVMgMjAyNQog wqDCoMKgwqDCoMKgwqDCoMKgwqAgMzFzdCBJbnRlcm5hdGlvbmFsIENvbmZlcmVuY2Ugb24KIMKg wqDCoMKgwqDCoMKgwqDCoMKgwqDCoCBUeXBlcyBmb3IgUHJvb2ZzIGFuZCBQcm9ncmFtcwoKIMKg wqDCoMKgwqDCoMKgwqAgR2xhc2dvdywgU2NvdGxhbmQsIDkgLS0gMTMgSnVuZSAyMDI1CiDCoMKg wqDCoMKgwqDCoCBodHRwczovL21zcC5jaXMuc3RyYXRoLmFjLnVrL3R5cGVzMjAyNS8KClJFR0lT VFJBVElPTgotLS0tLS0tLS0tLS0KClJlZ2lzdHJhdGlvbiBpcyBub3cgb3Blbjsgc2VlIApodHRw czovL21zcC5jaXMuc3RyYXRoLmFjLnVrL3R5cGVzMjAyNS9yZWdpc3RyYXRpb24uaHRtbApmb3Ig bW9yZSBpbmZvcm1hdGlvbi4KCiogRWFybHkgcmVnaXN0cmF0aW9uIHVudGlsIDEyIE1heQoqIExh dGUgcmVnaXN0cmF0aW9uIHVudGlsIDMwIE1heQoKU3R1ZGVudHMgY2FuIHJlZ2lzdGVyIGF0IGEg cmVkdWNlZCBmZWUuIEZvciBkZXRhaWxzLCBzZWUgdGhlIGFib3ZlIGxpbmsuCgpSZXNlYXJjaGVy cyBmcm9tIENPU1QgSW5jbHVzaXZlbmVzcyBUYXJnZXQgQ291bnRyaWVzIGFyZSByZW1pbmRlZCB0 aGF0CnRoZSBFdXJvcGVhbiBSZXNlYXJjaCBOZXR3b3JrIG9uIEZvcm1hbCBQcm9vZnMgQ09TVCBh Y3Rpb24gaGFzIHNvbWUKZnVuZGluZyBhdmFpbGFibGUgZm9yIGNvbmZlcmVuY2UgYXR0ZW5kYW5j ZSwgd2l0aCBhIGRlYWRsaW5lIG9mIDQgTWF5LCBzZWUKaHR0cHM6Ly9ldXJvcHJvb2ZuZXQuZ2l0 aHViLmlvL2dyYW50cy8gLgoKCklOVklURUQgU1BFQUtFUlMKLS0tLS0tLS0tLS0tLS0tLQoKSW5n byBCbGVjaHNjaG1pZHQgKFVuaXZlcnNpdHkgb2YgQW50d2VycCkKU29uaWEgTWFyaW4gKFVuaXZl cnNpdHkgb2YgQmlybWluZ2hhbSkKQ2hyaXMgTWFydGVucyAoTm9ydGhlYXN0ZXJuIFVuaXZlcnNp dHkpCkNocmlzdGlhbiBTYXR0bGVyIChDaGFsbWVycyBVbml2ZXJzaXR5IG9mIFRlY2hub2xvZ3kg YW5kIFVuaXZlcnNpdHkgb2YgCkdvdGhlbmJ1cmcpCgoKQ09OVFJJQlVURUQgVEFMS1MKLS0tLS0t LS0tLS0tLS0tLS0KCkEgbGlzdCBvZiBhY2NlcHRlZCBjb250cmlidXRlZCB0YWxrcyBjYW4gYmUg Zm91bmQgYXQgCmh0dHBzOi8vbXNwLmNpcy5zdHJhdGguYWMudWsvdHlwZXMyMDI1L2FjY2VwdGVk Lmh0bWwgLgoKCkNPTE9DQVRFRCBFVkVOVFMKLS0tLS0tLS0tLS0tLS0tLQoKKiAxMCBKdW5lOiBX b21lbiBpbiBFdXJvUHJvb2ZOZXQgCihodHRwczovL2V1cm9wcm9vZm5ldC5naXRodWIuaW8vd29t ZW4tZXBuLTIwMjUvICkKKiAxNiAtLSAyMCBKdW5lOiBDQUxDTyAyMDI1ICYgTUZQUyBYTEkgCiho dHRwczovL3d3dy5jb2FsZy5vcmcvY2FsY28tbWZwcy0yMDI1LyApCgoKQkFDS0dST1VORAotLS0t LS0tLS0tCgpUaGUgVFlQRVMgbWVldGluZ3MgYXJlIGEgZm9ydW0gdG8gcHJlc2VudCBuZXcgYW5k IG9uZ29pbmcgd29yayBpbiBhbGwKYXNwZWN0cyBvZiB0eXBlIHRoZW9yeSBhbmQgaXRzIGFwcGxp Y2F0aW9ucywgZXNwZWNpYWxseSBpbiBmb3JtYWxpc2VkCmFuZCBjb21wdXRlciBhc3Npc3RlZCBy ZWFzb25pbmcgYW5kIGNvbXB1dGVyIHByb2dyYW1taW5nLgoKVGhlIFRZUEVTIGFyZWFzIG9mIGlu dGVyZXN0IGluY2x1ZGUsIGJ1dCBhcmUgbm90IGxpbWl0ZWQgdG86CgoqIGZvdW5kYXRpb25zIG9m IHR5cGUgdGhlb3J5IGFuZCBjb25zdHJ1Y3RpdmUgbWF0aGVtYXRpY3M7CiogYXBwbGljYXRpb25z IG9mIHR5cGUgdGhlb3J5OwoqIGRlcGVuZGVudGx5IHR5cGVkIHByb2dyYW1taW5nOwoqIGluZHVz dHJpYWwgdXNlcyBvZiB0eXBlIHRoZW9yeSB0ZWNobm9sb2d5OwoqIG1ldGEtdGhlb3JldGljIHN0 dWRpZXMgb2YgdHlwZSBzeXN0ZW1zOwoqIHByb29mIGFzc2lzdGFudHMgYW5kIHByb29mIHRlY2hu b2xvZ3k7CiogYXV0b21hdGlvbiBpbiBjb21wdXRlci1hc3Npc3RlZCByZWFzb25pbmc7CiogbGlu a3MgYmV0d2VlbiB0eXBlIHRoZW9yeSBhbmQgZnVuY3Rpb25hbCBwcm9ncmFtbWluZzsKKiBmb3Jt YWxpemluZyBtYXRoZW1hdGljcyB1c2luZyB0eXBlIHRoZW9yeS4KCkluIHRoZSBzcGlyaXQgb2Yg d29ya3Nob3BzLCB0YWxrcyBtYXkgYmUgYmFzZWQgb24gbmV3bHkgcHVibGlzaGVkIHBhcGVycywK d29yayBzdWJtaXR0ZWQgZm9yIHB1YmxpY2F0aW9uLCBidXQgYWxzbyB3b3JrIGluIHByb2dyZXNz LiBQYXJ0aWNpcGF0aW9uCmluIHRoZSBtZWV0aW5nIGlzIHByaW1hcmlseSBpbiBwZXJzb24sIGFz IGZhY2UtdG8tZmFjZSBpbnRlcmFjdGlvbnMKYXJlIGhpZ2hseSB2YWx1YWJsZS4gSWYgeW91IG5l ZWQgdG8gZGlzY3VzcyByZW1vdGUgcGFydGljaXBhdGlvbiwKcGxlYXNlIGNvbnRhY3QgdGhlIG9y Z2FuaXNlcnMuCgoKVklTQSBJU1NVRVMKLS0tLS0tLS0tLS0KCk5vdGUgdGhhdCBldmVuIGlmIHlv dSBhcmUgbHVja3kgZW5vdWdoIHRvIG5vdCByZXF1aXJlIGEgdmlzYSB0byBlbnRlciAKdGhlIFVL LAp5b3UgbWlnaHQgc3RpbGwgbmVlZCB0byBhcHBseSBmb3IgZWxlY3Ryb25pYyB0cmF2ZWwgYXV0 aG9yaXNhdGlvbiAoRVRBKS4gCkluIHBhcnRpY3VsYXIsCnRoaXMgYXBwbGllcyB0byBFVSBjaXRp emVucy4gWW91IGNhbiBjaGVjayB3aGF0IHlvdSBuZWVkIGhlcmU6CgpodHRwczovL3d3dy5nb3Yu dWsvY2hlY2stdWstdmlzYQoKSWYgeW91IGRvIG5lZWQgYSB2aXNhLCB3ZSBhcmUgaGFwcHkgdG8g d3JpdGUgeW91IGEgbGV0dGVyIG9mIGludml0YXRpb24sCmNvbmZpcm1pbmcgdGhhdCB5b3UgaGF2 ZSByZWdpc3RlcmVkIGZvciB0aGUgY29uZmVyZW5jZS4gU2VlIHRoZSAKcmVnaXN0cmF0aW9uIHBh Z2UgZm9yCm1vcmUgZGV0YWlscy4KCgpTUE9OU09SUwotLS0tLS0tLQoKSmFuZSBTdHJlZXQgKEdv bGQgU3BvbnNvcikKRm9ybWFsIFZpbmRpY2F0aW9ucwpXZWxsLVR5cGVkCklPRwpUdW5ub2NrJ3Mg KENhcmFtZWwgV2FmZXIgc3BvbnNvcikKCgpQUk9HUkFNTUUgQ09NTUlUVEVFCi0tLS0tLS0tLS0t LS0tLS0tLS0KCkRhbmVsIEFobWFuIChVbml2ZXJzaXR5IG9mIFRhcnR1LCBFc3RvbmlhKQpHdWls bGF1bWUgQWxsYWlzIChVbml2ZXJzaXR5IG9mIFN0cmF0aGNseWRlLCBTY290bGFuZCkKTWFsaW4g QWx0ZW5tw7xsbGVyIChVbml2ZXJzaXR5IG9mIEVkaW5idXJnaCwgU2NvdGxhbmQpClNhbmRyYSBB bHZlcyAoVW5pdmVyc2l0eSBvZiBQb3J0bywgUG9ydHVnYWwpCkNhc3BlciBCYWNoIChVbml2ZXJz aXR5IG9mIFNvdXRoZXJuIERlbm1hcmssIERlbm1hcmspCkFuYSBCb3ZlIChDaGFsbWVycyBhbmQg VW5pdmVyc2l0eSBvZiBHb3RoZW5idXJnLCBTd2VkZW4pCkxpYW5nLVRpbmcgQ2hlbiAoQWNhZGVt aWEgU2luaWNhLCBUYWl3YW4pClZpa3JhbWFuIENob3VkaHVyeSAoVW5pdmVyc2l0eSBvZiBCb2xv Z25hLCBJdGFseSkKR2lsZGEgRmVycmVpcmEgKFVuaXZlcnNpZGFkZSBBYmVydGEsIFBvcnR1Z2Fs KQpEYW5pZWwgR3JhdHplciAoQWFyaHVzIFVuaXZlcnNpdHksIERlbm1hcmspClRvbSBkZSBKb25n IChVbml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0sIEVuZ2xhbmQpCkRvbWluaWsgS2lyc3QgKElucmlh IFBhcmlzLCBGcmFuY2UpCk5lZWwgS3Jpc2huYXN3YW1pIChVbml2ZXJzaXR5IG9mIENhbWJyaWRn ZSwgRW5nbGFuZCkKQW5kcsOhcyBLb3bDoWNzIChVbml2ZXJzaXR5IG9mIEdvdGhlbmJ1cmcgYW5k IENoYWxtZXJzLCBTd2VkZW4pClBldGVyIExlRmFudSBMdW1zZGFpbmUgKFN0b2NraG9sbSBVbml2 ZXJzaXR5LCBTd2VkZW4pCktlbmppIE1haWxsYXJkIChJbnJpYSBSZW5uZXMtQnJldGFnbmUgQXRs YW50aXF1ZSwgRnJhbmNlKQpNYXggTmV3IChVbml2ZXJzaXR5IG9mIE1pY2hpZ2FuLCBVbml0ZWQg U3RhdGVzIG9mIEFtZXJpY2EpCkZyZWRyaWsgTm9yZHZhbGwgRm9yc2JlcmcgKFVuaXZlcnNpdHkg b2YgU3RyYXRoY2x5ZGUsIFNjb3RsYW5kKSAoY2hhaXIpCkVsYWluZSBQaW1lbnRlbCAoVW5pdmVy c2l0eSBDb2xsZWdlIExvbmRvbiwgRW5nbGFuZCkKQW5kcmV3IFN3YW4gKFVuaXZlcnNpdHkgb2Yg TGp1YmxqYW5hLCBTbG92ZW5pYSkKVGFybW8gVXVzdGFsdSAoUmV5a2phdsOtayBVbml2ZXJzaXR5 LCBJY2VsYW5kKQpOaWVscyB2YW4gZGVyIFdlaWRlIChSYWRib3VkIFVuaXZlcnNpdHkgTmlqbWVn ZW4sIFRoZSBOZXRoZXJsYW5kcykKVGjDqW8gV2ludGVyaGFsdGVyIChJbnJpYSBTYWNsYXksIEZy YW5jZSkKTWFhaWtlIFp3YXJ0IChJVCBVbml2ZXJzaXR5IENvcGVuaGFnZW4sIERlbm1hcmspCgoK VFlQRVMgU1RFRVJJTkcgQ09NTUlUVEVFCi0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLQoKRWR1YXJk byBIZXJtbyBSZXllcyAoRm9ybWFsIFZpbmRpY2F0aW9ucywgU3BhaW4pClRvbSBkZSBKb25nIChV bml2ZXJzaXR5IG9mIE5vdHRpbmdoYW0sIEVuZ2xhbmQpClJhc211cyBFamxlcnMgTcO4Z2VsYmVy ZyAoSVQgVW5pdmVyc2l0eSBvZiBDb3BlbmhhZ2VuLCBEZW5tYXJrKQpGcmVkcmlrIE5vcmR2YWxs IEZvcnNiZXJnIChVbml2ZXJzaXR5IG9mIFN0cmF0aGNseWRlLCBTY290bGFuZCkKUGFpZ2UgUmFu ZGFsbCBOb3J0aCAoVXRyZWNodCBVbml2ZXJzaXR5LCBUaGUgTmV0aGVybGFuZHMpIChjaGFpcikK QmVubm8gdmFuIGRlbiBCZXJnIChVbml2ZXJzaXR5IG9mIEFtc3RlcmRhbSwgVGhlIE5ldGhlcmxh bmRzKSAoc2VjcmV0YXJ5KQoKCkFCT1VUIFRZUEVTCi0tLS0tLS0tLS0tCgpUaGUgVFlQRVMgbWVl dGluZ3MgZnJvbSAxOTkwIHRvIDIwMDggd2VyZSBhbm51YWwgd29ya3Nob3BzIG9mIGEgc2VxdWVu Y2UKb2YgZml2ZSBFVSBmdW5kZWQgbmV0d29ya2luZyBwcm9qZWN0cy4gRnJvbSAyMDA5IG9ud2Fy ZHMsIFRZUEVTIGhhcyBiZWVuCnJ1biBhcyBhbiBpbmRlcGVuZGVudCBjb25mZXJlbmNlIHNlcmll cy4gUHJldmlvdXMgVFlQRVMgbWVldGluZ3Mgd2VyZQpoZWxkIGluIEFudGliZXMgKDE5OTApLCBF ZGluYnVyZ2ggKDE5OTEpLCBCw6VzdGFkICgxOTkyKSwgTmlqbWVnZW4KKDE5OTMpLCBCw6VzdGFk ICgxOTk0KSwgVG9yaW5vICgxOTk1KSwgQXVzc29pcyAoMTk5NiksIEtsb3N0ZXIgSXJzZWUKKDE5 OTgpLCBMw7ZrZWJlcmcgKDE5OTkpLCBEdXJoYW0gKDIwMDApLCBCZXJnIGVuIERhbCBuZWFyIE5p am1lZ2VuCigyMDAyKSwgVG9yaW5vICgyMDAzKSwgSm91eS1lbi1Kb3NhcyBuZWFyIFBhcmlzICgy MDA0KSwgTm90dGluZ2hhbQooMjAwNiksIENpdmlkYWxlIGRlbCBGcml1bGkgKDIwMDcpLCBUb3Jp bm8gKDIwMDgpLCBBdXNzb2lzICgyMDA5KSwKV2Fyc2F3ICgyMDEwKSwgQmVyZ2VuICgyMDExKSwg VG91bG91c2UgKDIwMTMpLCBQYXJpcyAoMjAxNCksIFRhbGxpbm4KKDIwMTUpLCBOb3ZpIFNhZCAo MjAxNiksIEJ1ZGFwZXN0ICgyMDE3KSwgQnJhZ2EgKDIwMTgpLCBPc2xvICgyMDE5KSwKVmlydHVh bCAoMjAyMSksIE5hbnRlcyAoMjAyMiksIFZhbMOobmNpYSAoMjAyMyksIENvcGVuaGFnZW4gKDIw MjQpLgoKCkNPTlRBQ1QKLS0tLS0tLQoKRW1haWw6IENJU190eXBlczIwMjVAZ3JvdXBzLnN0cmF0 aC5hYy51awoKCk9SR0FOSVNFUlMKLS0tLS0tLS0tLQoKR3VpbGxhdW1lIEFsbGFpcyAoVW5pdmVy c2l0eSBvZiBTdHJhdGhjbHlkZSwgU2NvdGxhbmQpClN0dWFydCBHYWxlIChVbml2ZXJzaXR5IG9m IFN0cmF0aGNseWRlLCBTY290bGFuZCkKRnJlZHJpayBOb3JkdmFsbCBGb3JzYmVyZyAoVW5pdmVy c2l0eSBvZiBTdHJhdGhjbHlkZSwgU2NvdGxhbmQpCgoKCl9fX19fX19fX19fX19fX19fX19fX19f X19fX19fX19fX19fX19fX19fX19fX19fCkFnZGEgbWFpbGluZyBsaXN0CkFnZGFAbGlzdHMuY2hh bG1lcnMuc2UKaHR0cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGEK