Document Open Access Logo

Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors Ke Sun , Di Wang , Sheng Chen , Meng Wang , Dan Hao

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.39.pdf
  • Filesize: 1.07 MB
  • 30 pages

Document Identifiers

Author Details

Ke Sun
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China
Di Wang
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China
Sheng Chen
  • The Center for Advanced Computer Studies, University of Louisiana, Lafayette, LA, USA
Meng Wang
  • University of Bristol, UK
Dan Hao
  • Key Lab of HCST (PKU), MOE, School of Computer Science, Peking University, Beijing, China

Funding

This work is sponsored by National Natural Science Foundation of China Grant No. 62232001, NSF Grant 1750886, and EPSRC Grant EP/T008911/1.

Acknowledgements

We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ECOOP.2024.39

Abstract

Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Software and its engineering → Formal software verification
Keywords
  • Refinement Types
  • Program Verification
  • Object-oriented Programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H. Schmitt, and Mattias Ulbrich, editors. Deductive software verification - the KeY book - from theory to practice, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-49812-6.
  2. Nada Amin, K. Rustan M. Leino, and Tiark Rompf. Computing with an SMT solver. In Martina Seidl and Nikolai Tillmann, editors, Tests and Proofs - 8th International Conference, TAP@STAF 2014, York, UK, July 24-25, 2014. Proceedings, volume 8570 of Lecture Notes in Computer Science, pages 20-35. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09099-3_2.
  3. Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The poplmark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 50-65. Springer, 2005. URL: https://doi.org/10.1007/11541868_4.
  4. Clark W. Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 171-177. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22110-1_14.
  5. Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. Java & lambda: a featherweight story. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:17)2018.
  6. Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David E. Langworthy. Semantic subtyping with an SMT solver. J. Funct. Program., 22(1):31-105, 2012. URL: https://doi.org/10.1017/S0956796812000032.
  7. Régis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. An overview of the leon verification system: verification by translation to recursive functions. In Proceedings of the 4th Workshop on Scala, SCALA@ECOOP 2013, Montpellier, France, July 2, 2013, pages 1:1-1:10. ACM, 2013. URL: https://doi.org/10.1145/2489837.2489838.
  8. Michael Borkowski, Niki Vazou, and Ranjit Jhala. Mechanizing refinement types. Proc. ACM Program. Lang., 8(POPL):2099-2128, 2024. URL: https://doi.org/10.1145/3632912.
  9. Aaron R. Bradley and Zohar Manna. The calculus of computation - decision procedures with applications to verification. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74113-8.
  10. Joana Campos and Vasco T. Vasconcelos. Dependent types for class-based mutable objects. In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, volume 109 of LIPIcs, pages 13:1-13:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.ECOOP.2018.13.
  11. Giuseppe Castagna. Covariance and contravariance: Conflict without a cause. ACM Trans. Program. Lang. Syst., 17(3):431-447, 1995. URL: https://doi.org/10.1145/203095.203096.
  12. Giuseppe Castagna, Giorgio Ghelli, and Giuseppe Longo. A semantics for lambda&-early: A calculus with overloading and early binding. In Marc Bezem and Jan Friso Groote, editors, Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA '93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science, pages 107-123. Springer, 1993. URL: https://doi.org/10.1007/BFB0037101.
  13. Arthur Charguéraud. The locally nameless representation. J. Autom. Reason., 49(3):363-408, 2012. URL: https://doi.org/10.1007/S10817-011-9225-2.
  14. Zilin Chen. A hoare logic style refinement types formalisation. In TyDe '22: 7th ACM SIGPLAN International Workshop on Type-Driven Development, Ljubljana, Slovenia, 11 September 2022, pages 1-14. ACM, 2022. URL: https://doi.org/10.1145/3546196.3550162.
  15. Adam Chlipala. Certified programming with dependent types - a pragmatic introduction to the Coq Proof Assistant. MIT Press, 2013. URL: http://mitpress.mit.edu/books/certified-programming-dependent-types.
  16. William R. Cook. On understanding data abstraction, revisited. In Shail Arora and Gary T. Leavens, editors, Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25-29, 2009, Orlando, Florida, USA, pages 557-572. ACM, 2009. URL: https://doi.org/10.1145/1640089.1640133.
  17. Samuel da Silva Feitosa, Rodrigo Geraldo Ribeiro, and André Rauber Du Bois. Towards an extrinsic formalization of featherweight java in agda. CLEI Electron. J., 24(3), 2021. URL: https://doi.org/10.19153/CLEIEJ.24.3.3.
  18. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In André Platzer and Geoff Sutcliffe, editors, Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings, volume 12699 of Lecture Notes in Computer Science, pages 625-635. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_37.
  19. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  20. Benjamin Delaware, William R. Cook, and Don S. Batory. Product lines of theorems. In Cristina Videira Lopes and Kathleen Fisher, editors, Proceedings of the 26th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2011, part of SPLASH 2011, Portland, OR, USA, October 22 - 27, 2011, pages 595-608. ACM, 2011. URL: https://doi.org/10.1145/2048066.2048113.
  21. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365-473, 2005. URL: https://doi.org/10.1145/1066100.1066102.
  22. Khalil Djelloul, Thi-Bich-Hanh Dao, and Thom W. Frühwirth. Theory of finite or infinite trees revisited. Theory Pract. Log. Program., 8(4):431-489, 2008. URL: https://doi.org/10.1017/S1471068407003171.
  23. Matthias Felleisen and Daniel P. Friedman. A little Java, a few patterns. MIT Press, 1996. Google Scholar
  24. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for java. In Jens Knoop and Laurie J. Hendren, editors, Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pages 234-245. ACM, 2002. URL: https://doi.org/10.1145/512529.512558.
  25. Maurizio Gabbrielli, Simone Martini, and Saverio Giallorenzo. Programming languages: principles and paradigms, Second Edition. Undergraduate Topics in Computer Science. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-34144-1.
  26. Catarina Gamboa, Paulo Canelas, Christopher Steven Timperley, and Alcides Fonseca. Usability-oriented design of liquid types for java. In 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023, pages 1520-1532. IEEE, 2023. URL: https://doi.org/10.1109/ICSE48619.2023.00132.
  27. Simon J. Gay, Nils Gesbert, António Ravara, and Vasco Thudichum Vasconcelos. Modular session types for objects. Log. Methods Comput. Sci., 11(4), 2015. URL: https://doi.org/10.2168/LMCS-11(4:12)2015.
  28. James Gosling, William N. Joy, and Guy L. Steele Jr. The Java Language Specification. Addison-Wesley, 1996. Google Scholar
  29. Jad Hamza, Nicolas Voirol, and Viktor Kuncak. System FR: formalized foundations for the stainless verifier. Proc. ACM Program. Lang., 3(OOPSLA):166:1-166:30, 2019. URL: https://doi.org/10.1145/3360592.
  30. Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler. Featherweight java: a minimal core calculus for java and GJ. ACM Trans. Program. Lang. Syst., 23(3):396-450, 2001. URL: https://doi.org/10.1145/503502.503505.
  31. Bart Jacobs. Objects and classes, co-algebraically. In Burkhard Freitag, Cliff B. Jones, Christian Lengauer, and Hans-Jörg Schek, editors, Object Orientation with Parallelism and Persistence (the book grow out of a Dagstuhl Seminar in April 1995), pages 83-103. Kluwer Academic Publishers, 1995. Google Scholar
  32. Ranjit Jhala and Niki Vazou. Refinement types: A tutorial. Found. Trends Program. Lang., 6(3-4):159-317, 2021. URL: https://doi.org/10.1561/2500000032.
  33. Milod Kazerounian, Niki Vazou, Austin Bourgerie, Jeffrey S. Foster, and Emina Torlak. Refinement types for ruby. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, volume 10747 of Lecture Notes in Computer Science, pages 269-290. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-73721-8_13.
  34. Kenneth L. Knowles and Cormac Flanagan. Compositional reasoning and decidable checking for dependent contract types. In Thorsten Altenkirch and Todd D. Millstein, editors, Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009, pages 27-38. ACM, 2009. URL: https://doi.org/10.1145/1481848.1481853.
  35. Daniel Kroening and Ofer Strichman. Decision procedures - an algorithmic point of view. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-74105-3.
  36. Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, and Werner Dietl. Scalability and precision by combining expressive type systems and deductive verification. Proc. ACM Program. Lang., 5(OOPSLA):1-29, 2021. URL: https://doi.org/10.1145/3485520.
  37. Nico Lehmann and Éric Tanter. Formalizing simple refinement types in coq. In 2nd International Workshop on Coq for Programming Languages (CoqPL’16), St. Petersburg, FL, USA, 2016. Google Scholar
  38. K Rustan M Leino. This is boogie 2. manuscript KRML, 178(131):9, 2008. Google Scholar
  39. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  40. K. Rustan M. Leino and Clément Pit-Claudel. Trigger selection strategies to stabilize program verifiers. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 361-381. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41528-4_20.
  41. Christof Löding, P. Madhusudan, and Lucas Peña. Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang., 2(POPL):10:1-10:30, 2018. URL: https://doi.org/10.1145/3158098.
  42. Julian Mackay, Hannes Mehnert, Alex Potanin, Lindsay Groves, and Nicholas Cameron. Encoding featherweight java with assignment and immutability using the coq proof assistant. In Wei-Ngan Chin and Aquinas Hobor, editors, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, FTfJP 2012, Beijing, China, June 12, 2012, pages 11-19. ACM, 2012. URL: https://doi.org/10.1145/2318202.2318206.
  43. P. Madhusudan, Gennaro Parlato, and Xiaokang Qiu. Decidable logics combining heap structures and data. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 611-622. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926455.
  44. Adithya Murali, Lucas Peña, Ranjit Jhala, and P. Madhusudan. Complete first-order reasoning for properties of functional programs. Proc. ACM Program. Lang., 7(OOPSLA2):1063-1092, 2023. URL: https://doi.org/10.1145/3622835.
  45. Adithya Murali, Lucas Peña, Christof Löding, and P. Madhusudan. A first-order logic with frames. ACM Trans. Program. Lang. Syst., 45(2):7:1-7:44, 2023. URL: https://doi.org/10.1145/3583057.
  46. Hanne Riis Nielson and Flemming Nielson. Semantics with applications, volume 104. Springer, 1992. Google Scholar
  47. Nathaniel Nystrom, Vijay A. Saraswat, Jens Palsberg, and Christian Grothoff. Constrained types for object-oriented languages. In Gail E. Harris, editor, Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN, USA, pages 457-474. ACM, 2008. URL: https://doi.org/10.1145/1449764.1449800.
  48. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. URL: https://doi.org/10.1016/J.TCS.2006.12.035.
  49. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 1-19. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_1.
  50. Johan Östlund and Tobias Wrigstad. Welterweight java. In Jan Vitek, editor, Objects, Models, Components, Patterns, 48th International Conference, TOOLS 2010, Málaga, Spain, June 28 - July 2, 2010. Proceedings, volume 6141 of Lecture Notes in Computer Science, pages 97-116. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13953-6_6.
  51. Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. Dynamic typing with dependent types. In Jean-Jacques Lévy, Ernst W. Mayr, and John C. Mitchell, editors, Exploring New Frontiers of Theoretical Informatics, IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), 22-27 August 2004, Toulouse, France, volume 155 of IFIP, pages 437-450. Kluwer/Springer, 2004. URL: https://doi.org/10.1007/1-4020-8141-3_34.
  52. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  53. Ruzica Piskac, Thomas Wies, and Damien Zufferey. Automating separation logic with trees and data. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 711-728. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_47.
  54. Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A decision procedure for separation logic in SMT. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 244-261, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_16.
  55. Reuben N. S. Rowe and Steffen van Bakel. Semantic types and approximation for featherweight java. Theor. Comput. Sci., 517:34-74, 2014. URL: https://doi.org/10.1016/J.TCS.2013.08.017.
  56. Georg Stefan Schmid and Viktor Kuncak. Smt-based checking of predicate-qualified types for scala. In Aggelos Biboudis, Manohar Jonnalagedda, Sandro Stucki, and Vlad Ureche, editors, Proceedings of the 7th ACM SIGPLAN Symposium on Scala, SCALA@SPLASH 2016, Amsterdam, Netherlands, October 30 - November 4, 2016, pages 31-40. ACM, 2016. URL: https://doi.org/10.1145/2998392.2998398.
  57. Peter H. Schmitt and Mattias Ulbrich. Axiomatization of typed first-order logic. In Nikolaj S. Bjørner and Frank S. de Boer, editors, FM 2015: Formal Methods - 20th International Symposium, Oslo, Norway, June 24-26, 2015, Proceedings, volume 9109 of Lecture Notes in Computer Science, pages 470-486. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19249-9_29.
  58. Thomas Studer. Constructive foundations for featherweight java. In Reinhard Kahle, Peter Schroeder-Heister, and Robert F. Stärk, editors, Proof Theory in Computer Science, International Seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings, volume 2183 of Lecture Notes in Computer Science, pages 202-238. Springer, 2001. URL: https://doi.org/10.1007/3-540-45504-3_13.
  59. Ke Sun, Sheng Chen, Meng Wang, and Dan Hao. What types are needed for typing dynamic objects? A python-based empirical study. In Chung-Kil Hur, editor, Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, volume 14405 of Lecture Notes in Computer Science, pages 24-45. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_2.
  60. Ke Sun, Yifan Zhao, Dan Hao, and Lu Zhang. Static type recommendation for python. In 37th IEEE/ACM International Conference on Automated Software Engineering, ASE 2022, Rochester, MI, USA, October 10-14, 2022, pages 98:1-98:13. ACM, 2022. URL: https://doi.org/10.1145/3551349.3561150.
  61. Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, and Santiago Zanella Béguelin. Dependent types and multi-monadic effects in F. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256-270. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837655.
  62. William W. Tait. Intensional interpretations of functionals of finite type I. J. Symb. Log., 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  63. Emina Torlak and Rastislav Bodík. Growing solver-aided languages with rosette. In Antony L. Hosking, Patrick Th. Eugster, and Robert Hirschfeld, editors, ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH '13, Indianapolis, IN, USA, October 26-31, 2013, pages 135-152. ACM, 2013. URL: https://doi.org/10.1145/2509578.2509586.
  64. Steffen van Bakel and Maribel Fernández. Normalization, approximation, and semantics for combinator systems. Theor. Comput. Sci., 290(1):975-1019, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00548-0.
  65. Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones. Refinement types for haskell. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014, pages 269-282. ACM, 2014. URL: https://doi.org/10.1145/2628136.2628161.
  66. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler, and Ranjit Jhala. Refinement reflection: complete verification with SMT. Proc. ACM Program. Lang., 2(POPL):53:1-53:31, 2018. URL: https://doi.org/10.1145/3158141.
  67. Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. Refinement types for typescript. In Chandra Krintz and Emery D. Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 310-325. ACM, 2016. URL: https://doi.org/10.1145/2908080.2908110.
  68. Peng Wang, Di Wang, and Adam Chlipala. Timl: a functional language for practical complexity analysis with invariants. Proc. ACM Program. Lang., 1(OOPSLA):79:1-79:26, 2017. URL: https://doi.org/10.1145/3133903.
  69. Stefan Wehr, Ralf Lämmel, and Peter Thiemann. Javagi : Generalized interfaces for java. In Erik Ernst, editor, ECOOP 2007 - Object-Oriented Programming, 21st European Conference, Berlin, Germany, July 30 - August 3, 2007, Proceedings, volume 4609 of Lecture Notes in Computer Science, pages 347-372. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73589-2_17.
  70. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Inf. Comput., 115(1):38-94, 1994. URL: https://doi.org/10.1006/INCO.1994.1093.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact