Consistency proof of an arithmetic with substitution inside a bounded arithmetic[slide]
Runtime verification for concurrent systems[slide]
Formal semantics of extended hierarchical state transition matrix by CSP[slide][paper]
Yoriyuki Yamagata, Weiqiang Kong, Akira Fukuda, Nguyen Van Tang, Hitoshi Ohsaki and Kenji Taguchi, UML&FM 2012
Camomile: a Unicode library for OCaml [slide]
ML Workshop 2011
A sequent calculus for limit computable mathematics [slide] [paper]
Stefano Berardi, Yoriyuki Yamagata, CL&C2006
Strong normalization of second-order symmetric lambda-mu calculus[paper]
TACS2001(Theoretical Aspects of Computer Software, 4th International Symposium)