All Stories

  1. Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers

    Article • Proceedings of the ACM on Programming Languages, January 2024, ACM (Association for Computing Machinery)

    Dr Hiroshi Unno

  2. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification

    Article • Proceedings of the ACM on Programming Languages, January 2023, ACM (Association for Computing Machinery)

    Dr Hiroshi Unno

  3. Software model-checking as cyclic-proof search

    Article • Proceedings of the ACM on Programming Languages, January 2022, ACM (Association for Computing Machinery)

    Dr Hiroshi Unno

  4. A Fixpoint Logic and Dependent Effects for Temporal Property Verification

    Article • July 2018, ACM (Association for Computing Machinery)

    Dr Hiroshi Unno

  5. Relatively complete refinement type system for verification of higher-order non-deterministic programs

    Article • Proceedings of the ACM on Programming Languages, January 2018, ACM (Association for Computing Machinery)

    Dr Hiroshi Unno

  6. Verification of tree-processing programs via higher-order mode checking

    Article • Mathematical Structures in Computer Science, November 2014, Cambridge University Press

    Dr Hiroshi Unno