Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi Type checking and typability in domain-free lambda calculi. (English) Zbl 1241.03011 Theor. Comput. Sci. 412, No. 44, 6193-6207 (2011). MSC: 03B40 PDF BibTeX XML Cite \textit{K. Nakazawa} et al., Theor. Comput. Sci. 412, No. 44, 6193--6207 (2011; Zbl 1241.03011) Full Text: DOI
Nakazawa, Koji; Tatsuta, Makoto; Kameyama, Yukiyoshi; Nakano, Hiroshi Undecidability of type-checking in domain-free typed lambda-calculi with existence. (English) Zbl 1156.03316 Kaminski, Michael (ed.) et al., Computer science logic. 22nd international workshop, CSL 2008, 17th annual conference of the EACSL, Bertinoro, Italy, September 16–19, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87530-7/pbk). Lecture Notes in Computer Science 5213, 478-492 (2008). MSC: 03B40 03B25 03B70 68N18 PDF BibTeX XML Cite \textit{K. Nakazawa} et al., Lect. Notes Comput. Sci. 5213, 478--492 (2008; Zbl 1156.03316) Full Text: DOI
Nakazawa, Koji; Tatsuta, Makoto Strong normalization of classical natural deduction with disjunctions. (English) Zbl 1141.03027 Ann. Pure Appl. Logic 153, No. 1-3, 21-37 (2008). Reviewer: M. Yasuhara (Princeton) MSC: 03F05 03B05 03B40 PDF BibTeX XML Cite \textit{K. Nakazawa} and \textit{M. Tatsuta}, Ann. Pure Appl. Logic 153, No. 1--3, 21--37 (2008; Zbl 1141.03027) Full Text: DOI
Nakazawa, Koji; Tatsuta, Makoto Strong normalization proof with CPS-translation for second order classical natural deduction. (English) Zbl 1058.03060 J. Symb. Log. 68, No. 3, 851-859 (2003); Corrigendum ibid. 68, No. 4, 1415-1416 (2003). MSC: 03F05 03B40 PDF BibTeX XML Cite \textit{K. Nakazawa} and \textit{M. Tatsuta}, J. Symb. Log. 68, No. 3, 851--859 (2003; Zbl 1058.03060) Full Text: DOI Euclid