Ichiro Ogata

Researcher at AIST,JAPAN

Research Interests

  • Computational aspects of Classical Logic
  • Theory of Programming Language
  • Proof Theory and Linear Logic

    • Recent Research Publications

  • Ichiro Ogata
    A Proof Theoretical Account of Continuation Passing Style
    In CSL'02 LNCS 2471 pp.490-505)
    abstract: We study ``classical proofs as programs'' paradigm in Call-By-Value (CBV) setting. Specifically, we show the CBV normalization for CND (Parigot 92) can be simulated by the cut-elimination procedure for LKQ (Danos-Joinet-Schellinx 93), namely the q-protocol. We use proof-term assignment system to prove this fact. The term calculus for CND we use follows Parigot's $\lambda\mu$-Calculus with new CBV normalization procedure. A new term calculus for LKQ is presented as a variant of $\lambda$-calculus with a let-construct. We then define a translation from CND into LKQ and prove simulation theorem. We also show the translation we use can be thought of a familiar CBV CPS-translation without translation on types.
    keywords: Classical Logic, Classical Natural Deduction, LKQ, Call-By-Value, CPS-translation, classical proof theory.
    Paper: pdf
    Paper: ps.gz

    Slides: pdf
  • Ichiro Ogata
    Correspondence between Normalization of CND and Cut-Elimination of LKT
    Paper: ps.gz
  • Ichiro Ogata
    Constructive Classical Logic as CPS-calculus
    In IJFCS (international journal of foundations of functional programming, Mar. 2000, volume 11, number 1, 89-112)
    Paper: ps.gz
  • Ichiro Ogata
    A CPS-transform of Constructive Classical Logic
    In Asian Computing Science Conference (Asian99, LNCS 1742 pp.266-280)
    Paper: ps.gz
  • Ichiro Ogata
    CPS-calculus in Various Style
    In 16th anual meeting of Japan Society Software Science and Technology (JSSST99)
    Paper: ps.gz OHP: ps.gz
  • Ichiro Ogata
    Cut Elimination for Classical Proofs as Continuation Passing Style Computation
    In Asian Computing Science Conference (Asian98, LNCS 1538 pp.61-78)
    Paper: ps.gz
  • Ichiro Ogata
    A proof theoretical approach to Continuation Passing Style (Presented at TTP-tokyo)
    Paper: ps.gz

    • Other Activities

  • The goals of my research (in japanese) ps.gz
  • An Introduction to Next Generation TV game consoles (in japanese) ps.gz

    • Useful Databases

    NameIchiro Ogata
    Initials IO
    Affiliation Information Technology Research Institute, The National Institute of Advanced Industrial Sience and Technology
    Postal address 1-1-1 Umezono, Tsukuba, 305-8568, JAPAN
    Email addressi.ogata@aist.go.jp
    Telephone (voice)+81 298-61-5906
    Telephone (fax)+81 298-61-5909
    Bibliographicinformation has been collected
    Last changed(28/may/01 update)