Nested refinements: a logic for duck typing. (English) Zbl 1321.68189
Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 231-244 (2012).
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 03B70 | Logic in computer science |
| 68N19 | Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) |
References:
| [1] | M. Abadi, L. Cardelli, B. C. Pierce, and G. Plotkin. Dynamic typing in a statically-typed language. In POPL, 1989. 10.1145/75277.75296 |
| [2] | J.-h. D. An, A. Chaudhuri, J. S. Foster, and M. Hicks. Dynamic inference of static types for ruby. In POPL, 2011. 10.1145/1926385.1926437 |
| [3] | C. Anderson, S. Drossopoulou, and P. Giannini. Towards Type Inference for JavaScript. In ECOOP, pages 428-452, June 2005. 10.1007/11531142_19 |
| [4] | J. Bengtson, K. Bhargavan, C. Fournet, A. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF, 2008. 10.1109/CSF.2008.27 |
| [5] | Y. Bertot and P. Castéran. Interactive theorem proving and program development. coq’art: The calculus of inductive constructions, 2004. · Zbl 1069.68095 |
| [6] | G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic subtyping with an smt solver. In ICFP, 2010. 10.1145/1863543.1863560 |
| [7] | A. R. Bradley, Z. Manna, and H. B. Sipma. What’s decidable about arrays? In VMCAI, pages 427-442, 2006. 10.1007/11609773_28 · Zbl 1176.68116 |
| [8] | R. Chugh, P. M. Rondon, and R. Jhala. Nested refinements: A logic for duck typing. http://arxiv.org/abs/1103.5055v2. |
| [9] | R. Chugh, J. A. Meister, R. Jhala, and S. Lerner. Staged information flow for javascript. In Proceedings of PLDI 2009, pages 50-62, 2009. 10.1145/1542476.1542483 |
| [10] | J. Condit, B. Hackett, S. K. Lahiri, and S. Qadeer. Unifying type checking and property checking for low-level code. In POPL, 2009. 10.1145/1480881.1480921 · Zbl 1315.68086 |
| [11] | R. Davies. Practical Refinement-Type Checking. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2005. |
| [12] | L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008. |
| [13] | L. de Moura and N. Bjørner. Generalized, efficient array decision procedures. In FMCAD, pages 45-52, 2009. |
| [14] | J. Dunfield. A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA, 2007. |
| [15] | R. B. Findler and M. Felleisen. Contracts for higher-order functions. In ICFP, pages 48-59, 2002. 10.1145/581478.581484 · Zbl 1322.68039 |
| [16] | C. Flanagan. Hybrid type checking. In POPL. ACM, 2006. 10.1145/1111037.1111059 |
| [17] | M. Furr, J. hoon (David) An, J. S. Foster, and M. W. Hicks. Static type inference for ruby. In SAC, pages 1859-1866, 2009. 10.1145/1529282.1529700 |
| [18] | A. Guha, C. Softoiu, and S. Krishnamurthi. Typing local control and state using flow analysis. In ESOP, 2011. |
| [19] | P. Heidegger and P. Thiemann. Recency types for analyzing scripting languages. In ECOOP, pages 200-224, 2010. |
| [20] | P. Hooimeijer and M. Veanes. An evaluation of automata algorithms for string analysis. In VMCAI, pages 248-262, 2011. · Zbl 1317.68287 |
| [21] | R. Jhala, R. Majumdar, and R.-G. Xu. State of the union: Type inference via craig interpolation. In TACAS, 2007. |
| [22] | A. J. Kennedy and B. C. Pierce. On decidability of nominal subtyping with variance. In FOOL-WOOD, 2007. |
| [23] | K. Knowles and C. Flanagan. Hybrid type checking. ACM TOPLAS, 32 (2), 2010. 10.1145/1667048.1667051 |
| [24] | R. Komondoor, G. Ramalingam, S. Chandra, and J. Field. Dependent types for program understanding. In TACAS, pages 157-173, 2005. 10.1007/978-3-540-31980-1_11 · Zbl 1087.68544 |
| [25] | J. McCarthy. Towards a mathematical science of computation. In In IFIP Congress, pages 21-28. North-Holland, 1962. |
| [26] | G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. TOPLAS, 1979. 10.1145/357073.357079 · Zbl 0452.68013 |
| [27] | X. Ou, G. Tan, Y. Mandelbaum, and D. Walker. Dynamic typing with dependent types. In IFIP TCS, pages 437-450, 2004. · Zbl 1088.68531 |
| [28] | J. Palsberg and M. I. Schwartzbach. OO Type Systems. Wiley, 1994. · Zbl 0821.68023 |
| [29] | B. C. Pierce and D. N. Turner. Local type inference. In POPL, pages 252-265, 1998. 10.1145/268946.268967 |
| [30] | D. Rémy. Type checking records and variants in a natural extension of ml. In POPL, 1989. 10.1145/75277.75284 |
| [31] | P. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, 2008. 10.1145/1375581.1375602 |
| [32] | P. Rondon, M. Kawaguchi, and R. Jhala. Low-level liquid types. In POPL, pages 131-144, 2010. 10.1145/1706299.1706316 · Zbl 1312.68033 |
| [33] | R. Shostak. Deciding combinations of theories. Journal of the ACM, 31 (1): 1-12, 1984. 10.1145/2422.322411 · Zbl 0629.68089 |
| [34] | J. Siek and W. Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, 2006. |
| [35] | N. Swamy, J. Chen, and R. Chugh. Enforcing stateful authorization and information flow policies in fine. In ESOP, 2010. 10.1007/978-3-642-11957-6_28 |
| [36] | The Dojo Foundation. Dojo toolkit. http://dojotoolkit.org/. |
| [37] | }python-32The Python Software Foundation. Python 3.2 standard library. http://python.org/. |
| [38] | P. Thiemann. Towards a type system for analyzing javascript programs. In ESOP, 2005. 10.1007/978-3-540-31987-0_28 |
| [39] | S. Tobin-Hochstadt and M. Felleisen. Logical types for untyped languages. In ICFP, pages 117-128, 2010. 10.1145/1863543.1863561 · Zbl 1323.68083 |
| [40] | H. Xi and F. Pfenning. Dependent types in practical programming. In POPL, 1999. 10.1145/292540.292560 |
| [41] | T. Zhao. Type inference for scripting languages with implicit extension. In FOOL, 2010. |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
