Abstract
Dependent refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness.
Chapter PDF
Similar content being viewed by others
References
Aguirre, A., Katsumata, S.: Weakest preconditions in fibrations. In: Proceedings of the Thirty-Sixth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2020, Paris, France (June 2020), to appear
Ahman, D.: Fibred Computational Effects. PhD Thesis, University of Edinburgh (2017)
Ahman, D.: Handling fibred algebraic effects. Proceedings of the ACM on Programming Languages 2, 1–29 (Jan 2018). https://doi.org/10.1145/3158095
Ahman, D., Ghani, N., Plotkin, G.D.: Dependent types and fibred computational effects. In: Jacobs, B., Löding, C. (eds.) Foundations of Software Science and Computation Structures, vol. 9634, pp. 36–54. Springer Berlin Heidelberg (2016). https://doi.org/10.1007/978-3-662-49630-5_3
Barthe, G., Gaboardi, M., Gallego Arias, E.J., Hsu, J., Roth, A., Strub, P.Y.: Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’15. pp. 55–68. ACM Press, Mumbai, India (2015). https://doi.org/10.1145/2676726.2677000
Flanagan, C.: Hybrid type checking. In: Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL’06. pp. 245–256. ACM Press, Charleston, South Carolina, USA (2006). https://doi.org/10.1145/1111037.1111059
Freeman, T., Pfenning, F.: Refinement types for ML. ACM SIGPLAN Notices 26(6), 268–277 (Jun 1991). https://doi.org/10.1145/113446.113468
Fujii, S., Katsumata, S.y., Melliès, P.A.: Towards a Formal Theory of Graded Monads. In: Jacobs, B., Löding, C. (eds.) Foundations of Software Science and Computation Structures, vol. 9634, pp. 513–530. Springer Berlin Heidelberg, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49630-5_30
Hermida, C.: Fibrations, logical predicates and indeterminates. PhD Thesis, University of Edinburgh, UK (1993)
Jacobs, B.: Categorical Logic and Type Theory. No. 141 in Studies in Logic and the Foundations of Mathematics, Elsevier, paperback edn. (2001)
Katsumata, S.: Parametric effect monads and semantics of effect systems. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’14. pp. 633–645. ACM Press, San Diego, California, USA (2014). https://doi.org/10.1145/2535838.2535846
Katsumata, S.: private communication (2020)
Knowles, K., Flanagan, C.: Compositional reasoning and decidable checking for dependent contract types. In: Proceedings of the 3rd Workshop on Programming Languages Meets Program Verification - PLPV ’09. p. 27. ACM Press, Savannah, GA, USA (2008). https://doi.org/10.1145/1481848.1481853
Lehmann, N., Tanter, É.: Gradual refinement types. ACM SIGPLAN Notices 52(1), 775–788 (May 2017). https://doi.org/10.1145/3093333.3009856
McDermott, D., Mycroft, A.: Extended Call-by-Push-Value: Reasoning About Effectful Programs and Evaluation Order. In: Caires, L. (ed.) Programming Languages and Systems, vol. 11423, pp. 235–262. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_9
Melliès, P.A., Zeilberger, N.: Functors are Type Refinement Systems. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL ’15. pp. 3–16. ACM Press, Mumbai, India (2015). https://doi.org/10.1145/2676726.2676970
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (Jul 1991). https://doi.org/10.1016/0890-5401(91)90052-4
Ou, X., Tan, G., Mandelbaum, Y., Walker, D.: Dynamic Typing with Dependent Types. In: Levy, J.J., Mayr, E.W., Mitchell, J.C. (eds.) Exploring New Frontiers of Theoretical Informatics, vol. 155, pp. 437–450. Kluwer Academic Publishers, Boston (2004). https://doi.org/10.1007/1-4020-8141-3_34
Rondon, P.M., Kawaguci, M., Jhala, R.: Liquid types. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’08. p. 159. ACM Press, Tucson, AZ, USA (2008). https://doi.org/10.1145/1375581.1375602
Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS. IEEE Transactions on Software Engineering 24(9), 709–720 (Sept/1998). https://doi.org/10.1109/32.713327
Sato, T., Barthe, G., Gaboardi, M., Hsu, J., Katsumata, S.y.: Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–14. IEEE, Vancouver, BC, Canada (Jun 2019). https://doi.org/10.1109/LICS.2019.8785668
Simpson, A., Plotkin, G.: Complete axioms for categorical fixed-point operators. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332). pp. 30–41. IEEE Comput. Soc, Santa Barbara, CA, USA (2000). https://doi.org/10.1109/LICS.2000.855753
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. Journal of Functional Programming 23(4), 402–451 (Jul 2013). https://doi.org/10.1017/S0956796813000142
Swamy, N., Weinberger, J., Schlesinger, C., Chen, J., Livshits, B.: Verifying higher-order programs with the dijkstra monad. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI ’13. p. 387. ACM Press, Seattle, Washington, USA (2013). https://doi.org/10.1145/2491956.2491978
Unno, H., Satake, Y., Terauchi, T.: Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proceedings of the ACM on Programming Languages 2, 1–29 (Jan 2018). https://doi.org/10.1145/3158100
Vazou, N., Rondon, P.M., Jhala, R.: Abstract Refinement Types. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems, vol. 7792, pp. 209–228. Springer Berlin Heidelberg, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-642-37036-6_13
Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton-Jones, S.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming - ICFP ’14. pp. 269–282. ACM Press, Gothenburg, Sweden (2014). https://doi.org/10.1145/2628136.2628161
Xi, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation - PLDI ’98. pp. 249–257. ACM Press, Montreal, Quebec, Canada (1998). https://doi.org/10.1145/277650.277732
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Kura, S. (2021). A General Semantic Construction of Dependent Refinement Type Systems, Categorically. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_21
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_21
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)