Structural proof theory (specifically the Gentzen-Prawitz theory of proofs) provides a foundational basis for designing and analyzing term structures and their operations. This talk illustrates this link by using the focused proof system LJF to design term structures. A key feature of LJF is the non-canonical assignment of polarization to primitive types, which gives rise to two distinct approaches to term representation. When all primitive types are given the negative polarity, focused proofs yield tree-like term structures commonly used in computational logic systems. Also, cut elimination corresponds to the standard notion of substitution. On the other hand, when all primitive types are given the positive polarity, focused proofs yield dag-like structures that are in administrative normal forms and which offer an explicit method for structure sharing. Here, cut elimination yields a different notion of substitution. We illustrate these two contrasting structuring disciplines by demonstrating how they encode untyped lambda-terms in strikingly different ways. This is joint work with Jui-Hsuan (Ray) Wu.

Dale Miller received his Ph.D. in Mathematics in 1983 from Carnegie Mellon University. He has been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and a Department Head in Computer Science and Engineering at Pennsylvania State University. He has held visiting positions at the Australian National University and the universities of Aix-Marseille, Sienna, Genoa, Pisa, and Edinburgh. He is currently Director of Research at Inria-Saclay, where he is a member of the Partout team.

Miller was a two-term editor-in-chief of the ACM Transactions on Computational Logic. He is a member of the Journal of Automated Reasoning editorial board. In 2014, he was a PC chair for CSL and LICS. He was awarded an ERC Advanced Grant in 2011, the LICS Test-of-Time awards in 2011 and 2014, and the Dov Gabbay Prize for Logic and Foundations in 2023. He is an ACM Fellow. Miller works on various topics in computational logic, including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates.