Goldberg, Mayer Gödelization in the lambda calculus. (English) Zbl 1339.03016 Inf. Process. Lett. 75, No. 1-2, 13-16 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{M. Goldberg}, Inf. Process. Lett. 75, No. 1--2, 13--16 (2000; Zbl 1339.03016) Full Text: DOI Link
Curien, Pierre-Louis; Herbelin, Hugo The duality of computation. (English) Zbl 1321.68146 Proceedings of the 5th ACM SIGPLAN international conference on functional programming, ICFP ’00, Montréal, Canada, September 18–21, 2000. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-202-6). ACM SIGPLAN Notices 35, No. 9, 233-243 (2000). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{P.-L. Curien} and \textit{H. Herbelin}, in: Proceedings of the 5th ACM SIGPLAN international conference on functional programming, ICFP '00, Montréal, Canada, September 18--21, 2000. New York, NY: Association for Computing Machinery (ACM). 233--243 (2000; Zbl 1321.68146) Full Text: DOI
Ogata, Ichiro Constructive classical logic as CPS-calculus. (English) Zbl 1320.03063 Int. J. Found. Comput. Sci. 11, No. 1, 89-112 (2000). MSC: 03B70 03B40 03F05 03F50 68N18 PDFBibTeX XMLCite \textit{I. Ogata}, Int. J. Found. Comput. Sci. 11, No. 1, 89--112 (2000; Zbl 1320.03063) Full Text: DOI
Asperti, Andrea; Coppola, Paolo; Martini, Simone (Optimal) duplication is not elementary recursive. (English) Zbl 1323.68091 Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’00, Boston, MA, USA, January 19–21, 2000. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-58113-125-9). 96-107 (2000). MSC: 68N18 03B40 03F52 PDFBibTeX XMLCite \textit{A. Asperti} et al., in: Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '00, Boston, MA, USA, January 19--21, 2000. New York, NY: Association for Computing Machinery (ACM). 96--107 (2000; Zbl 1323.68091) Full Text: DOI
Parigot, Michel Strong normalization of second order symmetric \(\lambda\)-calculus. (English) Zbl 1044.03008 Kapoor, Sanjiv (ed.) et al., FST TCS 2000: Foundations of software technology and theoretical computer science. 20th conference, New Delhi, India, December 13–15, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41413-4). Lect. Notes Comput. Sci. 1974, 442-453 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{M. Parigot}, Lect. Notes Comput. Sci. 1974, 442--453 (2000; Zbl 1044.03008) Full Text: Link
Di Gianantonio, Pietro; Franco, Gianluca The fine structure of game lambda models. (English) Zbl 1044.03007 Kapoor, Sanjiv (ed.) et al., FST TCS 2000: Foundations of software technology and theoretical computer science. 20th conference, New Delhi, India, December 13–15, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41413-4). Lect. Notes Comput. Sci. 1974, 429-441 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{P. Di Gianantonio} and \textit{G. Franco}, Lect. Notes Comput. Sci. 1974, 429--441 (2000; Zbl 1044.03007) Full Text: Link
Kuzichev, A. S. Solution of the Hilbert central problem following Kolmogorov. (English. Russian original) Zbl 1041.03507 Dokl. Math. 61, No. 2, 212-215 (2000); translation from Dokl. Akad. Nauk, Ross. Akad. Nauk 371, No. 3, 303-306 (2000). MSC: 03B40 03B30 PDFBibTeX XMLCite \textit{A. S. Kuzichev}, Dokl. Math. 61, No. 2, 303--306 (2000; Zbl 1041.03507); translation from Dokl. Akad. Nauk, Ross. Akad. Nauk 371, No. 3, 303--306 (2000)
Baba, Kensuke; Kameyama, Yukiyoshi; Hirokawa, Sachio Combinatory logic and \(\lambda\)-calculus for classical logic. (English) Zbl 1034.03011 Bull. Inf. Cybern. 32, No. 2, 105-121 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{K. Baba} et al., Bull. Inf. Cybern. 32, No. 2, 105--121 (2000; Zbl 1034.03011)
Ghani, Neil; de Paiva, Valéria; Ritter, Eike Linear explicit substitutions. (English) Zbl 1033.03007 Log. J. IGPL 8, No. 1, 7-31 (2000). MSC: 03B40 68N18 03F52 PDFBibTeX XMLCite \textit{N. Ghani} et al., Log. J. IGPL 8, No. 1, 7--31 (2000; Zbl 1033.03007) Full Text: DOI
Zajtsev, D. V. Combinators and implicative formulas. (Russian) Zbl 1009.03510 Karpenko, A. S. (ed.), Proceedings of the scientific research seminar of the Logic Center of the Institute of Philosophy RAS. 1999-2000. No.XIV. Moskva: Rossijskaya Akademiya Nauk, Institut Filosofii. Tr. Nauchno-Issled. Semin. Log. Tsentra Inst. Filos. RAN. 14, 42-53 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{D. V. Zajtsev}, in: Trudy nauchno-issledovatel'skogo seminara Logicheskogo Tsentra Instituta Filosofii RAN. 14. 1999--2000. Vyp. XIV. Moskva: Rossijskaya Akademiya Nauk, Institut Filosofii. 42--53 (2000; Zbl 1009.03510)
Abramsky, Samson; Jagadeesan, Radha; Malacaria, Pasquale Full abstraction for PCF. (English) Zbl 1006.68028 Inf. Comput. 163, No. 2, 409-470 (2000). MSC: 68N18 03B40 03D20 18C50 18D20 68Q05 68Q55 03B70 91A80 PDFBibTeX XMLCite \textit{S. Abramsky} et al., Inf. Comput. 163, No. 2, 409--470 (2000; Zbl 1006.68028) Full Text: DOI Link
Hyland, J. M. E.; Ong, C.-H. L. On full abstraction for PCF: I, II and III. (English) Zbl 1006.68027 Inf. Comput. 163, No. 2, 285-408 (2000). MSC: 68N18 03B40 03D20 18D20 68Q05 68Q55 03B70 91A80 PDFBibTeX XMLCite \textit{J. M. E. Hyland} and \textit{C. H. L. Ong}, Inf. Comput. 163, No. 2, 285--408 (2000; Zbl 1006.68027) Full Text: DOI
Bethke, Inge; Klop, Jan Willem; de Vrijer, Roel Descendants and origins in term rewriting. (English) Zbl 1046.68564 Inf. Comput. 159, No. 1-2, 59-124 (2000). MSC: 68Q42 03B40 PDFBibTeX XMLCite \textit{I. Bethke} et al., Inf. Comput. 159, No. 1--2, 59--124 (2000; Zbl 1046.68564) Full Text: DOI Link
Waldmann, Johannes The combinator S. (English) Zbl 1005.03017 Inf. Comput. 159, No. 1-2, 2-21 (2000). MSC: 03B40 68Q42 PDFBibTeX XMLCite \textit{J. Waldmann}, Inf. Comput. 159, No. 1--2, 2--21 (2000; Zbl 1005.03017) Full Text: DOI
Dowek, Gilles; Hardin, Thérèse; Kirchner, Claude Higher order unification via explicit substitutions. (English) Zbl 1005.03016 Inf. Comput. 157, No. 1-2, 183-235 (2000). MSC: 03B40 03B15 03B35 68Q42 PDFBibTeX XMLCite \textit{G. Dowek} et al., Inf. Comput. 157, No. 1--2, 183--235 (2000; Zbl 1005.03016) Full Text: DOI Link
Dougherty, Daniel J.; Subrahmanyam, Ramesh Equality between functionals in the presence of coproducts. (English) Zbl 1005.03015 Inf. Comput. 157, No. 1-2, 52-83 (2000). MSC: 03B40 03B70 68N18 PDFBibTeX XMLCite \textit{D. J. Dougherty} and \textit{R. Subrahmanyam}, Inf. Comput. 157, No. 1--2, 52--83 (2000; Zbl 1005.03015) Full Text: DOI Link
Fujita, Ken-Etsu; Schubert, Aleksy Partially typed terms between Church-style and Curry-style. (English) Zbl 0998.03009 van Leeuwen, Jan (ed.) et al., Theoretical computer science. Exploring new frontiers of theoretical informatics. International conference IFIP TCS 2000, Sendai, Japan, August 17-19, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1872, 505-520 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{K.-E. Fujita} and \textit{A. Schubert}, Lect. Notes Comput. Sci. 1872, 505--520 (2000; Zbl 0998.03009)
Dezani-Ciancaglini, M.; Honsell, F.; Motohama, Y. Compositional characterizations of \(\lambda\)-terms using intersection types (extended abstract). (English) Zbl 0996.03501 Nielsen, Mogens (ed.) et al., Mathematical foundations of computer science 2000. 25th international symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1893, 304-313 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{M. Dezani-Ciancaglini} et al., Lect. Notes Comput. Sci. 1893, 304--313 (2000; Zbl 0996.03501)
Abramsky, Samson; Lenisa, Marina Axiomatizing fully complete models for ML polymorphic types. (English) Zbl 0996.03041 Nielsen, Mogens (ed.) et al., Mathematical foundations of computer science 2000. 25th international symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1893, 141-151 (2000). MSC: 03G30 03F52 03B40 03B70 PDFBibTeX XMLCite \textit{S. Abramsky} and \textit{M. Lenisa}, Lect. Notes Comput. Sci. 1893, 141--151 (2000; Zbl 0996.03041)
Statman, Rick Church’s lambda delta calculus. (English) Zbl 0988.03027 Parigot, Michel (ed.) et al., Logic for programming and automated reasoning. 7th international conference, LPAR 2000, Reunion Island, France, November 6-10, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1955, 293-307 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{R. Statman}, Lect. Notes Comput. Sci. 1955, 293--307 (2000; Zbl 0988.03027)
Spreen, Dieter A new model construction for the polymorphic lambda calculus. (English) Zbl 0988.03026 Parigot, Michel (ed.) et al., Logic for programming and automated reasoning. 7th international conference, LPAR 2000, Reunion Island, France, November 6-10, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1955, 275-292 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{D. Spreen}, Lect. Notes Comput. Sci. 1955, 275--292 (2000; Zbl 0988.03026)
Qiao, Haiyan Formalising formulas-as-types-as-objects. (English) Zbl 0988.03028 Coquand, Thierry (ed.) et al., Types for proofs and programs. 3rd international workshop, TYPES ’99, Lökeberg, Sweden, June 12-16, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1956, 174-193 (2000). MSC: 03B40 03G30 03F07 18D15 03B70 03F35 68T15 PDFBibTeX XMLCite \textit{H. Qiao}, Lect. Notes Comput. Sci. 1956, 174--193 (2000; Zbl 0988.03028)
Delahaye, David Information retrieval in a Coq proof library using type isomorphisms. (English) Zbl 0988.68542 Coquand, Thierry (ed.) et al., Types for proofs and programs. 3rd international workshop, TYPES ’99, Lökeberg, Sweden, June 12-16, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1956, 131-147 (2000). MSC: 68N30 68P20 03B40 PDFBibTeX XMLCite \textit{D. Delahaye}, Lect. Notes Comput. Sci. 1956, 131--147 (2000; Zbl 0988.68542)
van Bakel, Steffen; Barbanera, Franco; Fernández, Maribel Polymorphic intersection type assignment for rewrite systems with abstraction and \(\beta\)-rule. (English) Zbl 0988.68092 Coquand, Thierry (ed.) et al., Types for proofs and programs. 3rd international workshop, TYPES ’99, Lökeberg, Sweden, June 12-16, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1956, 41-60 (2000). MSC: 68Q42 03B40 PDFBibTeX XMLCite \textit{S. van Bakel} et al., Lect. Notes Comput. Sci. 1956, 41--60 (2000; Zbl 0988.68092)
Abel, Andreas; Altenkirch, Thorsten A predicative strong normalisation proof for a \(\lambda\)-calculus with interleaving inductive types. (English) Zbl 0988.03029 Coquand, Thierry (ed.) et al., Types for proofs and programs. 3rd international workshop, TYPES ’99, Lökeberg, Sweden, June 12-16, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1956, 21-40 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{A. Abel} and \textit{T. Altenkirch}, Lect. Notes Comput. Sci. 1956, 21--40 (2000; Zbl 0988.03029)
Espírito Santo, José Revisiting the correspondence between cut elimination and normalisation. (English) Zbl 0973.03073 Montanari, Ugo (ed.) et al., Automata, languages and programming. 27th international colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1853, 600-611 (2000). MSC: 03F05 03B40 03B20 PDFBibTeX XMLCite \textit{J. Espírito Santo}, Lect. Notes Comput. Sci. 1853, 600--611 (2000; Zbl 0973.03073)
Plotkin, Gordon; Power, John; Sannella, Donald; Tennent, Robert Lax logical relations. (English) Zbl 0973.03016 Montanari, Ugo (ed.) et al., Automata, languages and programming. 27th international colloquium, ICALP 2000, Geneva, Switzerland, July 9-15, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1853, 85-102 (2000). MSC: 03B40 03G30 68N18 03B70 PDFBibTeX XMLCite \textit{G. Plotkin} et al., Lect. Notes Comput. Sci. 1853, 85--102 (2000; Zbl 0973.03016)
Ramsay, Allan Theorem proving for constructive \(\lambda\)-calculus. (English) Zbl 0973.68211 Cerri, Stefano A. (ed.) et al., Artificial intelligence: methodology, systems, and applications. 9th international conference, AIMSA 2000, Varna, Bulgaria, September 20-23, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1904, 69-79 (2000). MSC: 68T15 03B40 PDFBibTeX XMLCite \textit{A. Ramsay}, Lect. Notes Comput. Sci. 1904, 69--79 (2000; Zbl 0973.68211)
Parigot, Michel On the computational interpretation of negation. (English) Zbl 0973.03017 Clote, Peter G. (ed.) et al., Computer science logic. 14th international workshop, CSL 2000. Annual conference of the EACSL, Fischbachau, Germany, August 21-26, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1862, 472-484 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{M. Parigot}, Lect. Notes Comput. Sci. 1862, 472--484 (2000; Zbl 0973.03017)
Danos, Vincent; Krivine, Jean-Louis Disjunctive tautologies as synchronisation schemes. (English) Zbl 0973.03039 Clote, Peter G. (ed.) et al., Computer science logic. 14th international workshop, CSL 2000. Annual conference of the EACSL, Fischbachau, Germany, August 21-26, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1862, 292-301 (2000). MSC: 03B70 68Q60 03B15 03B40 PDFBibTeX XMLCite \textit{V. Danos} and \textit{J.-L. Krivine}, Lect. Notes Comput. Sci. 1862, 292--301 (2000; Zbl 0973.03039)
Aspinall, David Subtyping with power types. (English) Zbl 0973.03018 Clote, Peter G. (ed.) et al., Computer science logic. 14th international workshop, CSL 2000. Annual conference of the EACSL, Fischbachau, Germany, August 21-26, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1862, 156-171 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{D. Aspinall}, Lect. Notes Comput. Sci. 1862, 156--171 (2000; Zbl 0973.03018)
Abramsky, Samson; Lenisa, Marina A fully complete PER model for ML polymorphic types. (English) Zbl 0973.03015 Clote, Peter G. (ed.) et al., Computer science logic. 14th international workshop, CSL 2000. Annual conference of the EACSL, Fischbachau, Germany, August 21-26, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1862, 140-155 (2000). MSC: 03B40 03G30 03F52 PDFBibTeX XMLCite \textit{S. Abramsky} and \textit{M. Lenisa}, Lect. Notes Comput. Sci. 1862, 140--155 (2000; Zbl 0973.03015)
Fujita, Ken-etsu Multiple-conclusion system as communication calculus—informal meaning of proofs as communication terms. (English) Zbl 0969.03516 RIMS Kokyuroku 1166, 67-75 (2000). MSC: 03F07 03B40 68N18 68Q85 PDFBibTeX XMLCite \textit{K.-e. Fujita}, RIMS Kokyuroku 1166, 67--75 (2000; Zbl 0969.03516)
Fujita, Ken-Etsu Domain-free \(\lambda\mu\)-calculus. (English) Zbl 0974.68032 Theor. Inform. Appl. 34, No. 6, 433-466 (2000). MSC: 68N18 68Q05 03B40 PDFBibTeX XMLCite \textit{K.-E. Fujita}, Theor. Inform. Appl. 34, No. 6, 433--466 (2000; Zbl 0974.68032) Full Text: DOI EuDML
Došen, Kosta; Petrić, Zoran The maximality of the typed lambda calculus and of cartesian closed categories. (English) Zbl 0968.03019 Publ. Inst. Math., Nouv. Sér. 68(82), 1-19 (2000). Reviewer: Branislav Boričić (Novi Beograd) MSC: 03B40 18A15 03G30 18D15 PDFBibTeX XMLCite \textit{K. Došen} and \textit{Z. Petrić}, Publ. Inst. Math., Nouv. Sér. 68(82), 1--19 (2000; Zbl 0968.03019) Full Text: arXiv EuDML
Statman, Rick On the word problem for combinators. (English) Zbl 0964.03013 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 203-213 (2000). MSC: 03B40 03D40 PDFBibTeX XMLCite \textit{R. Statman}, Lect. Notes Comput. Sci. 1833, 203--213 (2000; Zbl 0964.03013)
Joachimski, Felix; Matthes, Ralph Standardization and confluence for a lambda calculus with generalized applications. (English) Zbl 0964.03014 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 141-155 (2000). MSC: 03B40 68Q42 PDFBibTeX XMLCite \textit{F. Joachimski} and \textit{R. Matthes}, Lect. Notes Comput. Sci. 1833, 141--155 (2000; Zbl 0964.03014)
de Groote, Philippe Linear higher-order matching is NP-complete. (English) Zbl 0964.68067 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 127-140 (2000). MSC: 68Q42 68Q25 03B40 PDFBibTeX XMLCite \textit{P. de Groote}, Lect. Notes Comput. Sci. 1833, 127--140 (2000; Zbl 0964.68067)
Bonelli, Eduardo; Kesner, Delia; Ríos, Alejandro A de Bruijn notation for higher-order rewriting. (Extended abstract). (English) Zbl 0964.68520 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 62-79 (2000). MSC: 68Q42 03B40 PDFBibTeX XMLCite \textit{E. Bonelli} et al., Lect. Notes Comput. Sci. 1833, 62--79 (2000; Zbl 0964.68520)
Blanqui, Frédéric Termination and confluence of higher-order rewrite systems. (English) Zbl 0964.68070 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 47-61 (2000). MSC: 68Q42 03B40 PDFBibTeX XMLCite \textit{F. Blanqui}, Lect. Notes Comput. Sci. 1833, 47--61 (2000; Zbl 0964.68070)
Bjørner, Nikolaj; Muñoz, César Absolute explicit unification. (English) Zbl 0964.03009 Bachmair, Leo (ed.), Rewriting techniques and applications. 11th international conference, RTA 2000, Norwich, GB, July 10-12, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1833, 31-46 (2000). MSC: 03B35 03B40 68Q42 PDFBibTeX XMLCite \textit{N. Bjørner} and \textit{C. Muñoz}, Lect. Notes Comput. Sci. 1833, 31--46 (2000; Zbl 0964.03009)
Goldberg, Mayer An adequate and efficient left-associated binary numeral system in the \(\lambda\)-calculus. (English) Zbl 0974.03017 J. Funct. Program. 10, No. 6, 607-623 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{M. Goldberg}, J. Funct. Program. 10, No. 6, 607--623 (2000; Zbl 0974.03017) Full Text: DOI
Bunder, M. W. Expedited Broda-Damas bracket abstraction. (English) Zbl 0977.03013 J. Symb. Log. 65, No. 4, 1850-1857 (2000). Reviewer: Pavel Materna (Praha) MSC: 03B40 PDFBibTeX XMLCite \textit{M. W. Bunder}, J. Symb. Log. 65, No. 4, 1850--1857 (2000; Zbl 0977.03013) Full Text: DOI Link
Hirokawa, Sachio; Komori, Yuichi; Nagayama, Misao A lambda proof of the P-W theorem. (English) Zbl 0970.03019 J. Symb. Log. 65, No. 4, 1841-1849 (2000). MSC: 03B20 03B40 PDFBibTeX XMLCite \textit{S. Hirokawa} et al., J. Symb. Log. 65, No. 4, 1841--1849 (2000; Zbl 0970.03019) Full Text: DOI
Barthe, Gilles; Sørensen, Morten Heine Domain-free pure type systems. (English) Zbl 0979.03013 J. Funct. Program. 10, No. 5, 417-452 (2000). Reviewer: Paula G.Severi (Montevideo) MSC: 03B40 03B15 68N18 03B70 PDFBibTeX XMLCite \textit{G. Barthe} and \textit{M. H. Sørensen}, J. Funct. Program. 10, No. 5, 417--452 (2000; Zbl 0979.03013) Full Text: DOI
Bimbó, Katalin Investigation into combinatory systems with dual combinators. (English) Zbl 0963.03021 Stud. Log. 66, No. 2, 285-296 (2000). MSC: 03B40 03B47 PDFBibTeX XMLCite \textit{K. Bimbó}, Stud. Log. 66, No. 2, 285--296 (2000; Zbl 0963.03021) Full Text: DOI
Spreen, Dieter On domains witnessing increase in information. (English) Zbl 0968.68091 Appl. Gen. Topol. 1, No. 1, 129-152 (2000). MSC: 68Q55 06B35 03B15 03B40 18B30 54B30 PDFBibTeX XMLCite \textit{D. Spreen}, Appl. Gen. Topol. 1, No. 1, 129--152 (2000; Zbl 0968.68091)
Seldin, Jonathan P. On the role of implication in formal logic. (English) Zbl 0976.03015 J. Symb. Log. 65, No. 3, 1076-1114 (2000); erratum ibid. 66, No. 4, 1975 (2001). Reviewer: M.W.Bunder (Wollongong) MSC: 03B40 03F05 03B47 03B10 PDFBibTeX XMLCite \textit{J. P. Seldin}, J. Symb. Log. 65, No. 3, 1076--1114 (2000; Zbl 0976.03015) Full Text: DOI
Intrigila, B.; Biasone, E. On the number of fixed points of a combinator in lambda calculus. (English) Zbl 0968.03018 Math. Struct. Comput. Sci. 10, No. 5, 595-615 (2000). Reviewer: Rainer Kerth (Carmel) MSC: 03B40 PDFBibTeX XMLCite \textit{B. Intrigila} and \textit{E. Biasone}, Math. Struct. Comput. Sci. 10, No. 5, 595--615 (2000; Zbl 0968.03018) Full Text: DOI
Moczurad, M.; Tyszkiewicz, J.; Zaionc, M. Statistical properties of simple types. (English) Zbl 0966.03016 Math. Struct. Comput. Sci. 10, No. 5, 575-594 (2000). Reviewer: Paula G.Severi (Montevideo) MSC: 03B40 PDFBibTeX XMLCite \textit{M. Moczurad} et al., Math. Struct. Comput. Sci. 10, No. 5, 575--594 (2000; Zbl 0966.03016) Full Text: DOI
Beckmann, Arnold; Weiermann, Andreas Characterizing the elementary recursive functions by a fragment of Gödel’s \(T\). (English) Zbl 0965.03070 Arch. Math. Logic 39, No. 7, 475-491 (2000). Reviewer: G.Mints (Stanford) MSC: 03F05 03D20 03B40 03D10 PDFBibTeX XMLCite \textit{A. Beckmann} and \textit{A. Weiermann}, Arch. Math. Logic 39, No. 7, 475--491 (2000; Zbl 0965.03070) Full Text: DOI
Mazzucchelli, Luigi; Pasquali-Coluzzi, Dario \(\lambda\)-graphs structures and optimal implementations. (English) Zbl 0968.68027 Mitt. Math. Semin. Gießen 243, 19-50 (2000). Reviewer: Paula G.Severi (Montevideo) MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{L. Mazzucchelli} and \textit{D. Pasquali-Coluzzi}, Mitt. Math. Semin. Gießen 243, 19--50 (2000; Zbl 0968.68027)
Kamareddine, Fairouz Postponement, conservation and preservation of strong normalization for generalized reduction. (English) Zbl 0969.03022 J. Log. Comput. 10, No. 5, 721-738 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{F. Kamareddine}, J. Log. Comput. 10, No. 5, 721--738 (2000; Zbl 0969.03022) Full Text: DOI Link
Ivanov, Lyubomir Boldface recursion on Platek spaces. (English) Zbl 0969.03053 Fundam. Inform. 44, No. 1-2, 183-208 (2000). MSC: 03D75 03B40 PDFBibTeX XMLCite \textit{L. Ivanov}, Fundam. Inform. 44, No. 1--2, 183--208 (2000; Zbl 0969.03053)
Intrigila, Benedetto; Laurenzi, Anna R. Two problems on reduction graphs in lambda calculus. (English) Zbl 0963.03022 Fundam. Inform. 44, No. 1-2, 133-144 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{B. Intrigila} and \textit{A. R. Laurenzi}, Fundam. Inform. 44, No. 1--2, 133--144 (2000; Zbl 0963.03022)
Joly, Thierry Non finitely generated types and \(\lambda\)-terms combinatoric representation cost. (English. Abridged French version) Zbl 0962.03009 C. R. Acad. Sci., Paris, Sér. I, Math. 331, No. 8, 581-186 (2000). MSC: 03B40 PDFBibTeX XMLCite \textit{T. Joly}, C. R. Acad. Sci., Paris, Sér. I, Math. 331, No. 8, 581--186 (2000; Zbl 0962.03009) Full Text: DOI
Carboni, A.; Rosolini, G. Locally cartesian closed exact completions. (English) Zbl 0962.18001 J. Pure Appl. Algebra 154, No. 1-3, 103-116 (2000). Reviewer: Jiri Rosický (Brno) MSC: 18A35 03B40 18B30 03B15 PDFBibTeX XMLCite \textit{A. Carboni} and \textit{G. Rosolini}, J. Pure Appl. Algebra 154, No. 1--3, 103--116 (2000; Zbl 0962.18001) Full Text: DOI
Plotkin, Gordon (ed.); Stirling, Colin (ed.); Tofte, Mads (ed.) Proof, language, and interaction. Essays in honour of Robin Milner. (English) Zbl 0968.68018 MIT Press Series in the Foundations of Computing. Cambridge, MA: MIT Press. xiv, 722 p. $ 70.00; £48.95/hbk (2000). MSC: 68N15 00B30 68-06 03B40 68N18 68Q55 68Q85 68T15 PDFBibTeX XMLCite \textit{G. Plotkin} (ed.) et al., Proof, language, and interaction. Essays in honour of Robin Milner. Cambridge, MA: MIT Press (2000; Zbl 0968.68018)
Cantini, Andrea Feasible operations and applicative theories based on \(\lambda\eta\). (English) Zbl 0968.03067 Math. Log. Q. 46, No. 3, 291-311 (2000). Reviewer: Thomas Strahm (Bern) MSC: 03F30 03B40 03D15 PDFBibTeX XMLCite \textit{A. Cantini}, Math. Log. Q. 46, No. 3, 291--311 (2000; Zbl 0968.03067) Full Text: DOI
Mogensen, Torben Æ. Linear time self-interpretation of the pure lambda calculus. (English) Zbl 0956.03010 Bjørner, Dines (ed.) et al., Perspectives of system informatics. 3rd international Andrei Ershov memorial conference, PSI ’99. Akademgorodik, Novosibirsk, Russia, July 6-9, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1755, 128-142 (2000). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{T. Æ. Mogensen}, Lect. Notes Comput. Sci. 1755, 128--142 (2000; Zbl 0956.03010)
Scott, P. J. Some aspects of categories in computer science. (English) Zbl 0967.18003 Hazewinkel, M. (ed.), Handbook of algebra. Volume 2. Amsterdam: North-Holland. 3-77 (2000). Reviewer: A.Maggiolo-Schettini (Pisa) MSC: 18D15 68Q05 18-00 19-00 03B40 68Q55 03B70 18C50 PDFBibTeX XMLCite \textit{P. J. Scott}, in: Handbook of algebra. Volume 2. Amsterdam: North-Holland. 3--77 (2000; Zbl 0967.18003)
Broda, S.; Damas, L. On principal types of combinators. (English) Zbl 0949.68045 Theor. Comput. Sci. 247, No. 1-2, 277-290 (2000). MSC: 68N18 PDFBibTeX XMLCite \textit{S. Broda} and \textit{L. Damas}, Theor. Comput. Sci. 247, No. 1--2, 277--290 (2000; Zbl 0949.68045) Full Text: DOI
Schubert, Aleksy Type inference for first-order logic. (English) Zbl 0961.68032 Tiuryn, Jerzy (ed.), Foundations of software science and computation structures. 3rd international conference, FOSSACS 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1784, 297-313 (2000). MSC: 68N30 03B40 03B25 03B10 PDFBibTeX XMLCite \textit{A. Schubert}, Lect. Notes Comput. Sci. 1784, 297--313 (2000; Zbl 0961.68032)
Di Cosmo, Roberto; Kesner, Delia; Polonovski, Emmanuel Proof nets and explicit substitutions. (English) Zbl 0955.03064 Tiuryn, Jerzy (ed.), Foundations of software science and computation structures. 3rd international conference, FOSSACS 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1784, 63-81 (2000). MSC: 03F05 03B40 03F52 03F07 PDFBibTeX XMLCite \textit{R. Di Cosmo} et al., Lect. Notes Comput. Sci. 1784, 63--81 (2000; Zbl 0955.03064)
Bellantoni, Stephen J.; Niggl, Karl-Heinz; Schwichtenberg, Helmut Higher type recursion, ramification and polynomial time. (English) Zbl 0959.03027 Ann. Pure Appl. Logic 104, No. 1-3, 17-30 (2000). MSC: 03D65 03B40 03D15 03D20 68Q15 68Q42 68N15 03F03 03F10 03F35 PDFBibTeX XMLCite \textit{S. J. Bellantoni} et al., Ann. Pure Appl. Logic 104, No. 1--3, 17--30 (2000; Zbl 0959.03027) Full Text: DOI
Melliès, Paul-André Axiomatic rewriting theory. II: The \(\lambda\sigma\)-calculus enjoys finite normalisation cones. (English) Zbl 0971.68082 J. Log. Comput. 10, No. 3, 461-487 (2000). MSC: 68Q42 68N18 03B40 PDFBibTeX XMLCite \textit{P.-A. Melliès}, J. Log. Comput. 10, No. 3, 461--487 (2000; Zbl 0971.68082) Full Text: DOI
Kfoury, Assaf J. A linearization of the lambda-calculus and consequences. (English) Zbl 0953.03014 J. Log. Comput. 10, No. 3, 411-436 (2000). MSC: 03B40 68Q42 PDFBibTeX XMLCite \textit{A. J. Kfoury}, J. Log. Comput. 10, No. 3, 411--436 (2000; Zbl 0953.03014) Full Text: DOI Link
Khasidashvili, Zurab; Piperno, Adolfo A syntactical analysis of normalization. (English) Zbl 0953.03015 J. Log. Comput. 10, No. 3, 381-410 (2000). MSC: 03B40 68Q42 PDFBibTeX XMLCite \textit{Z. Khasidashvili} and \textit{A. Piperno}, J. Log. Comput. 10, No. 3, 381--410 (2000; Zbl 0953.03015) Full Text: DOI
Kamareddine, Fairouz; Rìos, Alejandro Relating the \(\lambda\sigma\)- and \(\lambda s\)-styles of explicit substitutions. (English) Zbl 0953.03013 J. Log. Comput. 10, No. 3, 349-380 (2000). MSC: 03B40 68Q42 PDFBibTeX XMLCite \textit{F. Kamareddine} and \textit{A. Rìos}, J. Log. Comput. 10, No. 3, 349--380 (2000; Zbl 0953.03013) Full Text: DOI
Glauert, John; Kennaway, Richard; Khasidashvili, Zurab Stable results and relative normalization. (English) Zbl 0966.68090 J. Log. Comput. 10, No. 3, 323-348 (2000). MSC: 68Q42 03B40 68N18 PDFBibTeX XMLCite \textit{J. Glauert} et al., J. Log. Comput. 10, No. 3, 323--348 (2000; Zbl 0966.68090) Full Text: DOI
Padovani, Vincent Decidability of fourth-order matching. (English) Zbl 0954.03017 Math. Struct. Comput. Sci. 10, No. 3, 361-372 (2000). MSC: 03B40 03B25 68N18 PDFBibTeX XMLCite \textit{V. Padovani}, Math. Struct. Comput. Sci. 10, No. 3, 361--372 (2000; Zbl 0954.03017) Full Text: DOI
Pitts, Andrew M. Parametric polymorphism and operational equivalence. (English) Zbl 0955.68024 Math. Struct. Comput. Sci. 10, No. 3, 321-359 (2000). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{A. M. Pitts}, Math. Struct. Comput. Sci. 10, No. 3, 321--359 (2000; Zbl 0955.68024) Full Text: DOI
Troelstra, A. S.; Schwichtenberg, H. Basic proof theory. 2nd ed. (English) Zbl 0957.03053 Cambridge Tracts in Theoretical Computer Science. 43. Cambridge: Cambridge University Press. xii, 417 p. (2000). Reviewer: Anton Setzer (Uppsala) MSC: 03F03 03-02 03-01 03F52 68N17 03F05 03B40 03G30 03B45 03F30 03F35 03B70 PDFBibTeX XMLCite \textit{A. S. Troelstra} and \textit{H. Schwichtenberg}, Basic proof theory. 2nd ed. Cambridge: Cambridge University Press (2000; Zbl 0957.03053)
Bunder, M. W. Proof finding algorithms for implicational logics. (English) Zbl 0972.03022 Theor. Comput. Sci. 232, No. 1-2, 165-186 (2000). Reviewer: G.Mints (Stanford) MSC: 03B47 03B40 03B15 03B20 03B35 PDFBibTeX XMLCite \textit{M. W. Bunder}, Theor. Comput. Sci. 232, No. 1--2, 165--186 (2000; Zbl 0972.03022) Full Text: DOI
Ritter, Eike; Pym, David; Wallen, Lincoln On the intuitionistic force of classical search. (English) Zbl 0952.03007 Theor. Comput. Sci. 232, No. 1-2, 299-333 (2000). MSC: 03B35 03B20 03B40 03F03 03B70 PDFBibTeX XMLCite \textit{E. Ritter} et al., Theor. Comput. Sci. 232, No. 1--2, 299--333 (2000; Zbl 0952.03007) Full Text: DOI
Seldin, Jonathan P. A Gentzen-style sequent calculus of constructions with expansion rules. (English) Zbl 0945.03082 Theor. Comput. Sci. 243, No. 1-2, 199-215 (2000). MSC: 03F05 03B40 PDFBibTeX XMLCite \textit{J. P. Seldin}, Theor. Comput. Sci. 243, No. 1--2, 199--215 (2000; Zbl 0945.03082) Full Text: DOI
Nour, Karim Mixed logic and storage operators. (English) Zbl 0946.03018 Arch. Math. Logic 39, No. 4, 261-280 (2000). Reviewer: Karim Nour (Le Bourget du Lac) MSC: 03B40 PDFBibTeX XMLCite \textit{K. Nour}, Arch. Math. Logic 39, No. 4, 261--280 (2000; Zbl 0946.03018) Full Text: DOI arXiv
Simmons, Harold Derivation and computation. Taking the Curry-Howard correspondence seriously. (English) Zbl 0954.03001 Cambridge Tracts in Theoretical Computer Science. 51. Cambridge: Cambridge University Press. xxv, 384 p. (2000). Reviewer: Leon Harkleroad (Wilton) MSC: 03-02 03B40 03F03 03F15 03D60 03-01 03D20 68-02 68N18 PDFBibTeX XMLCite \textit{H. Simmons}, Derivation and computation. Taking the Curry-Howard correspondence seriously. Cambridge: Cambridge University Press (2000; Zbl 0954.03001)
Haghverdi, Esfandiar Unique decomposition categories, geometry of interaction and combinatory logic. (English) Zbl 0951.03062 Math. Struct. Comput. Sci. 10, No. 2, 205-231 (2000). MSC: 03G30 03B40 03F05 PDFBibTeX XMLCite \textit{E. Haghverdi}, Math. Struct. Comput. Sci. 10, No. 2, 205--231 (2000; Zbl 0951.03062) Full Text: DOI
Ritter, Eike; Pym, David; Wallen, Lincoln Proof-terms for classical and intuitionistic resolution. (English) Zbl 0958.03012 J. Log. Comput. 10, No. 2, 173-207 (2000). Reviewer: N.Zamov (Kazan’) MSC: 03B35 03B40 PDFBibTeX XMLCite \textit{E. Ritter} et al., J. Log. Comput. 10, No. 2, 173--207 (2000; Zbl 0958.03012) Full Text: DOI Link
Longo, Giuseppe Prototype proofs in type theory. (English) Zbl 0971.03020 Math. Log. Q. 46, No. 2, 257-266 (2000). Reviewer: M.W.Bunder (Wollongong) MSC: 03B40 03B15 PDFBibTeX XMLCite \textit{G. Longo}, Math. Log. Q. 46, No. 2, 257--266 (2000; Zbl 0971.03020) Full Text: DOI
Orilia, Francesco Property theory and the revision theory of definitions. (English) Zbl 0960.03003 J. Symb. Log. 65, No. 1, 212-246 (2000). Reviewer: Pavel Materna (Praha) MSC: 03A05 03B65 03B40 PDFBibTeX XMLCite \textit{F. Orilia}, J. Symb. Log. 65, No. 1, 212--246 (2000; Zbl 0960.03003) Full Text: DOI
Kahle, Reinhard N-strictness in applicative theories. (English) Zbl 0960.03050 Arch. Math. Logic 39, No. 2, 125-144 (2000). MSC: 03F50 03B40 PDFBibTeX XMLCite \textit{R. Kahle}, Arch. Math. Logic 39, No. 2, 125--144 (2000; Zbl 0960.03050) Full Text: DOI
Barendregt, Henk; Ghilezan, Silvia Lambda terms for natural deduction, sequent calculus and cut elimination. (English) Zbl 0949.03055 J. Funct. Program. 10, No. 1, 121-134 (2000). MSC: 03F05 03B40 68N18 PDFBibTeX XMLCite \textit{H. Barendregt} and \textit{S. Ghilezan}, J. Funct. Program. 10, No. 1, 121--134 (2000; Zbl 0949.03055) Full Text: DOI
Hasegawa, Masahito Girard translation and logical predicates. (English) Zbl 0944.03013 J. Funct. Program. 10, No. 1, 77-89 (2000). MSC: 03B40 68N18 03F52 03F50 PDFBibTeX XMLCite \textit{M. Hasegawa}, J. Funct. Program. 10, No. 1, 77--89 (2000; Zbl 0944.03013) Full Text: DOI
Awodey, Steven Topological representation of the \(\lambda\)-calculus. (English) Zbl 0942.03015 Math. Struct. Comput. Sci. 10, No. 1, 81-96 (2000). MSC: 03B40 18C50 PDFBibTeX XMLCite \textit{S. Awodey}, Math. Struct. Comput. Sci. 10, No. 1, 81--96 (2000; Zbl 0942.03015) Full Text: DOI
Goguen, Healfdene; Goubault-Larrecq, Jean Sequent combinators: A Hilbert system for the lambda calculus. (English) Zbl 0957.03015 Math. Struct. Comput. Sci. 10, No. 1, 1-79 (2000). Reviewer: Teruo Hikita (Kawasaki) MSC: 03B40 PDFBibTeX XMLCite \textit{H. Goguen} and \textit{J. Goubault-Larrecq}, Math. Struct. Comput. Sci. 10, No. 1, 1--79 (2000; Zbl 0957.03015) Full Text: DOI