Domain-free λμ-calculus
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 34 (2000) no. 6, pp. 433-466. 
@article{ITA_2000__34_6_433_0,
     author = {Fujita, Ken-Etsu},
     title = {Domain-free $\lambda \mu $-calculus},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {433--466},
     publisher = {EDP-Sciences},
     volume = {34},
     number = {6},
     year = {2000},
     mrnumber = {1844713},
     zbl = {0974.68032},
     language = {en},
     url = {http://www.numdam.org/item/ITA_2000__34_6_433_0/}
}
TY  - JOUR
AU  - Fujita, Ken-Etsu
TI  - Domain-free $\lambda \mu $-calculus
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2000
SP  - 433
EP  - 466
VL  - 34
IS  - 6
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_2000__34_6_433_0/
LA  - en
ID  - ITA_2000__34_6_433_0
ER  - 
%0 Journal Article
%A Fujita, Ken-Etsu
%T Domain-free $\lambda \mu $-calculus
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2000
%P 433-466
%V 34
%N 6
%I EDP-Sciences
%U http://www.numdam.org/item/ITA_2000__34_6_433_0/
%G en
%F ITA_2000__34_6_433_0
Fujita, Ken-Etsu. Domain-free $\lambda \mu $-calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 34 (2000) no. 6, pp. 433-466. http://www.numdam.org/item/ITA_2000__34_6_433_0/

[1] Y. Andou, A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols, Tsukuba J. Math. 19 (1995) 153-162. | MR | Zbl

[2] Y. Andou Church-Rosser property of a simple reduction for full first order classical natural deduction (submitted). | Zbl

[3] Y. Andou, Strong normalization of classical natural deduction, Logic Colloquium 2000. Bull. Symbolic Logic (to appear).

[4] F. Barbanera and S. Berardi, Extracting Constructive Context front Classical Logic via Control-like Reductions. Springer, Lecture Notes in Comput. Sci. 664 (1993) 45-59. | MR | Zbl

[5] H. P. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Revised edition. North-Holland (1984). | MR | Zbl

[6] H. P. Barendregt, Lambda Calculi with Types. Oxford University Press, Handbook of Logic in Comput. Sci. 2 (1992) 117-309. | MR

[7]G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems. Springer, Lecture Notes in Comput. Sci. 1234 (1997) 9-20. | MR | Zbl

[8] G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems, the revised version of [7].

[9] K. Baba, S. Hirokawa and K. Fujita, Parallel Reduction in Type-Free λμ-Calculus, in The 7th Asian Logic Conference (1999).

[10] K. Baba, S. Hirokawa and K. Fujita, Parallel Reduction in Type-Free λμ-Calculus. Elsevier, Amsterdam, Electron. Notes Theoret. Comput. Sci. 42 (2001) 52-66.

[11] L. Damas and R. Milner, Principal type-schemes for functional programs, in Proc. the 9th Annual ACM Symposium on Principles of Programming Languages (1982) 207-212.

[12] R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, in Proc. the 23rd Annual ACM Symposium of Principles of Programming Languages (1996).

[13] R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, Technical Report CMU-CS-99-153 (1999).

[14] M. Felleisen, D. P. Friedman, E. Kohlbecker and B. Duba, Reasoning with Continuations, in Proc. the Annual IEEE Symposium on Logic in Computer Science (1986) 131-141.

[15] P. C. Fischer, Turing Machines with Restricted Memory Acces. Inform. and Control 9 (1966) 364-379. | MR | Zbl

[16] K. Fujita, On embedding of Classical Substractural Logics, RIMS 918. Research Institute for Mathematical Sciences, Kyoto University (1995) 178-195. | Zbl

[17] K. Fujita, Calculus of Classical Proofs I. Springer, Lecture Notes in Comput. Sci. 1345 (1997) 321-335. | MR | Zbl

[18] K. Fujita, Polymorphic Call-by-Value Calculus based on Classical Proofs. Springer, Lecture Notes in Artificial Intelligence 1476 (1998) 170-182. | Zbl

[19] K. Fujita, Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value. Springer, Lecture Notes in Comput Sci. 1581 (1999) 162-176. | MR | Zbl

[20] K. Fujita, Type Inference for Domain-Free λ2 Technical Report in Computer Science and Systems Engineering CSSE-5. Kyushu Institute of Technology (1999).

[21] K. Fujita and A. Schubert, Partially Typed Terms between Church-Style and Curry-Style. Springer, Lecture Notes in Comput. Sci. 1872 (2000) 505-520. | Zbl

[22] T.G. Griffin, A Formulae-as-Types Notion of Control, in Proc. the 17th Annual ACM Symposium on Principles of Programming Languages (1990) 47-58.

[23] Ph. De Groote, A CPS-Translation for the λμ-Calculus. Springer, Lecture Notes in Comput. Sci. 787 (1994) 85-99. | MR | Zbl

[24] Ph. De Groote, A Simple Calculus of Exception Handling. Springer, Lecture Notes in Comput. Sci. 902 (1995) 201-215. | MR | Zbl

[25] R. Harper, B. F. Duba and D. Macqueen, Typing First-Class Continuations in ML. J. Funct. Programming 3 (1993) 465-484.

[26] R. Harper and M. Lillibridge, ML with calice is unsound. The Types Form, 8 July (1991).

[27] R. Harper and M. Lillibridge, Explicit polymorphism and CPS conversion, in Proc. the 20th Annual ACM Symposium on Principles of Programming Languages (1993) 206-219.

[28] R. Harper and M. Lillibridge, Polymorphic type assignment and CPS conversion. LISP and Symbolic Computation 6 (1993) 361-380.

[29] R. Harper and J. C. Mitchell On The Type Structure of Standard ML. ACM Trans. Programming Languages and Systems 15 (1993) 210-252.

[30] M. Hofmann, Sound and complete axiomatisations of call-by-value control operators. Math. Structures Comput. Sci. 5 (1995) 461-482. | MR | Zbl

[31] M. Hofmann and T. Streicher, Continuation models are universal for λμ-calculus, in Proc. the 12th Annual IEEE Symposium on Logic in Computer Science (1997) 387-395.

[32] J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979). | MR | Zbl

