Abstract
We present an extension of System F with types for term-level equations. This internalization of the rich equational theory of the polymorphic lambda calculus yields an expressive core language, suitable for formalizing features such as Haskell’s rewriting rules mechanism or Extended ML signatures.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. In: Principles of Programming Languages, pp. 157–170 (1993)
Abel, A.: Weak βη-Normalization and Normalization by Evaluation for System F. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 497–511. Springer, Heidelberg (2008)
Atkey, R.: Syntax for Free: Representing Syntax with Binding Using Parametricity. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 35–49. Springer, Heidelberg (2009)
Bellucci, R., Abadi, M., Curien, P.-L.: A Model for Formal Parametric Polymorphism: A PER Interpretation for System R. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol. 902, pp. 32–46. Springer, Heidelberg (1995)
Bernardy, J.-P., Jansson, P., Paterson, R.: Parametricity and dependent types. In: Hudak, P., Weirich, S. (eds.) Proceeding of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP 2010, pp. 345–356. ACM (2010)
Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Domain-theoretical models of parametric polymorphism. Theoretical Computer Science 388(1-3), 152–172 (2007)
Birkedal, L., Støvring, K., Thamsborg, J.: Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science 20(4), 655–703 (2010)
Cardelli, L., Leroy, X.: Abstract types and the dot notation. In: Broy, M., Jones, C.B. (eds.) Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 479–504. North-Holland (1990)
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 (1986)
Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)
Jones, S.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Reppy, J.H., Lawall, J.L. (eds.) Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, pp. 50–61. ACM (2006)
Jones, S.P., Tolmach, A., Hoare, T.: Playing by the rules: rewriting as a practical optimisation technique in GHC. In: Haskell Workshop (2001)
Kahrs, S., Sannella, D., Tarlecki, A.: The definition of Extended ML: A gentle introduction. Theoretical Computer Science 173(2), 445–484 (1997)
Krishnaswami, N.R.: Verifying Higher-Order Imperative Programs with Higher-Order Separation Logic. PhD thesis, Carnegie Mellon University (2011)
Marlow, S., Wadler, P.: Deforestation for higher-order functions. In: Launchbury, J., Sansom, P.M. (eds.) Functional Programming, Workshops in Computing, pp. 154–165. Springer, Heidelberg (1992)
Martin-Löf, P.: Intuitionistic Type Theory. Bibliopolis (1984)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10, 470–502 (1988)
Neis, G., Dreyer, D., Rossberg, A.: Non-parametric parametricity. In: Hutton, G., Tolmach, A.P. (eds.) Proceeding of the 14th ACM SIGPLAN International Conference on Functional Programming, pp. 135–148. ACM (2009)
Plotkin, G.D., Abadi, M.: A Logic for Parametric Polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513–523 (1983)
Rossberg, A., Russo, C.V., Dreyer, D.: F-ing modules. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2010, ACM (2010)
Wadler, P.: The Girard-Reynolds isomorphism (second edition). Theoretical Computer Science 375(1-3), 201–226 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Krishnaswami, N.R., Benton, N. (2012). Adding Equations to System F Types. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)