Using Abstraction to Automate Program Improvement by Transformation. - Ian Green (AAAI, 1991)

A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (Abstract). - Peter Madden; Jane Hesketh; Ian Green; Alan Bundy (LOPSTR, 1993)

A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans. - Peter Madden; Ian Green (AISMC, 1994)

Coloured Rippling: An Extension of a Theorem Proving Heuristic. - Tetsuya Yoshida; Alan Bundy; Ian Green; Toby Walsh; David A. Basin (ECAI, 1994)

Higher-Order Annotated Terms for Proof Search. - Alan Smaill; Ian Green (TPHOLs, 1996)

Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs. - Louise A. Dennis; Alan Bundy; Ian Green (CADE, 1997)

Automation of Diagrammatic Reasoning. - Mateja Jamnik; Alan Bundy; Ian Green (IJCAI (1), 1997)

System Description: Proof Planning in Higher-Order Logic with Lambda-Clam. - Julian Richardson; Alan Smaill; Ian Green (CADE, 1998)

Observant: An Annotated Term-Rewriting System for Deciding Observation Congruence. - Raúl Monroy; Alan Bundy; Ian Green (ECAI, 1998)

Planning Equational Verification in CCS. - Raúl Monroy; Alan Bundy; Ian Green (ASE, 1998)

A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers. - Predrag Janicic; Alan Bundy; Ian Green (CADE, 1999)

Extensions to the Estimation Calculus. - Jeremy Gow; Alan Bundy; Ian Green (LPAR, 1999)

Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm. - Alessandro Armando; Alan Smaill; Ian Green (Autom. Softw. Eng., 1999)

On Automating Diagrammatic Proofs of Arithmetic Arguments. - Mateja Jamnik; Alan Bundy; Ian Green (J. Log. Lang. Inf., 1999)

Searching for a Solution to Program Verification=Equation Solving in CCS. - Raúl Monroy; Alan Bundy; Ian Green (MICAI, 2000)

Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts. - Louise A. Dennis; Alan Bundy; Ian Green (Ann. Math. Artif. Intell., 2000)

Planning Proofs of Equations in CCS. - Raúl Monroy; Alan Bundy; Ian Green (Autom. Softw. Eng., 2000)

On Automating Diagrammatic Proofs of Arithmetic Arguments. - Mateja Jamnik; Alan Bundy; Ian Green (Diagrammatic Representation and Reasoning, 2002)

On Process Equivalence = Equation Solving in CCS. - Raúl Monroy; Alan Bundy; Ian Green (J. Autom. Reason., 2009)

The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling. - Louise A. Dennis; Ian Green; Alan Smaill (J. Autom. Reason., 2011)