On the occasion of a reception in honor of Peter Andrews's 49 years of service to the Department of Mathematical Sciences and to wish him well on his retirement.

Wednesday, April 4, 2012, 6 - 8 p.m.

Perlis Atrium, Newell Simon Hall, Carnegie Mellon University

I thought I would briefly describe the first time that I met Peter Andrews: actually, it's a moment that I'm hoping he doesn't remember himself.

In 1978, I first arrived at the Mathematics Department of CMU to start the phd program, I was unsure of the subject in mathematics I wanted to pursue. Although I am guessing, I am pretty certain that I was channeled to Peter as his student since my application material mentioned that I had done LISP programming. At that time, Peter's theorem proving efforts were being written with LISP and LISP experience was pretty rare then (and probably now too).

I remember entering the math offices on the 6th floor and learning that I was assigned to Professor Andrews as my adviser. They told me his office was upstairs and I raced up the stairwell from the 6th to the 7th floor to try to find him in his office. In my eagerness, I almost ran over a quiet man in a light blue suit trying to enter the stairwell. I didn't find Peter in his office: as I soon learned, the person I almost knocked down in the stairwell was, of course, Peter.

Despite that initial collision, I have lots of good memories of my times as a PhD student advised by Peter.

Since I knew nothing of logic and theorem proving at that time, I essentially took on some of Peter's research goals. He gave me several papers to read. That initial collection made a huge impact on me. They included

- Church 1940,
*A Formulation of the Simple Theory of Types* - Andrews 1971,
*Resolution in Type Theory* - Huet 1975,
*A unification algorithm for typed λ-calculus*

Years later when people asked me: How was it to have Peter Andrews as the judge of my dissertation, I admitted that I had found it rather scary: Peter had helped to find an error in Herbrand's thesis and he observed that Henkin hadn't gotten the description of general models quite right.

Having had Peter as an adviser also gives me the opportunity to attract PhD students by telling them that their academic genealogy could also include a Herbrand award winner as well as Alonzo Church.

I am grateful to Peter for my early lessons in logic and for providing me links to core ideas in logic and to some of the key historical players in logic.

-- Dale Miller