Donor‐acceptor pair recombination luminescence from Cu2ZnSnS4 bulk single crystals K Tanaka, Y Miyamoto, H Uchiki, K Nakazawa, H Araki Physica status solidi (a) 203 (11), 2891-2896, 2006 | 117 | 2006 |
Strong normalization proof with CPS-translation for second order classical natural deduction K Nakazawa, M Tatsuta The Journal of Symbolic Logic 68 (3), 851-859, 2003 | 22 | 2003 |
Undecidability of type-checking in domain-free typed lambda-calculi with existence K Nakazawa, M Tatsuta, Y Kameyama, H Nakano Computer Science Logic: 22nd International Workshop, CSL 2008, 17th Annual …, 2008 | 17 | 2008 |
Completeness of cyclic proofs for symbolic heaps with inductive definitions M Tatsuta, K Nakazawa, D Kimura Programming Languages and Systems: 17th Asian Symposium, APLAS 2019, Nusa …, 2019 | 15 | 2019 |
Compositional Z: Confluence proofs for permutative conversion K Nakazawa, K Fujita Studia Logica 104, 1205-1224, 2016 | 14 | 2016 |
Strong normalization proofs by CPS-translations S Ikeda, K Nakazawa Information Processing Letters 99 (4), 163-170, 2006 | 13 | 2006 |
Reduction system for extensional lambda-mu calculus K Nakazawa, T Nagai International Conference on Rewriting Techniques and Applications, 349-363, 2014 | 12 | 2014 |
Failure of cut-elimination in cyclic proofs of separation logic D Kimura, K Nakazawa, T Terauchi, H Unno コンピュータ ソフトウェア 37 (1), 1_39-1_52, 2020 | 11 | 2020 |
Confluency and strong normalizability of call-by-value λμ-calculus K Nakazawa Theoretical Computer Science 290 (1), 429-463, 2003 | 11 | 2003 |
Cyclic theorem prover for separation logic by magic wand K Nakazawa, M Tatsuta, D Kimura, M Yamamura ADSL 18 (First Workshop on Automated Deduction for Separation Logics), 2018 | 6 | 2018 |
Extensional models of untyped Lambda-mu calculus K Nakazawa, S Katsumata arXiv preprint arXiv:1210.3116, 2012 | 6 | 2012 |
Strong normalization of classical natural deduction with disjunctions K Nakazawa, M Tatsuta Annals of Pure and Applied Logic 153 (1-3), 21-37, 2008 | 6 | 2008 |
An isomorphism between cut-elimination procedure and proof reduction K Nakazawa International Conference on Typed Lambda Calculi and Applications, 336-350, 2007 | 5 | 2007 |
Restriction on cut in cyclic proof system for symbolic heaps K Saotome, K Nakazawa, D Kimura Functional and Logic Programming: 15th International Symposium, FLOPS 2020 …, 2020 | 4 | 2020 |
Type Checking and Inference for Polymorphic and Existential Types. K Nakazawa, M Tatsuta CATS, 61-69, 2009 | 4 | 2009 |
Confluence proofs of lambda-mu-calculi by Z theorem Y Honda, K Nakazawa, K Fujita Studia Logica 109 (5), 917-936, 2021 | 3 | 2021 |
Development and calibration of fine collimators for the ASTRO-H soft gamma-ray detector T Mizuno, D Kimura, Y Fukazawa, S Furui, K Goto, T Hayashi, ... Space Telescopes and Instrumentation 2014: Ultraviolet to Gamma Ray 9144 …, 2014 | 3 | 2014 |
Monadic translation of classical sequent calculus JE Santo, R Matthes, K Nakazawa, L Pinto Mathematical Structures in Computer Science 23 (6), 1111-1162, 2013 | 3 | 2013 |
Function Pointer Eliminator for C Programs D Kimura, MFA Ameen, M Tatsuta, K Nakazawa Programming Languages and Systems: 19th Asian Symposium, APLAS 2021, Chicago …, 2021 | 2 | 2021 |
Failure of cut-elimination in the cyclic proof system of bunched logic with inductive propositions K Saotome, K Nakazawa, D Kimura 6th International Conference on Formal Structures for Computation and …, 2021 | 2 | 2021 |