Completeness of continuation models for λμ-calculus

Abstract

We show that a certain simple call-by-name continuation semantics of Parigot's λμ-calculus is complete. More precisely, for every λμ-theory we construct a cartesian closed category such that the ensuing continuation-style interpretation of λμ, which maps terms to functions sending abstract continuations to responses, is full and faithful. Thus, any λμ-category in the sense of L. Ong (1996, in "Proceedings of LICS '96," IEEE Press, New York) is isomorphic to a continuation model (Y. Lafont, B. Reus, and T. Streicher, "Continuous Semantics or Expressing Implication by Negation," Technical Report 93-21, University of Munich) derived from a cartesian-closed category of continuations. We also extend this result to a later call-by-value version of λμ developed by C.-H.L. Ong and C.A. Stewart (1997, in "Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, January 1997," Assoc. Comput. Much. Press, New York). © 2002 Elsevier Science (USA).