Abstract
Modern programming languages have effects and mix multiple calling conventions, and their core calculi should too. We characterize calling conventions by their “substitution discipline” that says what variables stand for, and design calculi for mixing disciplines in a single program. Building on variations of the reducibility candidates method, including biorthogonality and symmetric candidates which are both specialized for one discipline, we develop a single uniform framework for strong normalization encompassing call-by-name, call-by-value, call-by-need, call-by-push-value, non-deterministic disciplines, and any others satisfying some simple criteria. We explicate commonalities of previous methods and show they are special cases of the uniform framework and they extend to multi-discipline programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ariola, Z.M., Herbelin, H., Saurin, A.: Classical call-by-need and duality. In: TLCA 2011 (2011)
Barbanera, F., Berardi, S.: A symmetric lambda calculus for “classical” program extraction. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 495–515. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-57887-0_112
Curien, P.L., Herbelin, H.: The duality of computation. In: ICFP 2000 (2000)
Downen, P., Ariola, Z.M.: The duality of construction. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 249–269. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54833-8_14
Downen, P., Johnson-Freyd, P., Ariola, Z.M.: Structures for structural recursion. In: ICFP 2015 (2015)
Girard, J.Y.: Interprétation fonctionnelle et elimination des coupures de l’arithmétique d’ordre supérieur. These d’état, Université de Paris 7 (1972)
Girard, J.Y.: Linear logic. Theoret. Comput. Sci. 50, 1–102 (1987)
Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, New York (1989)
Graham-Lengrand, S.: Polarities & Focussing: a journey from Realisability to Automated Reasoning. Habilitation thesis, Université Paris-Sud (2014)
Herbelin, H., Zimmermann, S.: An operational account of call-by-value minimal and classical \(\lambda \)-calculus in “natural deduction” form. In: TLCA 2009 (2009)
Kleene, S.C.: On the interpretation of intuitionistic number theory. J. Symbolic Logic 10(4), 109–124 (1945)
Krivine, J.L.: A call-by-name lambda-calculus machine. High. Order Symbolic Comput. 20(3), 199–207 (2007)
Krivine, J.L.: Realizability in classical logic. In: Interactive models of computation and program behaviour, vol. 27. Société Mathématique de France (2009)
Lengrand, S., Miquel, A.: Classical F\(\omega \), orthogonality and symmetric candidates. Ann. Pure Appl. Logic 153(1), 3–20 (2008)
Levy, P.B.: Call-By-Push-Value. Ph.D. thesis, University of London, August 2001
Liskov, B.: Keynote address-data abstraction and hierarchy. In: OOPSLA 1987 (1987)
Munch-Maccagnoni, G.: Focalisation and classical realisability. In: CSL 2009 (2009)
Munch-Maccagnoni, G.: Syntax and Models of a non-Associative Composition of Programs and Proofs. Ph.D. thesis, Université Paris Diderot (2013)
Peyton Jones, S.: https://www.red-gate.com/simple-talk/opinion/geek-of-the-week/simon-peyton-jones-geek-of-the-week/
Peyton Jones, S.L., Launchbury, J.: Unboxed values as first class citizens in a non-strict functional language. In: FPCA, pp. 636–666 (1991)
Pitts, A.M.: Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10(3), 321–359 (2000)
Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theoret. Comput. Sci. 1, 125–159 (1975)
Ronchi Della Rocca, S., Paolini, L.: The Parametric \(\lambda \)-Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-10394-4
Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LFP 1992, pp. 288–298 (1992)
Tait, W.W.: Intensional interpretations of functionals of finite type I. J. Symbolic Logic 32, 198–212 (1967)
Turbak, F., Gifford, D., Sheldon, M.A.: Design Concepts in Programming Languages. The MIT Press (2008)
Wadler, P.: Theorems for free! In: FPCA 1989 (1989)
Wadler, P.: Call-by-value is dual to call-by-name. In: ICFP 2003 (2003)
Wright, A., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38–94 (1994)
Zeilberger, N.: The logical basis of evaluation order and pattern-matching. Ph.D. thesis, Carnegie Mellon University (2009)
Acknowledgments
This work is supported by the National Science Foundation under grants CCF-1719158 and CCF-1423617.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Downen, P., Johnson-Freyd, P., Ariola, Z.M. (2018). Uniform Strong Normalization for Multi-discipline Calculi. In: Rusu, V. (eds) Rewriting Logic and Its Applications. WRLA 2018. Lecture Notes in Computer Science(), vol 11152. Springer, Cham. https://doi.org/10.1007/978-3-319-99840-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-99840-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99839-8
Online ISBN: 978-3-319-99840-4
eBook Packages: Computer ScienceComputer Science (R0)