Abstract
The Λμ-calculus is an extension of Parigot’s λμ-calculus. For the untyped Λμ-calculus, Saurin proved some fundamental properties such as the standardization and the separation theorem. Nakazawa and Katsumata gave extensional models, called stream models, in which terms are represented as functions on streams. This paper introduces a conservative extension of the Λμ-calculus, called Λμ cons , from which the open term model is straightforwardly constructed as a stream model, and for which we can define a reduction system satisfying several fundamental properties such as confluence, subject reduction, and strong normalization.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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
Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Ariola, Z.M., Klop, J.W.: Equational term graph rewriting. Fundamenta Informaticae 26(3-4), 207–240 (1996)
Carraro, A.: The untyped stack calculus and Böhm’s theorem. In: 7th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2012). Electric Proceedings in Theoretical Computer Science, vol. 113, pp. 77–92 (2012)
Carraro, A., Ehrhard, T., Salibra, A.: The stack calculus. In: 7th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2012). Electric Proceedings in Theoretical Computer Science, vol. 113, pp. 93–108 (2012)
David, R., Py, W.: λμ-calculus and Böhm’s theorem. The Journal of Symbolic Logic 66, 407–413 (2001)
de Groote, P.: A CPS-translation of the λμ-calculus. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, pp. 85–99. Springer, Heidelberg (1994)
Dehornoy, P., van Oostrom, V.Z.: Proving confluence by monotonic single-step upperbound functions. In: Logical Models of Reasoning and Computation, LMRC 2008 (2008)
de’Liguoro, U.: The approximation theorem for the Λμ-calculus. Mathematical Structures in Computer Science (to appear)
Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Logic Colloquium, pp. 22–37 (1973)
Gaboardi, M., Saurin, A.: A foundational calculus for computing with streams. In: 12th Italian Conference on Theoretical Computer Science (2010)
Komori, Y., Matsuda, N., Yamakawa, F.: A simplified proof of the church-rosser theorem. Studia Logica 101(1) (2013)
Milner, R.: A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences 28, 439–466 (1984)
Nakazawa, K.: Extensional models of typed lambda-mu caclulus (2014) (unpublished manuscript), http://www.fos.kuis.kyoto-u.ac.jp/~knak/papers/manuscript/typed-sm.pdf
Nakazawa, K., Katsumata, S.: Extensional models of untyped Lambda-mu calculus. In: Geuvers, H., de’Liguoro, U. (eds.) Proceedings Fourth Workshop on Classical Logic and Computation (CL&C 2012). Electric Proceedings in Theoretical Computer Science, vol. 97, pp. 35–47 (2012)
Pagani, M., Saurin, A.: Stream associative nets and λμ-calculus. Research Report 6431, INRIA (2008)
Parigot, M.: λμ-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Salomaa, A.: Two complete axiom systems for the algebra of regular events. Journal of the Associations for Computing Machinery 13(1), 158–169 (1966)
Saurin, A.: Separation with streams in the Λμ-calculus. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 356–365 (2005)
Saurin, A.: A hierarchy for delimited continuations in call-by-name. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 374–388. Springer, Heidelberg (2010)
Saurin, A.: Standardization and Böhm trees for Λμ-calculus. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 134–149. Springer, Heidelberg (2010)
Saurin, A.: Typing streams in the Λμ-calculus. ACM Transactions on Computational Logic 11 (2010)
Streicher, T., Reus, B.: Classical logic, continuation semantics and abstract machines. Journal of Functional Programming 8(6), 543–572 (1998)
Thielecke, H.: Categorical structure of continuation passing style. PhD thesis, University of Edinburgh (1997)
van Bakel, S., Barbanera, F., de’Liguoro, U.: A filter model for the λμ-calculus. In: Ong, L. (ed.) Typed Lambda Calculi and Applications. LNCS, vol. 6690, pp. 213–228. Springer, Heidelberg (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Nakazawa, K., Nagai, T. (2014). Reduction System for Extensional Lambda-mu Calculus. In: Dowek, G. (eds) Rewriting and Typed Lambda Calculi. RTA TLCA 2014 2014. Lecture Notes in Computer Science, vol 8560. Springer, Cham. https://doi.org/10.1007/978-3-319-08918-8_24
Download citation
DOI: https://doi.org/10.1007/978-3-319-08918-8_24
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08917-1
Online ISBN: 978-3-319-08918-8
eBook Packages: Computer ScienceComputer Science (R0)