A completeness result for the simply typed λμ-calculus

T. Coquand, Completeness theorem and λ-calculus. The 7th International Conference, TLCA 2005, Nara, Japan, April 21–23, volume 3461/2005, 2005, pp. 1–9 Farkh, 1998, Un résultat de complétude pour les types ∀+ du système F, Comptes Rendus de l’Académie des Sciences, Mathematics, 326, 275 Farkh, 1998, Types Complets dans une extension du système AF2, Informatique Théorique et Application, 31, 513, 10.1051/ita/1997310605131 T. Griffin, A formulae-as-types notion of control, in: Proc. POLP, 1990 J.R. Hindley, The simple semantics for Coppe-Dezani-Sallé types, in: Proceeding of the 5th Colloquium on International Symposium on Programming, 1982, pp. 212–226 Hindley, 1983, The completeness theorem for typing λ-terms, Theoretical Computer Science, 22, 1, 10.1016/0304-3975(83)90136-6 Hindley, 1983, Curry’s type-rules are complete with respect to the F-semantics too, Theoretical Computer Science, 22, 127, 10.1016/0304-3975(83)90141-X Kamareddine, 2007, A completeness result for a realizability semantics for an intersection type system, Annals of Pure and Applied Logic, 146, 180, 10.1016/j.apal.2007.02.001 Krivine, 1990 Labib-Sami, 1986 Nour, 2005, A semantics of realizability for the classical propositional natural deduction, Electronic Notes in Theoretical Computer Science, 140, 31, 10.1016/j.entcs.2005.06.026 Nour, 2005, A semantical proof of strong normalization theorem for full propositional classical natural deduction, Archive for Mathematical Logic, 45, 357, 10.1007/s00153-005-0314-y Nour, 1996, Opérateurs de mise en mémoire et types ∀-positifs, Theoretical Informatics and Applications, 30, 261, 10.1051/ita/1996300302611 Nour, 2000, Mixed logic and storage operators, Archive for Mathematical Logic, 39, 261, 10.1007/s001530050147 Parigot, 1992, λμ-calculus: An algorithm interpretation of classical natural deduction, vol. 624, 190 Parigot, 1997, Proofs of strong normalization for second order classical natural deduction, Journal of Symbolic Logic, 62, 1461, 10.2307/2275652 W. Py, Confluence en λμ-calcul, Ph.D. Thesis, University of Chambéry, 1998 Saurin, 2005, Separation and the λμ-calculus, 356