A classical realizability model for a semantical value restriction. (English) Zbl 1335.68059
Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 476-502 (2016).
Summary: We present a new type system with support for proofs of programs in a call-by-value language with control operators. The proof mechanism relies on observational equivalence of (untyped) programs. It appears in two type constructors, which are used for specifying program properties and for encoding dependent products. The main challenge arises from the lack of expressiveness of dependent products due to the value restriction. To circumvent this limitation we relax the syntactic restriction and only require equivalence to a value. The consistency of the system is obtained semantically by constructing a classical realizability model in three layers (values, stacks and terms).
For the entire collection see [Zbl 1333.68019].
For the entire collection see [Zbl 1333.68019].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Casinghino, C., Sjberg, V., Weirich, S.: Combining proofs and programs in a dependently typed language. In: Jagannathan, S., Sewell, P. (eds.) 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 33–46. ACM, San Diego (2014) · Zbl 1284.68125 · doi:10.1145/2535838.2535883 |
| [2] | Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice Hall, Upper Saddle River (1986) |
| [3] | Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2–3), 95–120 (1988) · Zbl 0654.03045 · doi:10.1016/0890-5401(88)90005-3 |
| [4] | Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1982, pp. 207–212. ACM, New York (1982) · doi:10.1145/582153.582176 |
| [5] | Garrigue, J.: Relaxing the value restriction. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 196–213. Springer, Heidelberg (2004) · Zbl 1122.68398 · doi:10.1007/978-3-540-24754-8_15 |
| [6] | Griffin, T.G.: A formulæ-as-types notion of control. In: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pp. 47–58. ACM Press (1990) · doi:10.1145/96709.96714 |
| [7] | Harper, R., Lillibridge, M.: ML with callcc is unsound (1991). http://www.seas.upenn.edu/ sweirich/types/archive/1991/msg00034.html |
| [8] | Howe, D.J.: Equality in lazy computation systems. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS 1989), 5–8 June 1989, Pacific Grove, California, USA, pp. 198–203 (1989) · Zbl 0716.68065 · doi:10.1109/LICS.1989.39174 |
| [9] | Hyvernat, P.: The size-change termination principle for constructor based languages. Logical Methods Comput. Sci. 10(1) (2014). http://www.lmcs-online.org/ojs/viewarticle.php?id=1409&layout=abstract · Zbl 1325.68048 |
| [10] | Jia, L., Vaughan, J.A., Mazurak, K., Zhao, J., Zarko, L., Schorr, J., Zdancewic, S.: AURA: a programming language for authorization and audit. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, 20–28 September 2008, Victoria, BC, Canada, pp. 27–38. ACM (2008) · Zbl 1323.68078 · doi:10.1145/1411204.1411212 |
| [11] | Krivine, J.: A call-by-name lambda-calculus machine. Higher-Order Symb. Comput. 20(3), 199–207 (2007) · Zbl 1130.68057 · doi:10.1007/s10990-007-9018-9 |
| [12] | Krivine, J.: Realizability in classical logic. In: Interactive Models of Computation and Program Behaviour, Panoramas et synthèses, vol. 27, pp. 197–229. Société Mathématique de France (2009) |
| [13] | Lepigre, R.: A realizability model for a semantical value restriction (2015). https://lama.univ-savoie.fr/ lepigre/files/docs/semvalrest2015.pdf · Zbl 1335.68059 |
| [14] | Leroy, X.: Polymorphism by name for references and continuations. In: 20th Symposium Principles of Programming Languages, pp. 220–231. ACM Press (1993) · doi:10.1145/158511.158632 |
| [15] | Leroy, X., Weis, P.: Polymorphic type inference and assignment. In: Proceedings of the 18th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language, POPL 1991, pp. 291–302. ACM, New York (1991) · doi:10.1145/99583.99622 |
| [16] | Licata, D.R., Harper, R.: Positively dependent types. In: Altenkirch, T., Millstein, T.D. (eds.) Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLpPV 2009, 20 January 2009, Savannah, GA, USA, pp. 3–14. ACM (2009) |
| [17] | Martin-Löf, P.: Constructive mathematics and computer programming. In: Cohen, L.J., Pfeiffer, H., Podewski, K.P. (eds.) Logic, Methodology and Philosophy of Science VI, Studies in Logic and the Foundations of Mathematics, vol. 104, pp. 153–175. North-Holland (1982) · Zbl 0541.03034 · doi:10.1016/S0049-237X(09)70189-2 |
| [18] | The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2004). http://coq.inria.fr |
| [19] | Mendler, N.P.: Recursive types and type constraints in second-order lambda calculus. In: Proceedings of the Symposium on Logic in Computer Science (LICS 1987), pp. 30–36 (1987) |
| [20] | Miquel, A.: Le Calcul des constructions implicites: syntaxe et Sémantique. Ph.D. thesis, Université Paris VII (2001) |
| [21] | Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 409–423. Springer, Heidelberg (2009) · Zbl 1257.03055 · doi:10.1007/978-3-642-04027-6_30 |
| [22] | Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009) · Zbl 1263.68038 · doi:10.1007/978-3-642-04652-0_5 |
| [23] | Owre, S., Rajan, S., Rushby, J., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411–414. Springer, Heidelberg (1996) · doi:10.1007/3-540-61474-5_91 |
| [24] | Parigot, M.: \[ \lambda \mu \] {\(\lambda\)} {\(\mu\)} -calculus: an algorithmic interpretation of classical. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992) · Zbl 0925.03092 · doi:10.1007/BFb0013061 |
| [25] | Raffalli, C.: L’Arithmétiques Fonctionnelle du Second Ordre avec Points Fixes. Ph.D. thesis, Université Paris VII (1994) |
| [26] | Raffalli, C.: A normaliser for pure and typed \[ \lambda \] {\(\lambda\)} -calculus (1996). http://lama.univ-savoie.fr/ raffalli/normaliser.html |
| [27] | Raffalli, C.: The PML programming language. LAMA - Université Savoie Mont-Blanc (2012). http://lama.univ-savoie.fr/tracpml/ |
| [28] | Swamy, N., Chen, J., Fournet, C., Strub, P., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, 19–21 September 2011, Tokyo, Japan, pp. 266–278. ACM (2011) · Zbl 1323.68229 · doi:10.1145/2034773.2034811 |
| [29] | Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1–34 (1990) · Zbl 0705.68028 · doi:10.1016/0890-5401(90)90018-D |
| [30] | Wright, A.K.: Simple imperative polymorphism. LISP Symb. Comput. 8, 343–356 (1995) · doi:10.1007/BF01018828 |
| [31] | Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994) · Zbl 0938.68559 · doi:10.1006/inco.1994.1093 |
| [32] | Xi, H.: Applied type system. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 394–408. Springer, Heidelberg (2004) · Zbl 1100.03518 · doi:10.1007/978-3-540-24849-1_25 |
| [33] | Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214–227, San Antonio, January 1999 · doi:10.1145/292540.292560 |
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.
