He is a Director of Research at Inria Saclay and one of the designers of the λProlog programming language and the Abella interactive theorem prover.
[1][2] Miller is most known for his research on topics in computational logic, including proof theory, automated reasoning, and formalized meta-theory.
[12] With Alwen Tiu, Miller extended the proof theory for fixed points and first-order quantification to incorporate λ-tree syntax.
[13] Working with Nadathur, Tiu, Andrew Gacek, and Kaustuv Chaudhuri, Miller helped design the Abella interactive theorem prover.
Since this prover directly supports λ-tree syntax, it is possible to use it to reason inductively and coinductively on syntactic objects containing binding.
This prover has successfully been applied to the formalized meta-theory of the λ-calculus, the π-calculus, and to programming languages specified using operational semantics.
[15] Working with Chuck Liang, he has helped to develop the notion of focused sequent calculus proof.