Research Interests
Logic, proof theory, proof search, and automated reasoning. He is also interested in automata theory, computability theory, and genetic algorithm. He is currently working on proof theory for BI family logics and separation logics.
Publications
[Conference]Automated Theorem Proving for Assertions in Separation Logic with All Connectives
Zhé Hóu, Rajeev Goré, and Alwen Tiu
To Appear in CADE25. (2015)[pdf]
[Journal]A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
Zhé Hóu, Alwen Tiu, and Rajeev Goré
Journal of Logic and Computation 2015: exv033v1-exv033. (2015)[pdf]
[Conference]Proof Search for Propositional Abstract Separation Logics via Labelled Sequents
Zhé Hóu, Ranald Clouston, Rajeev Goré, and Alwen Tiu
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '14). ACM, New York, NY, USA, 465-476. (2014)[pdf]
[Report]Proof Search for Propositional Abstract Separation Logics via Labelled Sequents
Zhé Hóu, Ranald Clouston, Rajeev Goré, and Alwen Tiu
arXiv:1307.5592 [cs.LO] (2013)[pdf]
[Conference]A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
Zhé Hóu, ALwen Tiu, and Rajeev Goré
TABLEAUX 2013: 172-187 (2013)[pdf]
[Journal]An Iterative Approach to Synthesize Business Process Templates from Compliance Rules
Ahmed Awad, Rajeev GorĂ©, Zhé Hóu, James Thomson, Matthias Weidlich
Inf. Syst. 37(8): 714-736 (2012)[pdf]
Talks
Proof Search for Propositional Abstract Separation Logics via Labelled Sequents
POPL 2014, San Diego, The U.S.
[slides]
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
TABLEAUX 2013, Nancy, France
[slides]
Implementations
To compile the following programs, you need OCaml. Those programs may run with a parameter that requires "pdflatex". Please refer to readme files for details.