Domain-free $\lambda \mu$-calculus

 Access to full text

 Full (PDF)

1. [1] Y. Andou, A Normalization-Procedure for the First Order Classical Natural Deduction with Full Logical Symbols, Tsukuba J. Math. 19 (1995) 153-162. Zbl0835.03021MR1346758
2. [2] Y. AndouChurch-Rosser property of a simple reduction for full first order classical natural deduction (submitted). Zbl1016.03006
3. [3] Y. Andou, Strong normalization of classical natural deduction, Logic Colloquium 2000. Bull. Symbolic Logic (to appear). 
4. [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. Zbl0788.68016MR1233139
5. [5] H. P. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Revised edition. North-Holland (1984). Zbl0551.03007MR774952
6. [6] H. P. Barendregt, Lambda Calculi with Types. Oxford University Press, Handbook of Logic in Comput. Sci. 2 (1992) 117-309. MR1381697
7. [7] G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems. Springer, Lecture Notes in Comput. Sci. 1234 (1997) 9-20. Zbl0887.03010MR1611405
8. [8] G. Barthe and M.H. Sørensen, Domain-Free Pure Type Systems, the revised version of [7]. Zbl0979.03013
9. [9] K. Baba, S. Hirokawa and K. Fujita, Parallel Reduction in Type-Free λμ-Calculus, in The 7th Asian Logic Conference (1999). 
10. [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. [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. [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). Zbl1323.68107
13. [13] R. Davies and F. Pfenning, A Modal Analysis of Staged Computation, Technical Report CMU-CS-99-153 (1999). Zbl1323.68107
14. [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. [15] P. C. Fischer, Turing Machines with Restricted Memory Acces. Inform. and Control 9 (1966) 364-379. Zbl0145.24205MR199061
16. [16] K. Fujita, On embedding of Classical Substractural Logics, RIMS 918. Research Institute for Mathematical Sciences, Kyoto University (1995) 178-195. Zbl0938.03536
17. [17] K. Fujita, Calculus of Classical Proofs I. Springer, Lecture Notes in Comput. Sci. 1345 (1997) 321-335. Zbl0890.03028MR1638567
18. [18] K. Fujita, Polymorphic Call-by-Value Calculus based on Classical Proofs. Springer, Lecture Notes in Artificial Intelligence 1476 (1998) 170-182. Zbl0914.03036
19. [19] K. Fujita, Explicitly Typed λμ-Calculus for Polymorphism and Call-by-Value. Springer, Lecture Notes in Comput Sci. 1581 (1999) 162-176. Zbl0933.03009MR1723964
20. [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. [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. Zbl0998.03009
22. [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. [23] Ph. de Groote, A CPS-Translation for the λμ-Calculus. Springer, Lecture Notes in Comput. Sci. 787 (1994) 85-99. Zbl0938.03024MR1286753
24. [24] Ph. de Groote, A Simple Calculus of Exception Handling. Springer, Lecture Notes in Comput. Sci. 902 (1995) 201-215. Zbl1063.68565MR1477984
25. [25] R. Harper, B. F. Duba and D. MacQueen, Typing First-Class Continuations in ML. J. Funct. Programming 3 (1993) 465-484. 
26. [26] R. Harper and M. Lillibridge, ML with calice is unsound. The Types Form, 8 July (1991). 
27. [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. [28] R. Harper and M. Lillibridge, Polymorphic type assignment and CPS conversion. LISP and Symbolic Computation 6 (1993) 361-380. Zbl1058.68727
29. [29] R. Harper and J. C. MitchellOn The Type Structure of Standard ML. ACM Trans. Programming Languages and Systems 15 (1993) 210-252. 
30. [30] M. Hofmann, Sound and complete axiomatisations of call-by-value control operators. Math. Structures Comput. Sci. 5 (1995) 461-482. Zbl0846.68066MR1377313
31. [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. [32] J. E. Hopcroft and J. D. Ullman, Introduction to Automata Theory, Languages and Computation. Addison-Wesley (1979). Zbl0426.68001MR645539
33. [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. MR592792
34. [34] A. J. Kfoury, J. Tiuryn and P. Urzyczyn, An Analysis of ML Typability. J. Assoc. Comput. Mach. 41 (1994) 368-398. Zbl0806.68016
35. [35] S. Kobayashi, Monads as modality. Theoret. Comput. Sci. 175 (1997) 29-74. Zbl0895.03011MR1449431
36. [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. [37] S. Martini and A. Massini, A Computational Interprétation of Modal Proofs, Proof Theory of Modal Logic. Kluwer (1996) 213-241. Zbl0867.03016
38. [38] A. Meyer and M. Wand, Continuation Semantics in Typed Lambda-Calculi. Springer, Lecture Notes in Comput Set 193 (1985) 219-224. Zbl0565.68028MR808800
39. [39] J. C. Mitchell, Polymorphic Type Inference and Containment. Inform. and Comput. 76 (1988) 211-249. Zbl0656.68023MR935896
40. [40] R. Milner, A Theory of Type Polymorphism in Programming. J. Comput. System Sci. 17 (1978) 348-375. Zbl0388.68003MR516844
41. [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. Zbl0105.00802MR140405
42. [42] E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991) 55-92. Zbl0723.68073MR1115262
43. [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. [44] C.-H.L. Ong, A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations, Linear Logic '96 Tokyo Meeting (1996). 
45. [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. [46] M. Parigot, λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. Springer, Lecture Notes in Comput. Sci. 624 (1992) 190-201. Zbl0925.03092MR1235373
47. [47] M. Parigot, Classical Proofs as Programs, Springer, Lecture Notes in Comput. Sci. 713 (1993) 263-276. Zbl0805.03012MR1254686
48. [48] M. Parigot, Proofs of Strong Normalization for Second Order Classical Natural Deduction. J. Symbolic Logic 62 (1997) 1461-1479. Zbl0941.03063MR1617992
49. [49] G. Plotkin, Call-by-Name, Call-by-Value and the λ-Calculus. Theoret. Comput. Sci. 1 (1975) 125-159. Zbl0325.68006MR429501
50. [50] D. Prawitz, Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell (1965). Zbl0173.00205MR193005
51. [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. Zbl0226.02031MR387024
52. [52] N. J. Rehof and M. H. Sørensen, The λ∆-Calculus. Springer, Lecture Notes in Comput. Sci. 789 (1994) 516-542. Zbl0942.03512MR1296690
53. [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. [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. [55] T. Streicher and B. Reus, Continuation semantics: Abstract machines and control operators. J. Funct. Programming (to appear). Zbl0928.68074MR1678817
56. [56] M. Takahashi, Parallel Reductions in λ-Calculus. J. Symbolic Comput. 7 (1989) 113-123. Zbl0661.03008MR989050
57. [57] J. Tiuryn, Type Inference Problems: A Survey. Springer, Lecture Notes in Comput. Sci. 452 (1990) 105-120. Zbl0745.03013MR1084827
58. [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.