### 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.