Dale Miller is currently Director of Research at INRIA-Saclay and LIX, École Polytechnique where he is the Scientiﬁc Leader of the Parsifal team. He has been a professor at the University of Pennsylvania, the Pennsylvania State University, and the École Polytechnique, France. Miller is the 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 Test-of-Time award of the IEEE Symposium on Logic in Computer Science. He works on many topics in the general area of computational logic, including automated reasoning, logic programming, proof theory, uniﬁcation theory, operational semantics, and, most recently, proof certiﬁcates.
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.
About the book >