Watanabe Yuki

I was a student at Yonezawa Laboratory.

My work

• Extending Hoare Type Theory for Arrays. Senior thesis, 2009. (MS Word, PDF)
• 渡邊裕貴、前田俊行、米澤明憲 「配列のためのホーア型理論の拡張」 第 7 回ディペンダブルシステムワークショップ、2009。 (PDF)
• A Type-Preserving Compiler for Dependently Typed Functions with Side Effects. Master thesis interim report. (MS Word, PDF; MS PowerPoint)
• Study on Proof of Type Preservation in CPS Transformation (CPS 変換における型保存の証明に関する研究). Master thesis. (MS Word, PDF; MS PowerPoint)
  • Coq proof scripts:
    • Unsorted named representation
    • Two-sorted named representation
    • Two-sorted de Bruijn representation
    • Two-sorted locally nameless representation
    • Target language with singleton types
    These scripts can be compiled with Coq version 8.2pl1.