The authors

Dale Miller is Director of Research at INRIA-Saclay and LIX, École Polytechnique . He has been a professor at the University of Pennsylvania, the Pennsylvania State University, and the École Polytechnique, France. Miller was a two-term Editor-in-Chief of the ACM Transactions on Computational Logic and has editorial duties on several other journals. He was awarded an ERC Advanced Investigators Grant in 2011 and is the recipient of the 2011 and 2014 Test-of-Time awards from the ACM/IEEE Symposium on Logic in Computer Science. He is also an ACM Fellow. Miller works on many topics in the general area of computational logic, including automated reasoning, logic programming, proof theory, unification theory, operational semantics, and proof certificates.

Gopalan Nadathur is Professor of Computer Science at the University of Minnesota. He has previously held faculty appointments at Duke University, University of Chicago, and Loyola University of Chicago. Nadathur’s research interests span the areas of computational logic, programming languages, and logic programming. His work has been regularly funded by the National Science Foundation and has appeared in publications such as the Journal of the Association of Computing Machinery, Information and Computation, the Journal of Automated Reasoning, Theoretical Computer Science, and Theory and Practice of Logic Programming among other places. He also led the effort to produce the Teyjus implementation of the λProlog language.