[33] W. Howard, The Formulae-as-Typ es Notion of Constructions, To H.B. Curry: Essays on combinatory logic, lambda-calculus, and formalism. Academic Press (1980) 479-490. | MR

[34] A. J. Kfoury, J. Tiuryn and P. Urzyczyn, An Analysis of ML Typability. J. Assoc. Comput. Mach. 41 (1994) 368-398. | Zbl

[35] S. Kobayashi, Monads as modality. Theoret. Comput. Sci. 175 (1997) 29-74. | MR | Zbl

[36] X. Leroy, Polymorphism by name for references and continuations, in Proc. the 20th Annual ACM Symposium of Principles of Programming Languages (1993) 220-231.

[37] S. Martini and A. Massini, A Computational Interprétation of Modal Proofs, Proof Theory of Modal Logic. Kluwer (1996) 213-241. | Zbl

[38] A. Meyer and M. Wand, Continuation Semantics in Typed Lambda-Calculi. Springer, Lecture Notes in Comput Set 193 (1985) 219-224. | MR | Zbl

[39] J. C. Mitchell, Polymorphic Type Inference and Containment. Inform. and Comput. 76 (1988) 211-249. | MR | Zbl

[40] R. Milner, A Theory of Type Polymorphism in Programming. J. Comput. System Sci. 17 (1978) 348-375. | MR | Zbl

[41] M. L. Minsky, Recursive Unsolvability of Post's Problem of "TAG" and Other Topics in Theory of Turing Machines. Ann. of Math. 74 (1961) 437-455. | MR | Zbl

[42] E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991) 55-92. | MR | Zbl

[43] C. R. Murthy, An Evaluation Semantics for Classical Proofs, in Proc. the 6th Annual IEEE Symposium on Logic in Computer Science (1991) 96-107.

[44] C.-H.L. Ong, A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations, Linear Logic '96 Tokyo Meeting (1996).

[45] C.-H.L. Ong and C.A. Stewart, A Curry-Howard Foundation for Functional Computation with Control, in Proc. the 24th Annual ACM Symposium of Principles of Programming Languages (1997).

[46] M. Parigot, λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. Springer, Lecture Notes in Comput. Sci. 624 (1992) 190-201. | MR | Zbl

[47] M. Parigot, Classical Proofs as Programs, Springer, Lecture Notes in Comput. Sci. 713 (1993) 263-276. | MR | Zbl

[48] M. Parigot, Proofs of Strong Normalization for Second Order Classical Natural Deduction. J. Symbolic Logic 62 (1997) 1461-1479. | MR | Zbl

[49] G. Plotkin, Call-by-Name, Call-by-Value and the λ-Calculus. Theoret. Comput. Sci. 1 (1975) 125-159. | MR | Zbl

[50] D. Prawitz, Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell (1965). | MR | Zbl

[51] D. Prawitz, Ideas and Results in Proof Theory, in Proc. the 2nd Scandinavian Logic Symposium, edited by N.E. Fenstad. North-Holland (1971) 235-307. | MR | Zbl

[52] N. J. Rehof and M. H. Sørensen, The λ∆-Calculus. Springer, Lecture Notes in Comput. Sci. 789 (1994) 516-542. | MR | Zbl

[53] A. Schubert, Second-order unification and type inference for Church-style, Tech. Report TR 97-02 (239). Institute of Informatics, Warsaw University (1997).

[54] A. Schubert, Second-order unification and type inference for Church-style, in Proc. the ACM Symposium on Principles of Programming Languages (1998) 279-288.

[55] T. Streicher and B. Reus, Continuation semantics: Abstract machines and control operators. J. Funct. Programming (to appear). | MR

[56] M. Takahashi, Parallel Reductions in λ-Calculus. J. Symbolic Comput. 7 (1989) 113-123. | MR | Zbl

[57] J. Tiuryn, Type Inference Problems: A Survey. Springer, Lecture Notes in Comput. Sci. 452 (1990) 105-120. | MR | Zbl

[58] J. B. Wells, Typability and Type Checking in the Second-Order λ-Calculus Are Equivalent and Undecidable, in Proc. IEEE Symposium on Logic in Computer Science (1994) 176-185.