Call for Papers: Tests and Proofs (TAP) (Now a Track at FM 2026)

"Achim D. Brucker" <[email protected]> Thu, 24 Jul 2025 05:58:07 +0100
Newsgroups gmane.comp.lang.haskell.general
Message-ID <kosxy7venlzrwrjqo5mnetz25yoo3rart6jrrz2i5ctzh6hweq@o6fhk2cuy2vc>
KipDQUxMIEZPUiBQQVBFUlMqKgoKKipTcGVjaWFsIFRyYWNrIG9uIFRlc3RzIGFuZCBQcm9vZnMg
KFRBUCAyMDI2KSoqCgoqYXQgdGhlKgoKKioyN3RoIEludGVybmF0aW9uYWwgU3ltcG9zaXVtIG9u
IEZvcm1hbCBNZXRob2RzIChGTSAyMDI2KSoqCgoqKk1heSAxOC0yMiwgMjAyNiAtLS0gVG9reW8s
IEphcGFuKioKCioqV2Vic2l0ZToqKiA8aHR0cHM6Ly9jb25mLnJlc2VhcmNoci5vcmcvdHJhY2sv
Zm0tMjAyNi8+CgoqKkFic3RyYWN0IFN1Ym1pc3Npb24qKjogVHVlc2RheSwgMjUgTm92ZW1iZXIg
MjAyNQoqKkZ1bGwgUGFwZXIgU3VibWlzc2lvbjoqKiBUdWVzZGF5LCAyIERlY2VtYmVyIDIwMjUK
CiMjIyAqKk5ldyBUQVAgVHJhY2sgYXQgRk0gMjAyNjogQSBQcmVtaWVyIFZlbnVlIGZvciBUZXN0
cyBhbmQgUHJvb2ZzKioKClNpbmNlIDIwMDcsIHRoZSBbVGVzdCBhbmQgUHJvb2YgKFRBUCkKY29u
ZmVyZW5jZV0oaHR0cHM6Ly90YXBjb25mZXJlbmNlLmdpdGh1Yi5pby8yMDI0LykgaGFzIGxvbmcg
YmVlbiBhCmxlYWRpbmcgdmVudWUgZm9yIHJlc2VhcmNoIG9uIHRoZSBpbnRlcnNlY3Rpb24gb2Yg
c29mdHdhcmUgdGVzdGluZyBhbmQKZm9ybWFsIHZlcmlmaWNhdGlvbi4gTm93LCBUQVAgaXMgam9p
bmluZyB0aGUgMjd0aCBJbnRlcm5hdGlvbmFsClN5bXBvc2l1bSBvbiBGb3JtYWwgTWV0aG9kcyAo
Rk0gMjAyNikgYXMgYSBuZXcgc3BlY2lhbCB0cmFjay4gVGhpcwppbnRlZ3JhdGlvbiBwbGFjZXMg
dGhlIGdyb3VuZC1icmVha2luZyB3b3JrIG9mIHRoZSBUZXN0IGFuZCBQcm9vZnMKY29tbXVuaXR5
IGF0IHRoZSBoZWFydCBvZiB0aGUgd29ybGQncyBwcmVtaWVyIGNvbmZlcmVuY2Ugb24gZm9ybWFs
Cm1ldGhvZHMuCgpUaGlzIG5ldyB0cmFjayBwcm92aWRlcyBhIGRlZGljYXRlZCBmb3J1bSBmb3Ig
cmVzZWFyY2hlcnMsCnByYWN0aXRpb25lcnMsIGFuZCB0b29sIGRldmVsb3BlcnMgdG8gcHJlc2Vu
dCBhbmQgZGlzY3VzcyB0aGUgbGF0ZXN0CmFkdmFuY2VzIGluIHRoZSBzeW5lcmdpc3RpYyBjb21i
aW5hdGlvbiBvZiB0cmFkaXRpb25hbGx5IGRpc3RpbmN0IGFyZWFzCm9mIGR5bmFtaWMgYW5hbHlz
aXMsIGUuZy4sIHRlc3RpbmcsIGFuZCBzdGF0aWMgYW5hbHlzaXMsIGUuZy4sIHByb3ZpbmcuCkJ5
IGpvaW5pbmcgRk0sIHRoZSBUQVAgdHJhY2sgb2ZmZXJzIGF1dGhvcnMgYSB3aWRlciwgbW9yZSBk
aXZlcnNlCmF1ZGllbmNlIGFuZCB0aGUgcHJlc3RpZ2Ugb2YgcHVibGljYXRpb24gaW4gdGhlIG1h
aW4sIG9wZW4tYWNjZXNzIEZNCjIwMjYgcHJvY2VlZGluZ3MsIHB1Ymxpc2hlZCBieSBTcHJpbmdl
ciBpbiB0aGUgTE5DUyBzZXJpZXMuIFdlIGludml0ZQp5b3UgdG8gYmUgcGFydCBvZiB0aGlzIGV4
Y2l0aW5nIG5ldyBjaGFwdGVyIGZvciB0aGUgdGVzdHMgYW5kIHByb29mcwpjb21tdW5pdHkhCgoq
KlRyYWNrIEhpZ2hsaWdodDogRk0gMjAyNiBLZXlub3RlIGJ5IFByb2Zlc3NvciBDcmlzdGlhbiBD
YWRhcioqCgpXZSBhcmUgdGhyaWxsZWQgdG8gYW5ub3VuY2UgdGhhdCBUQVAgVHJhY2sgYXQgRk0g
MjAyNiB3aWxsIGZlYXR1cmUgYQprZXlub3RlIGFkZHJlc3MgYnkgKipQcm9mZXNzb3IgQ3Jpc3Rp
YW4gQ2FkYXIqKiBvZiBJbXBlcmlhbCBDb2xsZWdlCkxvbmRvbi4gUHJvZmVzc29yIENhZGFyIGlz
IGEgd29ybGQtcmVub3duZWQgYXV0aG9yaXR5IG9uIHNvZnR3YXJlCnJlbGlhYmlsaXR5LCBzZWN1
cml0eSwgYW5kIHZlcmlmaWNhdGlvbiwgYW5kIGlzIHBhcnRpY3VsYXJseSBjZWxlYnJhdGVkCmZv
ciBoaXMgcGlvbmVlcmluZyBjb250cmlidXRpb25zIHRvIHN5bWJvbGljIGFuZCBkeW5hbWljIGV4
ZWN1dGlvbgooZS5nLiwgS0xFRSkuIEhpcyBzZWxlY3Rpb24gYXMgYSBtYWluIHN5bXBvc2l1bSBr
ZXlub3RlIHNwZWFrZXIgaXMgYQpwb3dlcmZ1bCB0ZXN0YW1lbnQgdG8gdGhlIGluY3JlYXNpbmcg
aW1wb3J0YW5jZSBvZiB0aGUgY29yZSB0b3BpY3Mgb2YKdGhlIFRBUCB0cmFjayB0byB0aGUgYnJv
YWRlciBjb21wdXRlciBzY2llbmNlIGNvbW11bml0eS4KCiMjIyAqKlNjb3BlIGFuZCBUb3BpY3Mg
b2YgSW50ZXJlc3QqKgoKVGhlIFRBUCB0cmFjayBzb2xpY2l0cyBoaWdoLXF1YWxpdHksIG9yaWdp
bmFsIHJlc2VhcmNoIG9uIHRoZSBpbnRlcnBsYXkKYmV0d2VlbiBkeW5hbWljIHRlY2huaXF1ZXMg
c3VjaCBhcyB0ZXN0aW5nLCBydW50aW1lIHZlcmlmaWNhdGlvbgpldGMudGVzdGluZyBhbmQgZm9y
bWFsIHZlcmlmaWNhdGlvbiBzdWNoIGFzIHByb3ZpbmcsIG1vZGVsIGNoZWNraW5nLAphYnN0cmFj
dCBpbnRlcnByZXRhdGlvbiwgZXRjLiAuIFRoZSB0cmFjayBhaW1zIHRvIGZvc3RlciBuZXcKY29s
bGFib3JhdGlvbnMgYW5kIGFkdmFuY2UgdGhlIHN0YXRlIG9mIHRoZSBhcnQgaW4gY3JlYXRpbmcg
cmVsaWFibGUgYW5kCnNlY3VyZSBzb2Z0d2FyZSBhbmQgc3lzdGVtcy4gVG9waWNzIG9mIGludGVy
ZXN0IGluY2x1ZGUsIGJ1dCBhcmUgbm90CmxpbWl0ZWQgdG8sIHRoZSBmb2xsb3dpbmcgYXJlYXM6
CgoqKkZvdW5kYXRpb25zIGZvciBDb21iaW5pbmcgVGVzdGluZyBhbmQgVmVyaWZpY2F0aW9uKioK
Ci0gICBGb3JtYWxpc21zIGFuZCB0aGVvcmllcyB0aGF0IHVuaWZ5IHRlc3RpbmcgYW5kIHByb29m
XAotICAgU2VtYW50aWMgZm91bmRhdGlvbnMgZm9yIGNvbWJpbmVkIHN0YXRpYyBhbmQgZHluYW1p
YyBhbmFseXNpc1wKLSAgIFByb29mIHRoZW9yeSBmb3IgdGVzdC1jYXNlIGdlbmVyYXRpb24gYW5k
IHNwZWNpZmljYXRpb24gY29uZm9ybWFuY2VcCi0gICBUeXBlIHN5c3RlbXMgd2l0aCBhIHRlc3Rp
bmcgYW5kIHByb3ZpbmcgZm9jdXNcCi0gICBGb3JtYWwgbW9kZWxzIG9mIHRlc3QtYmFzZWQgYW5k
IHByb29mLWJhc2VkIGRldmVsb3BtZW50CgoqKlN5bmVyZ2lzdGljIFRlY2huaXF1ZXMgYW5kIFRv
b2xzKioKCi0gICBDb21iaW5hdGlvbiBvZiBtb2RlbCBjaGVja2luZywgdGhlb3JlbSBwcm92aW5n
LCBhbmQgcnVudGltZQogICAgdmVyaWZpY2F0aW9uCi0gICBTeW5lcmdpZXMgYmV0d2VlbiBzeW1i
b2xpYyBleGVjdXRpb24sIGZ1enppbmcsIGFuZCBmb3JtYWwgYW5hbHlzaXMKLSAgIFRlc3QtY2Fz
ZSBnZW5lcmF0aW9uIGZyb20gZm9ybWFsIHNwZWNpZmljYXRpb25zIChlLmcuLCB1c2luZyBCLCBa
LAogICAgVExBKywgVkRNKQotICAgVXNpbmcgdGVzdCBleGVjdXRpb24gcmVzdWx0cyB0byBndWlk
ZSBvciBhdXRvbWF0ZSBwcm9vZiBkaXNjb3ZlcnkKLSAgIFN0YXRpYyBhbmFseXNpcyBmb3IgdGVz
dC1zdWl0ZSByZWR1Y3Rpb24sIHByaW9yaXRpemF0aW9uLCBhbmQKICAgIG9wdGltaXphdGlvbgot
ICAgVmVyaWZpY2F0aW9uLWJhc2VkIGFuZCBwcm9wZXJ0eS1iYXNlZCB0ZXN0aW5nCi0gICBGb3Jt
YWwgbWV0aG9kcyBmb3IgdGVzdGluZyBBSS9NTC1iYXNlZCBzeXN0ZW1zCi0gICBBSS9NTCB0ZWNo
bmlxdWVzIGZvciBlbmhhbmNpbmcgZm9ybWFsIHZlcmlmaWNhdGlvbiBhbmQgdGVzdGluZwotICAg
RGVyaXZhdGlvbiBvZiBzcGVjaWZpY2F0aW9ucyBhbmQgY29udHJhY3RzIGZyb20gdGVzdHMKLSAg
IENvbWJpbmF0aW9uIG9mIHN0YXRpYyBhbmQgZHluYW1pYyBhbmFseXNpcyBmb3Igc2VjdXJpdHkK
ICAgIHZ1bG5lcmFiaWxpdHkgZGV0ZWN0aW9uCgoqKkFwcGxpY2F0aW9ucyBhbmQgRW1waXJpY2Fs
IEV2YWx1YXRpb24qKgoKLSAgIENhc2Ugc3R1ZGllcyBhbmQgZXhwZXJpZW5jZSByZXBvcnRzIGFw
cGx5aW5nIGNvbWJpbmVkIHRlc3QtYW5kLXByb29mCiAgICB0ZWNobmlxdWVzIHRvIGluZHVzdHJp
YWwgc3lzdGVtcyAoZS5nLiwgaW4gc2VjdXJpdHksIGN5YmVyLXBoeXNpY2FsCiAgICBzeXN0ZW1z
LCBhdXRvbm9tb3VzIHN5c3RlbXMsIGJsb2NrY2hhaW4sIG9yIElvVCkKLSAgIEVtcGlyaWNhbCBj
b21wYXJpc29ucyBvZiBkaWZmZXJlbnQgdmVyaWZpY2F0aW9uLCB0ZXN0aW5nLCBhbmQKICAgIGNv
bWJpbmVkIHRlY2huaXF1ZXMKLSAgIFRvb2wgZGVtb25zdHJhdGlvbiBwYXBlcnMgZm9yIG5ldyBh
bmQgaW5ub3ZhdGl2ZSB0b29scyB0aGF0IHN1cHBvcnQKICAgIHRlc3RzIGFuZCBwcm9vZnMKLSAg
IEFwcGxpY2F0aW9uIG9mIFRBUCB0ZWNobmlxdWVzIHRvIGNoYWxsZW5nZSBwcm9ibGVtcyBhbmQg
YmVuY2htYXJrcwoKIyMjICoqU3VibWlzc2lvbiBDYXRlZ29yaWVzIGFuZCBHdWlkZWxpbmVzKioK
ClRoZSBUQVAgdHJhY2sgcGFwZXJzIGNhbiBiZSBzdWJtaXR0ZWQgaW4gYWxsIHBhcGVyIGNhdGVn
b3JpZXMgc3VwcG9ydGVkCmJ5IHRoZSBGTSAyMDI2IFJlc2VhcmNoIFRyYWNrIGFuZCBzdWJtaXNz
aW9ucyB0byB0aGUgVEFQIHRyYWNrIHdpbGwgYmUKcmV2aWV3ZWQgZm9sbG93aW5nIHRoZSBwb2xp
Y2llcyBhbmQgcXVhbGl0eSBjcml0ZXJpYSBvZiB0aGUgRk0gUmVzZWFyY2gKVHJhY2suCgpUaGUg
VEFQIHRyYWNrIHNvbGljaXRzIHBhcGVycyBpbiB0aGUgZm9sbG93aW5nIGNhdGVnb3JpZXM6Cgot
ICAgKipSZWd1bGFyIFBhcGVycyAobWF4IDE1IHBhZ2VzLCBleGNsdWRpbmcgcmVmZXJlbmNlcyBh
bmQKICAgIGFwcGVuZGljZXMpOioqIEZvciBtYXR1cmUsIG9yaWdpbmFsIHJlc2VhcmNoIGNvbnRy
aWJ1dGlvbnMuCi0gICAqKkxvbmcgVG9vbCBQYXBlcnMgKG1heCAxNSBwYWdlcywgZXhjbHVkaW5n
IHJlZmVyZW5jZXMgYW5kCiAgICBhcHBlbmRpY2VzKToqKiBGb3IgcHJlc2VudGluZyBtYXR1cmUg
dG9vbHMsIHRoZWlyIHRoZW9yZXRpY2FsCiAgICBmb3VuZGF0aW9ucywgYW5kIGVtcGlyaWNhbCBl
dmFsdWF0aW9ucy4KLSAgICoqQ2FzZSBTdHVkeSBQYXBlcnMgKG1heCAxNSBwYWdlcywgZXhjbHVk
aW5nIHJlZmVyZW5jZXMgYW5kCiAgICBhcHBlbmRpY2VzKToqKiBGb3IgaW4tZGVwdGggcmVwb3J0
cyBvbiB0aGUgYXBwbGljYXRpb24gb2YgVEFQCiAgICB0ZWNobmlxdWVzIHRvIHNpZ25pZmljYW50
LCByZWFsLXdvcmxkIHByb2JsZW1zLgotICAgKipTaG9ydCBQYXBlcnMgKG1heCA2IHBhZ2VzLCBl
eGNsdWRpbmcgcmVmZXJlbmNlcyBhbmQgYXBwZW5kaWNlcyk6KioKICAgIEZvciBwcmVzZW50aW5n
IG5vdmVsIGJ1dCBub3QgeWV0IGZ1bGx5IG1hdHVyZSBpZGVhcywgb3IgZm9yIHRvb2wKICAgIGRl
bW9uc3RyYXRpb24gcGFwZXJzIHRoYXQgZm9jdXMgb24gYSB0b29sJ3MgZmVhdHVyZXMgYW5kIHVz
YWdlLgoKUGFwZXJzIHNob3VsZCBiZSBvcmlnaW5hbCB3b3JrLCBub3QgcHVibGlzaGVkIG9yIHN1
Ym1pdHRlZCBlbHNld2hlcmUsIGluClNwcmluZ2VyIFtMTkNTIGZvcm1hdF0oaHR0cHM6Ly93d3cu
c3ByaW5nZXIuY29tL2dwL2NvbXB1dGVyLXNjaWVuY2UvbG5jcy9jb25mZXJlbmNlLXByb2NlZWRp
bmdzLWd1aWRlbGluZXMpLAphbmQgd3JpdHRlbiBpbiBFbmdsaXNoLgoKU3VibWl0IHlvdXIgcGFw
ZXJzIGF0IGh0dHBzOi8vZWFzeWNoYWlyLm9yZy9jb25mZXJlbmNlcy8/Y29uZj1mbTIwMjYKClJl
dmlld2luZyBpcyBzaW5nbGUtYmxpbmQuIEVhY2ggcGFwZXIgd2lsbCBiZSBldmFsdWF0ZWQgYnkg
YXQgbGVhc3QKdGhyZWUgbWVtYmVycyBvZiB0aGUgUHJvZ3JhbSBDb21taXR0ZWUuIFBhcGVycyB3
aWxsIGJlIGFjY2VwdGVkIG9yCnJlamVjdGVkIGluIHRoZSBjYXRlZ29yeSBpbiB3aGljaCB0aGV5
IHdlcmUgc3VibWl0dGVkIGFuZCB3aWxsIG5vdCBiZQptb3ZlZCBiZXR3ZWVuIGNhdGVnb3JpZXMK
CkF1dGhvcnMgb2YgYWNjZXB0ZWQgcGFwZXJzIGFyZSBzdHJvbmdseSBlbmNvdXJhZ2VkIHRvIHN1
Ym1pdCB0aGVpcgpzdXBwb3J0aW5nIGFydGlmYWN0cyB0byB0aGUgRk0gMjAyNiBBcnRpZmFjdCBF
dmFsdWF0aW9uIHRyYWNrLgoKIyMjICoqSW1wb3J0YW50IERhdGVzKioKCkFsbCBkZWFkbGluZXMg
YXJlICoqQW55d2hlcmUgb24gRWFydGggKEFvRSwgVVRDLTEyaCkqKi4gVGhlIGRlYWRsaW5lcwpm
b3IgdGhlIFRBUCB0cmFjayBhcmUgYWxpZ25lZCB3aXRoIHRoZSBGTSAyMDI2IFJlc2VhcmNoIFRy
YWNrLgoKICBNaWxlc3RvbmUgICAgICAgICAgICAgICAgICAgRGF0ZQogIC0tLS0tLS0tLS0tLS0t
LS0tLS0tLS0tLS0tLSAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tCiAgKipBYnN0cmFj
dCBTdWJtaXNzaW9uKiogICAgICoqVHVlc2RheSwgMjUgTm92ZW1iZXIgMjAyNSoqCiAgKipGdWxs
IFBhcGVyIFN1Ym1pc3Npb24qKiAgICoqVHVlc2RheSwgMiBEZWNlbWJlciAyMDI1KioKICAqKkF1
dGhvciBOb3RpZmljYXRpb24qKiAgICAgKipGcmlkYXksIDYgRmVicnVhcnkgMjAyNioqCiAgKipD
YW1lcmEtUmVhZHkgVmVyc2lvbioqICAgICoqTW9uZGF5LCAyIE1hcmNoIDIwMjYqKgogICoqRk0g
MjAyNiBDb25mZXJlbmNlKiogICAgICAqKk1heSAxOC0yMiwgMjAyNioqCgojIyMgKipQdWJsaWNh
dGlvbioqCgpBbGwgYWNjZXB0ZWQgcGFwZXJzIGZvciB0aGUgVEFQIHRyYWNrIHdpbGwgYmUgcHVi
bGlzaGVkIGFzIHBhcnQgb2YgdGhlCm1haW4gRk0gMjAyNiBjb25mZXJlbmNlIHByb2NlZWRpbmdz
LiBUaGUgcHJvY2VlZGluZ3Mgd2lsbCBiZSBwdWJsaXNoZWQKYnkgU3ByaW5nZXIgaW4gdGhlaXIg
KipvcGVuLWFjY2VzcyBMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2UKKExOQ1MpKiog
c2VyaWVzLiBBdCBsZWFzdCBvbmUgYXV0aG9yIG9mIGFuIGFjY2VwdGVkIHBhcGVyIG11c3QgcmVn
aXN0ZXIKZm9yIHRoZSBjb25mZXJlbmNlIGFuZCBwcmVzZW50IHRoZSB3b3JrLgoKIyMjICoqVHJh
Y2sgT3JnYW5pemF0aW9uKioKCioqVHJhY2sgQ2hhaXJzOioqCgotIE1hcmllLUNocmlzdGluZSBK
YWtvYnMsIEx1ZHdpZy1NYXhpbWlsYW4gVW5pdmVyc2l0eSwgTXVuaWNoLCBHZXJtYW55Ci0gQWNo
aW0gRC4gQnJ1Y2tlciwgVW5pdmVyc2l0eSBvZiBFeGV0ZXIsIFVLCgpGb3IgaW5xdWlyaWVzLCBw
bGVhc2UgY29udGFjdCB0aGUgdHJhY2sgY2hhaXJzLgoKLS0gClByb2YuIEFjaGltIEJydWNrZXIg
fCBDaGFpciBpbiBDeWJlcnNlY3VyaXR5ICYgSGVhZCBvZiBHcm91cCB8IFVuaXZlcnNpdHkgb2Yg
RXhldGVyCiAgICAgICAgICAgaHR0cHM6Ly93d3cuYnJ1Y2tlci5jaCB8IGh0dHBzOi8vbG9naWNh
bGhhY2tpbmcuY29tL2Jsb2cKICAgICAgICAgICAgICAgICAgICAgICAgIEBhZGJydWNrZXIgfCBA
bG9naWNhbGhhY2tpbmcKX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19f
X19fX18KSGFza2VsbCBtYWlsaW5nIGxpc3QKSGFza2VsbEBoYXNrZWxsLm9yZwpodHRwOi8vbWFp
bC5oYXNrZWxsLm9yZy9jZ2ktYmluL21haWxtYW4vbGlzdGluZm8vaGFza2VsbAo=