Cited By
View all- Qian KSmith SStride BWeng SWu K(2024)Semantic-Type-Guided Bug FindingProceedings of the ACM on Programming Languages10.1145/36897888:OOPSLA2(2183-2210)Online publication date: 8-Oct-2024
Ill-Typed Programs Don’t Evaluate
Article No.: 67, Pages 2010 - 2040
Abstract
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't go wrong and that ill-typed programs don't 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't evaluate, but in which well-typed programs may yet go wrong.
References
[1]
Alexander Aiken, Edward L. Wimmers, and T. K. Lakshman. 1994. Soft Typing with Conditional Types. In Conference Record of POPL’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Portland, Oregon, USA, January 17-21, 1994. 163–173. https://doi.org/10.1145/174675.177847
[2]
Julian Bradfield and Igor Walukiewicz. 2018. Handbook of Model Checking. Springer International Publishing, 871–919. https://doi.org/10.1007/978-3-319-10575-8_26
[3]
Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. 2013. Automatic Inference of Necessary Preconditions. In Verification, Model Checking, and Abstract Interpretation, Roberto Giacobazzi, Josh Berdine, and Isabella Mastroeni (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 128–148. isbn:978-3-642-35873-9 https://doi.org/10.1007/978-3-642-35873-9_10
[4]
Patrick Cousot, Radhia Cousot, and Francesco Logozzo. 2011. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In Verification, Model Checking, and Abstract Interpretation, Ranjit Jhala and David Schmidt (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 150–168. isbn:978-3-642-18275-4 https://doi.org/10.1007/978-3-642-18275-4_12
[5]
Pierre-Louis Curien and Hugo Herbelin. 2000. The duality of computation. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000, Martin Odersky and Philip Wadler (Eds.). ACM, 233–243. https://doi.org/10.1145/351240.351262
[6]
Stephen Dolan and Alan Mycroft. 2017. Polymorphism, Subtyping, and Type Inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL ’17). Association for Computing Machinery, New York, NY, USA. 60–72. isbn:9781450346603 https://doi.org/10.1145/3009837.3009882
[7]
H.-D. Ebbinghaus, J. Flum, and W. Thomas. 1994. Mathematical Logic. Springer. https://doi.org/10.1007/978-1-4757-2355-7
[8]
Jonathan Eifrig, Scott Smith, and Valery Trifonov. 1995. Sound Polymorphic Type Inference for Objects. In Proceedings of the Tenth Annual Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA ’95). Association for Computing Machinery, New York, NY, USA. 169–184. isbn:0897917030 https://doi.org/10.1145/217838.217858
[9]
Robert Jakob and Peter Thiemann. 2015. A Falsification View of Success Typing. In NASA Formal Methods, Klaus Havelund, Gerard Holzmann, and Rajeev Joshi (Eds.). Springer International Publishing, Cham. 234–247. isbn:978-3-319-17524-9 https://doi.org/10.1007/978-3-319-17524-9_17
[10]
Eddie Jones and Steven Ramsay. 2021. Intensional Datatype Refinement: With Application to Scalable Verification of Pattern-Match Safety. Proc. ACM Program. Lang., 5, POPL (2021), Article 55, jan, 29 pages. https://doi.org/10.1145/3434336
[11]
Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Finding Real Bugs in Big Programs with Incorrectness Logic. Proc. ACM Program. Lang., 6, OOPSLA1 (2022), Article 81, apr, 27 pages. https://doi.org/10.1145/3527325
[12]
Tobias Lindahl and Konstantinos Sagonas. 2006. Practical Type Inference Based on Success Typings. In Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP ’06). Association for Computing Machinery, New York, NY, USA. 167–178. isbn:1595933883 https://doi.org/10.1145/1140335.1140356
[13]
Francisco J. López-Fraguas, Manuel Montenegro, and Gorka Suárez-García. 2018. Polymorphic success types for Erlang. In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Gilles Barthe, Geoff Sutcliffe, and Margus Veanes (Eds.) (EPiC Series in Computing, Vol. 57). EasyChair, 515–533. issn:2398-7340 https://doi.org/10.29007/w2m2
[14]
Julian Mackay, Susan Eisenbach, James Noble, and Sophia Drossopoulou. 2022. Necessity Specifications for Robustness. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 154, oct, 30 pages. https://doi.org/10.1145/3563317
[15]
Simon Marlow and Philip Wadler. 1997. A Practical Subtyping System for Erlang. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (ICFP ’97). Association for Computing Machinery, New York, NY, USA. 136–149. isbn:0897919181 https://doi.org/10.1145/258948.258962
[16]
John C. Mitchell. 1984. Coercion and Type Inference. In Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’84). Association for Computing Machinery, New York, NY, USA. 175–185. isbn:0897911253 https://doi.org/10.1145/800017.800529
[17]
Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types. TAPOS, 5, 1 (1999), 35–55. https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0.CO;2-4
[18]
Peter W. O’Hearn. 2019. Incorrectness Logic. Proc. ACM Program. Lang., 4, POPL (2019), Article 10, dec, 32 pages. https://doi.org/10.1145/3371078
[19]
Lionel Parreaux and Chun Yin Chau. 2022. MLstruct: Principal Type Inference in a Boolean Algebra of Structural Types. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 141, oct, 30 pages. https://doi.org/10.1145/3563304
[20]
Azalea Raad, Josh Berdine, Derek Dreyer, and Peter W. O’Hearn. 2022. Concurrent Incorrectness Separation Logic. Proc. ACM Program. Lang., 6, POPL (2022), Article 34, jan, 29 pages. https://doi.org/10.1145/3498695
[21]
Steven Ramsay and Charlie Walpole. 2023. Ill-Typed Programs Don’t Evaluate. https://doi.org/10.48550/arXiv.2307.06928 arxiv:2307.06928.
[22]
Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008. Liquid types. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008. 159–169. https://doi.org/10.1145/1375581.1375602
[23]
Konstantinos Sagonas. 2010. Using Static Analysis to Detect Type Errors and Concurrency Defects in Erlang Programs. In Functional and Logic Programming, Matthias Blume, Naoki Kobayashi, and Germán Vidal (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 13–18. isbn:978-3-642-12251-4 https://doi.org/10.1007/978-3-642-12251-4_2
[24]
Tachio Terauchi. 2010. Dependent types from counterexamples. In Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010. 119–130. https://doi.org/10.1145/1706299.1706315
[25]
Hiroshi Unno and Naoki Kobayashi. 2009. Dependent type inference with interpolants. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal. 277–288. https://doi.org/10.1145/1599410.1599445
[26]
Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs. Proc. ACM Program. Lang., 2, POPL (2017), Article 12, dec, 29 pages. https://doi.org/10.1145/3158100
[27]
Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015. Bounded refinement types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015. 48–61. https://doi.org/10.1145/2784731.2784745
[28]
Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013. Abstract Refinement Types. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. 209–228. https://doi.org/10.1007/978-3-642-37036-6_13
[29]
Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton-Jones. 2014. Refinement Types for Haskell. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). 269–282. isbn:978-1-4503-2873-9
[30]
Glynn Winskel. 1993. The Formal Semantics of Programming Languages: An Introduction. MIT Press. https://doi.org/10.7551/mitpress/3054.001.0001
[31]
A.K. Wright and M. Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), 38–94. https://doi.org/10.1006/inco.1994.1093
[32]
Noam Zilberstein, Derek Dreyer, and Alexandra Silva. 2023. Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. Proc. ACM Program. Lang., 7, OOPSLA1 (2023), Article 93, apr, 29 pages. https://doi.org/10.1145/3586045
Index Terms
- Ill-Typed Programs Don’t Evaluate
Recommendations
Liberal typing for functional logic programs
APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systemsWe propose a new type system for functional logic programming which is more liberal than the classical Damas-Milner usually adopted, but it is also restrictive enough to ensure type soundness. Starting from Damas-Milner typing of expressions we propose ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Typing constraint logic programs
We present a prescriptive type system with parametric polymorphism and subtyping for constraint logic programs. The aim of this type system is to detect programming errors statically. It introduces a type discipline for constraint logic programs and ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 472Total Downloads
- Downloads (Last 12 months)472
- Downloads (Last 6 weeks)75
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
Cited By
View all- Qian KSmith SStride BWeng SWu K(2024)Semantic-Type-Guided Bug FindingProceedings of the ACM on Programming Languages10.1145/36897888:OOPSLA2(2183-2210)Online publication date: 8-Oct-2024
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in