Domain-free λμ-calculus
Fujita, Ken-Etsu
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 34 (2000), p. 433-466 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU)
Publié le : 2000-01-01
@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},
     volume = {34},
     year = {2000},
     pages = {433-466},
     mrnumber = {1844713},
     zbl = {0974.68032},
     language = {en},
     url = {http://dml.mathdoc.fr/item/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) pp. 433-466. http://gdmltest.u-ga.fr/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 1346758 | Zbl 0835.03021

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

[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 1233139 | Zbl 0788.68016

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

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

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

[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 199061 | Zbl 0145.24205

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

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

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

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

[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 0998.03009

[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 1286753 | Zbl 0938.03024

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

[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 1377313 | Zbl 0846.68066

[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 645539 | Zbl 0426.68001

[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 592792

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

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

[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 0867.03016

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

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

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

[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 140405 | Zbl 0105.00802

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

[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 1235373 | Zbl 0925.03092

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

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

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

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

[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 387024 | Zbl 0226.02031

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

[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 1678817

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

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

[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.