zbMATH — the first resource for mathematics

Extensible datasort refinements. (English) Zbl 06721332
Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer (ISBN 978-3-662-54433-4/pbk; 978-3-662-54434-1/ebook). Lecture Notes in Computer Science 10201, 476-503 (2017).
Summary: Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes.
Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type definitions, and consequently, duplicating code.
We enrich the traditional notion of a signature, which describes the inhabitants of datasorts, to allow re-refinement via signature extension, without duplicating definitions. Since arbitrary updates to a signature can invalidate the inversion principles used to check case expressions, we develop a definition of signature well-formedness that ensures that extensions maintain existing inversion principles. This definition allows different parts of a program to extend the same signature in different ways, without conflicting with each other. Each part can be type-checked independently, allowing separate compilation.
For the entire collection see [Zbl 1360.68021].
68Nxx Theory of software
Full Text: DOI
[1] Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2008). https://gforge.inria.fr/frs/download.php/file/10994/tata.pdf
. Accessed 18 Nov 2008
[2] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977) · doi:10.1145/512950.512973
[3] Davies, R.: Practical refinement-type checking. Ph.D. thesis, Carnegie Mellon University, CMU-CS-05-110 (2005)
[4] Davies, R.: SML checker for intersection and datasort refinements (pronounced ”cider”) (2013). https://github.com/rowandavies/sml-cidre
[5] Davies, R., Pfenning, F.: Intersection types and computational effects. In: ICFP, pp. 198–208 (2000) · Zbl 1321.68147 · doi:10.1145/351240.351259
[6] Dunfield, J.: Refined typechecking with stardust. In: Programming Languages Meets Program Verification (PLPV 2007) (2007a) · doi:10.1145/1292597.1292602
[7] Dunfield, J.: A unified system of type refinements. Ph.D. thesis, Carnegie Mellon University, CMU-CS-07-129 (2007b)
[8] Dunfield, J., Krishnaswami, N.R.: Complete and easy bidirectional typechecking for higher-rank polymorphism. In: ICFP (2013). arXiv:1306.6032 · Zbl 1323.68204
[9] Dunfield, J., Pfenning, F.: Type assignment for intersections and unions in call-by-value languages. In: Gordon, A.D. (ed.) FoSSaCS 2003. LNCS, vol. 2620, pp. 250–266. Springer, Heidelberg (2003). doi: 10.1007/3-540-36576-1_16 · Zbl 1029.68098 · doi:10.1007/3-540-36576-1_16
[10] Dunfield, J., Pfenning, F.: Tridirectional typechecking. In: Principles of Programming Languages, pp. 281–292 (2004) · Zbl 1325.68062 · doi:10.1145/964001.964025
[11] Freeman, T.: Refinement types for ML. Ph.D. thesis, Carnegie Mellon University, CMU-CS-94-110 (1994)
[12] Freeman, T., Pfenning, F.: Refinement types for ML. In: Programming Language Design and Implementation, pp. 268–277 (1991) · doi:10.1145/113445.113468
[13] Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, 176–210, 405–431 (1934). English translation, Investigations into logical deduction. In: Szabo, M. (ed.) Collected Papers of Gerhard Gentzen, pp. 68–131. North-Holland (1969) · JFM 60.0020.02
[14] Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. ACM 40(1), 143–184 (1993) · Zbl 0778.03004 · doi:10.1145/138027.138060
[15] Kennedy, A.: Programming languages and dimensions. Ph.D. thesis, University of Cambridge (1996)
[16] Koot, R., Hage, J.: Type-based exception analysis for non-strict higher-order functional languages with imprecise exception semantics. In: Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pp. 127–138 (2015) · doi:10.1145/2678015.2682542
[17] Lovas, W.: Refinement types for logical frameworks. Ph.D. thesis, Carnegie Mellon University, CMU-CS-10-138 (2010) · Zbl 1202.68108
[18] Pfenning, F., Schürmann, C.: System description: Twelf–a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999). doi: 10.1007/3-540-48660-7_14 · doi:10.1007/3-540-48660-7_14
[19] Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 15–21. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14203-1_2 · Zbl 1291.68366 · doi:10.1007/978-3-642-14203-1_2
[20] Poswolsky, A., Schürmann, C.: System description: Delphin–a functional programming language for deductive systems. In: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008). Electronic Notes in Theoretical Computer Science, vol. 228, pp. 135–141 (2009) · Zbl 06578013 · doi:10.1016/j.entcs.2008.12.120
[21] Reynolds, J.C.: Types, abstraction, and parametric polymorphism. In: Information Processing 83, pp. 513–523. Elsevier (1983). http://www.cs.cmu.edu/afs/cs/user/jcr/ftp/typesabpara.pdf
[22] Reynolds, J.C.: Design of the programming language Forsythe. Technical report CMU-CS-96-146, Carnegie Mellon University (1996)
[23] Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: Programming Language Design and Implementation, pp. 159–169 (2008) · doi:10.1145/1375581.1375602
[24] Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-37036-6_13 · Zbl 1381.68038 · doi:10.1007/978-3-642-37036-6_13
[25] Wright, A.K.: Simple imperative polymorphism. Lisp Symbolic Comput. 8(4), 343–355 (1995) · Zbl 05478828 · doi:10.1007/BF01018828
[26] Xi, H.: Dependent types in practical programming. Ph.D. thesis, Carnegie Mellon University (1998)
[27] Xi, H., Pfenning, F.: Dependent types in practical programming. In: Principles of Programming Languages, pp. 214–227 (1999) · doi:10.1145/292540.292560
[28] Zeilberger, N.: The logical basis of evaluation order and pattern-matching. Ph.D. thesis, Carnegie Mellon University, CMU-CS-09-122 (2009)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.