TYPES 2025: Second Call for Contributions
Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg-3oVnsloLHoGFxr2TtlUqVg@public.gmane.org> Mon, 10 Feb 2025 11:12:57 +0000
| Newsgroups | gmane.comp.lang.agda,gmane.comp.science.types.announce,gmane.science.mathematics.logic.coq.club,gmane.science.mathematics.prooftheory |
|---|---|
| Message-ID | <[email protected]> |
W1RoZSBUWVBFUyAyMDI1IHN1Ym1pc3Npb24gZGVhZGxpbmUgaXMgbGVzcyB0aGFuIGEgbW9udGgg YXdheS5dCgogwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIFNlY29uZCBDYWxsIGZvciBDb250cmli dXRpb25zCgogwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIFRZUEVT IDIwMjUKIMKgwqDCoMKgwqDCoMKgwqDCoMKgIDMxc3QgSW50ZXJuYXRpb25hbCBDb25mZXJlbmNl IG9uCiDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqAgVHlwZXMgZm9yIFByb29mcyBhbmQgUHJvZ3Jh bXMKCiDCoMKgwqDCoMKgwqDCoMKgIEdsYXNnb3csIFNjb3RsYW5kLCA5IC0tIDEzIEp1bmUgMjAy NQogwqDCoMKgwqDCoMKgwqAgaHR0cHM6Ly9tc3AuY2lzLnN0cmF0aC5hYy51ay90eXBlczIwMjUv CgpPVkVSVklFVwotLS0tLS0tLQoKVGhlIFRZUEVTIG1lZXRpbmdzIGFyZSBhIGZvcnVtIHRvIHBy ZXNlbnQgbmV3IGFuZCBvbmdvaW5nIHdvcmsgaW4gYWxsCmFzcGVjdHMgb2YgdHlwZSB0aGVvcnkg YW5kIGl0cyBhcHBsaWNhdGlvbnMsIGVzcGVjaWFsbHkgaW4gZm9ybWFsaXNlZAphbmQgY29tcHV0 ZXIgYXNzaXN0ZWQgcmVhc29uaW5nIGFuZCBjb21wdXRlciBwcm9ncmFtbWluZy4KClRoZSBUWVBF UyBhcmVhcyBvZiBpbnRlcmVzdCBpbmNsdWRlLCBidXQgYXJlIG5vdCBsaW1pdGVkIHRvOgoKKiBm b3VuZGF0aW9ucyBvZiB0eXBlIHRoZW9yeSBhbmQgY29uc3RydWN0aXZlIG1hdGhlbWF0aWNzOwoq IGFwcGxpY2F0aW9ucyBvZiB0eXBlIHRoZW9yeTsKKiBkZXBlbmRlbnRseSB0eXBlZCBwcm9ncmFt bWluZzsKKiBpbmR1c3RyaWFsIHVzZXMgb2YgdHlwZSB0aGVvcnkgdGVjaG5vbG9neTsKKiBtZXRh LXRoZW9yZXRpYyBzdHVkaWVzIG9mIHR5cGUgc3lzdGVtczsKKiBwcm9vZiBhc3Npc3RhbnRzIGFu ZCBwcm9vZiB0ZWNobm9sb2d5OwoqIGF1dG9tYXRpb24gaW4gY29tcHV0ZXItYXNzaXN0ZWQgcmVh c29uaW5nOwoqIGxpbmtzIGJldHdlZW4gdHlwZSB0aGVvcnkgYW5kIGZ1bmN0aW9uYWwgcHJvZ3Jh bW1pbmc7CiogZm9ybWFsaXppbmcgbWF0aGVtYXRpY3MgdXNpbmcgdHlwZSB0aGVvcnkuCgpXZSBl bmNvdXJhZ2UgdGFsa3MgcHJvcG9zaW5nIG5ldyB3YXlzIG9mIGFwcGx5aW5nIHR5cGUgdGhlb3J5 LiBJbiB0aGUKc3Bpcml0IG9mIHdvcmtzaG9wcywgdGFsa3MgbWF5IGJlIGJhc2VkIG9uIG5ld2x5 IHB1Ymxpc2hlZCBwYXBlcnMsCndvcmsgc3VibWl0dGVkIGZvciBwdWJsaWNhdGlvbiwgYnV0IGFs c28gd29yayBpbiBwcm9ncmVzcy4gUGFydGljaXBhdGlvbgppbiB0aGUgbWVldGluZyBpcyBwcmlt YXJpbHkgaW4gcGVyc29uLCBhcyBmYWNlLXRvLWZhY2UgaW50ZXJhY3Rpb25zCmFyZSBoaWdobHkg dmFsdWFibGUuIElmIHlvdSBuZWVkIHRvIGRpc2N1c3MgcmVtb3RlIHBhcnRpY2lwYXRpb24sCnBs ZWFzZSBjb250YWN0IHRoZSBQQyBjaGFpci4KClJlc2VhcmNoZXJzIGZyb20gQ09TVCBJbmNsdXNp dmVuZXNzIFRhcmdldCBDb3VudHJpZXMgYXJlIHJlbWluZGVkIHRoYXQKdGhlIEV1cm9wZWFuIFJl c2VhcmNoIE5ldHdvcmsgb24gRm9ybWFsIFByb29mcyBDT1NUIGFjdGlvbiBoYXMgc29tZQpmdW5k aW5nIGF2YWlsYWJsZSBmb3IgY29uZmVyZW5jZSBhdHRlbmRhbmNlLCBzZWUKaHR0cHM6Ly9ldXJv cHJvb2ZuZXQuZ2l0aHViLmlvL2dyYW50cy8gLgoKQ09OVFJJQlVURUQgVEFMS1MKLS0tLS0tLS0t LS0tLS0tLS0KClRZUEVTIHNvbGljaXRzIGNvbnRyaWJ1dGVkIHRhbGtzIHRvIHN0aW11bGF0ZSBk aXNjdXNzaW9ucy4gU2VsZWN0aW9uCm9mIHRob3NlIHdpbGwgYmUgYmFzZWQgb24gZXh0ZW5kZWQg YWJzdHJhY3RzL3Nob3J0IHBhcGVycyBvZiAyIHBwIChub3QKY291bnRpbmcgdGhlIGJpYmxpb2dy YXBoeSkgZm9ybWF0dGVkIHdpdGggZWFzeWNoYWlyLmNscy4KClRoZSBzdWJtaXNzaW9uIHNpdGUg aXM6IApodHRwczovL29wZW5yZXZpZXcubmV0L2dyb3VwP2lkPVRZUEVTLzIwMjUvQ29uZmVyZW5j ZQoKSU1QT1JUQU5UIERBVEVTCi0tLS0tLS0tLS0tLS0tLQoKKiBTdWJtaXNzaW9uIG9mIDItcGFn ZSBhYnN0cmFjdMKgwqDCoMKgwqAgMyBNYXJjaCAyMDI1IEFvRQoqIEF1dGhvciBub3RpZmljYXRp b27CoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIDExIEFwcmlsIDIwMjUgQW9FCiogQ2FtZXJh LXJlYWR5IHZlcnNpb24gb2YgYWJzdHJhY3TCoMKgIDkgTWF5wqDCoCAyMDI1IEFvRQoqIENvbmZl cmVuY2XCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgwqDCoMKgIDkgLS0g MTMgSnVuZSAyMDI1CgpDYW1lcmEtcmVhZHkgdmVyc2lvbnMgb2YgdGhlIGFjY2VwdGVkIGNvbnRy aWJ1dGlvbnMgd2lsbCBiZSBwdWJsaXNoZWQKaW4gYW4gaW5mb3JtYWwgYm9vayBvZiBhYnN0cmFj dHMgZm9yIGRpc3RyaWJ1dGlvbiBkdXJpbmcgdGhlIGNvbmZlcmVuY2UuCgpJTlZJVEVEIFNQRUFL RVJTCi0tLS0tLS0tLS0tLS0tLS0KCkluZ28gQmxlY2hzY2htaWR0IChVbml2ZXJzaXR5IG9mIEF1 Z3NidXJnKQpTb25pYSBNYXJpbiAoVW5pdmVyc2l0eSBvZiBCaXJtaW5naGFtKQpDaHJpcyBNYXJ0 ZW5zIChOb3J0aGVhc3Rlcm4gVW5pdmVyc2l0eSkKQ2hyaXN0aWFuIFNhdHRsZXIgKENoYWxtZXJz IFVuaXZlcnNpdHkgb2YgVGVjaG5vbG9neSBhbmQgVW5pdmVyc2l0eSBvZiAKR290aGVuYnVyZykK ClBPU1QtUFJPQ0VFRElOR1MKLS0tLS0tLS0tLS0tLS0tLQoKQSBwb3N0LXByb2NlZWRpbmdzIHZv bHVtZSB3aWxsIGJlIHB1Ymxpc2hlZCBpbiB0aGUgTGVpYm5peiBJbnRlcm5hdGlvbmFsClByb2Nl ZWRpbmdzIGluIEluZm9ybWF0aWNzIChMSVBJY3MpIHNlcmllcy4gU3VibWlzc2lvbiB0byB0aGF0 IHZvbHVtZQp3aWxsIGJlIG9wZW4gdG8gZXZlcnlvbmUuCgpUZW50YXRpdmUgc3VibWlzc2lvbiBk ZWFkbGluZSBmb3IgdGhlIHBvc3QtcHJvY2VlZGluZ3M6IE9jdG9iZXIgMjAyNS4KCgpWSVNBIElT U1VFUwotLS0tLS0tLS0tLQoKTm90ZSB0aGF0IGV2ZW4gaWYgeW91IGFyZSBsdWNreSBlbm91Z2gg dG8gbm90IHJlcXVpcmUgYSB2aXNhIHRvIGVudGVyIAp0aGUgVUssCmJ5IHRoZSB0aW1lIFRZUEVT IGhhcHBlbnMsIHlvdSBtaWdodCBzdGlsbCBuZWVkIHRvIGFwcGx5IGZvciBlbGVjdHJvbmljCnRy YXZlbCBhdXRob3Jpc2F0aW9uLgoKaHR0cHM6Ly93d3cuZ292LnVrL2d1aWRhbmNlL2FwcGx5LWZv ci1hbi1lbGVjdHJvbmljLXRyYXZlbC1hdXRob3Jpc2F0aW9uLWV0YQoKSWYgeW91IGRvIG5lZWQg YSB2aXNhLCB3ZSBhcmUgaGFwcHkgdG8gd3JpdGUgeW91IGEgbGV0dGVyIG9mIGludml0YXRpb24s CmNvbmZpcm1pbmcgdGhhdCB5b3UgaGF2ZSByZWdpc3RlcmVkIGZvciB0aGUgY29uZmVyZW5jZS4K CgpDT05GSVJNRUQgU1BPTlNPUlMKLS0tLS0tLS0tLS0tLS0tLS0tCgpGb3JtYWwgVmluZGljYXRp b25zCldlbGwtVHlwZWQKCgpQUk9HUkFNTUUgQ09NTUlUVEVFCi0tLS0tLS0tLS0tLS0tLS0tLS0K CkRhbmVsIEFobWFuIChVbml2ZXJzaXR5IG9mIFRhcnR1LCBFc3RvbmlhKQpHdWlsbGF1bWUgQWxs YWlzIChVbml2ZXJzaXR5IG9mIFN0cmF0aGNseWRlLCBTY290bGFuZCkKTWFsaW4gQWx0ZW5tw7xs bGVyIChVbml2ZXJzaXR5IG9mIEVkaW5idXJnaCwgU2NvdGxhbmQpClNhbmRyYSBBbHZlcyAoVW5p dmVyc2l0eSBvZiBQb3J0bywgUG9ydHVnYWwpCkNhc3BlciBCYWNoIChVbml2ZXJzaXR5IG9mIFNv dXRoZXJuIERlbm1hcmssIERlbm1hcmspCkFuYSBCb3ZlIChDaGFsbWVycyBhbmQgVW5pdmVyc2l0 eSBvZiBHb3RoZW5idXJnLCBTd2VkZW4pCkxpYW5nLVRpbmcgQ2hlbiAoQWNhZGVtaWEgU2luaWNh LCBUYWl3YW4pClZpa3JhbWFuIENob3VkaHVyeSAoVW5pdmVyc2l0eSBvZiBCb2xvZ25hLCBJdGFs eSkKR2lsZGEgRmVycmVpcmEgKFVuaXZlcnNpZGFkZSBBYmVydGEsIFBvcnR1Z2FsKQpEYW5pZWwg R3JhdHplciAoQWFyaHVzIFVuaXZlcnNpdHksIERlbm1hcmspClRvbSBkZSBKb25nIChVbml2ZXJz aXR5IG9mIE5vdHRpbmdoYW0sIEVuZ2xhbmQpCkRvbWluaWsgS2lyc3QgKElucmlhIFBhcmlzLCBG cmFuY2UpCk5lZWwgS3Jpc2huYXN3YW1pIChVbml2ZXJzaXR5IG9mIENhbWJyaWRnZSwgRW5nbGFu ZCkKQW5kcsOhcyBLb3bDoWNzIChVbml2ZXJzaXR5IG9mIEdvdGhlbmJ1cmcgYW5kIENoYWxtZXJz LCBTd2VkZW4pClBldGVyIExlRmFudSBMdW1zZGFpbmUgKFN0b2NraG9sbSBVbml2ZXJzaXR5LCBT d2VkZW4pCktlbmppIE1haWxsYXJkIChJbnJpYSBSZW5uZXMtQnJldGFnbmUgQXRsYW50aXF1ZSwg RnJhbmNlKQpNYXggTmV3IChVbml2ZXJzaXR5IG9mIE1pY2hpZ2FuLCBVbml0ZWQgU3RhdGVzIG9m IEFtZXJpY2EpCkZyZWRyaWsgTm9yZHZhbGwgRm9yc2JlcmcgKFVuaXZlcnNpdHkgb2YgU3RyYXRo Y2x5ZGUsIFNjb3RsYW5kKSAoY2hhaXIpCkVsYWluZSBQaW1lbnRlbCAoVW5pdmVyc2l0eSBDb2xs ZWdlIExvbmRvbiwgRW5nbGFuZCkKQW5kcmV3IFN3YW4gKFVuaXZlcnNpdHkgb2YgTGp1YmxqYW5h LCBTbG92ZW5pYSkKVGFybW8gVXVzdGFsdSAoUmV5a2phdsOtayBVbml2ZXJzaXR5LCBJY2VsYW5k KQpOaWVscyB2YW4gZGVyIFdlaWRlIChSYWRib3VkIFVuaXZlcnNpdHkgTmlqbWVnZW4sIFRoZSBO ZXRoZXJsYW5kcykKVGjDqW8gV2ludGVyaGFsdGVyIChJbnJpYSBTYWNsYXksIEZyYW5jZSkKTWFh aWtlIFp3YXJ0IChJVCBVbml2ZXJzaXR5IENvcGVuaGFnZW4sIERlbm1hcmspCgpUWVBFUyBTVEVF UklORyBDT01NSVRURUUKLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCgpFZHVhcmRvIEhlcm1vIFJl eWVzIChGb3JtYWwgVmluZGljYXRpb25zLCBTcGFpbikKVG9tIGRlIEpvbmcgKFVuaXZlcnNpdHkg b2YgTm90dGluZ2hhbSwgRW5nbGFuZCkKUmFzbXVzIEVqbGVycyBNw7hnZWxiZXJnIChJVCBVbml2 ZXJzaXR5IG9mIENvcGVuaGFnZW4sIERlbm1hcmspCkZyZWRyaWsgTm9yZHZhbGwgRm9yc2Jlcmcg KFVuaXZlcnNpdHkgb2YgU3RyYXRoY2x5ZGUsIFNjb3RsYW5kKQpQYWlnZSBSYW5kYWxsIE5vcnRo IChVdHJlY2h0IFVuaXZlcnNpdHksIFRoZSBOZXRoZXJsYW5kcykgKGNoYWlyKQpCZW5ubyB2YW4g ZGVuIEJlcmcgKFVuaXZlcnNpdHkgb2YgQW1zdGVyZGFtLCBUaGUgTmV0aGVybGFuZHMpIChzZWNy ZXRhcnkpCgpBQk9VVCBUWVBFUwotLS0tLS0tLS0tLQoKVGhlIFRZUEVTIG1lZXRpbmdzIGZyb20g MTk5MCB0byAyMDA4IHdlcmUgYW5udWFsIHdvcmtzaG9wcyBvZiBhIHNlcXVlbmNlCm9mIGZpdmUg RVUgZnVuZGVkIG5ldHdvcmtpbmcgcHJvamVjdHMuIEZyb20gMjAwOSBvbndhcmRzLCBUWVBFUyBo YXMgYmVlbgpydW4gYXMgYW4gaW5kZXBlbmRlbnQgY29uZmVyZW5jZSBzZXJpZXMuIFByZXZpb3Vz IFRZUEVTIG1lZXRpbmdzIHdlcmUKaGVsZCBpbiBBbnRpYmVzICgxOTkwKSwgRWRpbmJ1cmdoICgx OTkxKSwgQsOlc3RhZCAoMTk5MiksIE5pam1lZ2VuCigxOTkzKSwgQsOlc3RhZCAoMTk5NCksIFRv cmlubyAoMTk5NSksIEF1c3NvaXMgKDE5OTYpLCBLbG9zdGVyIElyc2VlCigxOTk4KSwgTMO2a2Vi ZXJnICgxOTk5KSwgRHVyaGFtICgyMDAwKSwgQmVyZyBlbiBEYWwgbmVhciBOaWptZWdlbgooMjAw MiksIFRvcmlubyAoMjAwMyksIEpvdXktZW4tSm9zYXMgbmVhciBQYXJpcyAoMjAwNCksIE5vdHRp bmdoYW0KKDIwMDYpLCBDaXZpZGFsZSBkZWwgRnJpdWxpICgyMDA3KSwgVG9yaW5vICgyMDA4KSwg QXVzc29pcyAoMjAwOSksCldhcnNhdyAoMjAxMCksIEJlcmdlbiAoMjAxMSksIFRvdWxvdXNlICgy MDEzKSwgUGFyaXMgKDIwMTQpLCBUYWxsaW5uCigyMDE1KSwgTm92aSBTYWQgKDIwMTYpLCBCdWRh cGVzdCAoMjAxNyksIEJyYWdhICgyMDE4KSwgT3NsbyAoMjAxOSksClZpcnR1YWwgKDIwMjEpLCBO YW50ZXMgKDIwMjIpLCBWYWzDqG5jaWEgKDIwMjMpLCBDb3BlbmhhZ2VuICgyMDI0KS4KCkNPTlRB Q1QKLS0tLS0tLQoKRW1haWw6IENJU190eXBlczIwMjVAZ3JvdXBzLnN0cmF0aC5hYy51awoKT1JH QU5JWkVSUwotLS0tLS0tLS0tCgpHdWlsbGF1bWUgQWxsYWlzIChVbml2ZXJzaXR5IG9mIFN0cmF0 aGNseWRlLCBTY290bGFuZCkKU3R1YXJ0IEdhbGUgKFVuaXZlcnNpdHkgb2YgU3RyYXRoY2x5ZGUs IFNjb3RsYW5kKQpGcmVkcmlrIE5vcmR2YWxsIEZvcnNiZXJnIChVbml2ZXJzaXR5IG9mIFN0cmF0 aGNseWRlLCBTY290bGFuZCkKCgoKCl9fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f X19fX19fX19fX19fCkFnZGEgbWFpbGluZyBsaXN0CkFnZGFAbGlzdHMuY2hhbG1lcnMuc2UKaHR0 cHM6Ly9saXN0cy5jaGFsbWVycy5zZS9tYWlsbWFuL2xpc3RpbmZvL2FnZGEK