Collaborated with:
Y.Satake T.Terauchi S.Torii H.Sakamoto Akihiro Murase N.K.0001 R.Sato
Talks about:
program (3) higher (3) order (3) function (2) verif (2) determinist (1) proposit (1) complet (1) tempor (1) system (1)
Person: Hiroshi Unno 0001
DBLP: 0001:Hiroshi_Unno
Contributed to:
Wrote 4 papers:
- CAV-2017-UnnoTS #automation #horn clause #induction
- Automating Induction for Solving Horn Clauses (HU0, ST, HS), pp. 571–591.
- CAV-2018-Satake0 #functional #higher-order #logic #source code
- Propositional Dynamic Logic for Higher-Order Functional Programs (YS, HU0), pp. 105–123.
- POPL-2016-MuraseT0SU #functional #higher-order #source code #verification
- Temporal verification of higher-order functional programs (AM, TT, NK0, RS, HU0), pp. 57–68.
- POPL-2018-0001ST #higher-order #nondeterminism #refinement #source code #type system #verification
- Relatively complete refinement type system for verification of higher-order non-deterministic programs (HU0, YS, TT), p. 29.