{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:42Z","timestamp":1780994682405,"version":"3.54.1"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don\u2019t go wrong and that ill-typed programs don\u2019t evaluate - that is, reach a value. This makes two-sided type systems suitable for incorrectness reasoning in higher-order program verification, which we illustrate through an application to precise data-flow typing in a language with constructors and pattern matching. Finally, we investigate the internalisation of the meta-level negation in the system as a complement operator on types. This motivates an alternative semantics for the typing judgement, which guarantees that ill-typed programs don\u2019t evaluate, but in which well-typed programs may yet go wrong.<\/jats:p>","DOI":"10.1145\/3632909","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"2010-2040","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Ill-Typed Programs Don\u2019t Evaluate"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0825-8386","authenticated-orcid":false,"given":"Steven","family":"Ramsay","sequence":"first","affiliation":[{"name":"University of Bristol, Bristol, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9011-1202","authenticated-orcid":false,"given":"Charlie","family":"Walpole","sequence":"additional","affiliation":[{"name":"University of Bristol, Bristol, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177847"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_26"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009882"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2355-7"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/217838.217858"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_17"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434336"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140356"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.29007\/w2m2"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563317"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258962"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800529"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1%35::AID-TAPO4%3.0.CO;2-4"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563304"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Steven Ramsay and Charlie Walpole. 2023. Ill-Typed Programs Don\u2019t Evaluate. https:\/\/doi.org\/10.48550\/arXiv.2307.06928 10.48550\/arXiv.2307.06928 arXiv:2307.06928 [cs.PL]","DOI":"10.48550\/arXiv.2307.06928"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_2"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706315"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784745"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_13"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632909","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632909","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:55Z","timestamp":1751659675000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632909"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":32,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632909"],"URL":"https:\/\/doi.org\/10.1145\/3632909","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}