山形頼之

独立行政法人 産業技術総合研究所 研究員

論文

A sequent calculus for limit computable mathematics [最終版][著者版]

Stefano Berardi, Yoriyuki Yamagata, Annals of Pure and Applied Logic 153-3 (2008), Elsevier

Strong　normalization of second-order symmetric lambda-mu calculus [最終版][著者版]

Information and Computation 193-1 (2004), Elsevier.

Strong normalization of a symmetric lambda calculus for second-order classical logic[著者版]

Archive for Mathematical Logic 41-1 (2002), Springer. Copyright: Spinger Ferlag. 最終版はhttp://link.springer.deで公開されています。(有料)

Strong normalization of second-order symmetric lambda-mu calculus[著者版]

TACS2001(Theoretical Aspects of Computer Software, 4th International Symposium), Lecture Notes in Computer Science 2215(2001), Springer. 最終版はhttp://link.springer.deで公開されています。(有料)

講演 - 査読あり

Camomile: a Unicode library for OCaml [スライド]

ML Workshop 2011

YAMPII・P2P層の実装およびモデル検査

齋藤正也、山形頼之、第4回ディペンダブルソフトウェアワークショップ(DSW06-2)

A sequent calculus for limit computable mathematics [スライド] [論文]

Stefano Berardi, 山形頼之、CL&C2006

Strong normalization of second-order symmetric lambda-mu calculus[paper]

TACS2001(Theoretical Aspects of Computer Software, 4th International Symposium)

講演 - 査読なし

Existence and consistency in bounded arithmetic [スライド]

ラムダ計算と論理の晩夏セミナー 2011

A sequent calculus for 2-backtracking [スライド]

Stefano Berardi, 山形頼之, Types Workshop 2009

技術報告

Interpretation of STM by CSP

山形頼之、孔維強、福田晃、片平典幸、Van Tang Nguyen、大崎人士(2012)

ソフトウェア更新システムのモデル検査によるセキュリティ

齋藤正也、山形頼之(2007)

ソフトウェア更新システムプロトコルの BAN Logic による安全性検証(Preliminary Version)

吉田聡、山形頼之(2007)

A sequent calculus for limit computable mathematics (Technical Report)

Stefano Berardi、山形頼之(2006)

プレプリントその他

Bounded arithmetic in free logic (2012) [arXiv]

Halting problem and incompleteness theorem [原稿]

On use of an explicit congruence Predicate in bounded arithmetic (2009) [arXiv]

連絡先

メールアドレス: yoriyuki dot yamagata at aist dot go dot jp