VII International Symposium on
Unifying Theories of Programming

Co-located with FM 2019


UTP wordcloud
Word cloud of previous UTP symposia.

UTP 2019 will be held in the city of Porto, Portugal, on October 8, 2019, co-located with Formal Methods (FM 2019).

The main motivation for the 7th edition of the symposium is to celebrate Tony Hoareā€™s 85th Birthday. Submissions will be by invitation only and subject to a friendly review process.

Established in 2006, the UTP symposium series aims at bringing together researchers with interest in the fundamental problem of the combination of formal notations and theories of programming. The theories define, in various different ways, many common notions, such as abstraction, refinement, composition, termination, feasibility, locality, concurrency and communication. Despite these differences, such theories may be unified in a way that greatly facilitates their study and comparison. Moreover, such a unification offers a means of combining different languages describing various facets and artifacts of software development in a seamless, logically consistent, way.

Hoare and He's Unifying Theories of Programming (UTP) is widely acknowledged as one of the most significant such unification approaches. Based on their pioneering work, the aims of the UTP symposium series reaffirm the significance of the ongoing UTP project and stimulate efforts to advance.

Location and Registration

UTP 2019 will take place at the Alfandega Porto Congress Centre (APCC) in Porto, by the river Douro.

New Registration is now open at:

New Preliminary program available at:

Distinguished Invited Speaker

Keynote: A Calculus for Concurrent and Sequential Programming, jointly organised with LOPSTR'19, MPC'19, PPDP'19 and RV'19.

Tony Hoare

Tony Hoare

Tony Hoare's highest official academic qualification is an MA in Classical Greats at Oxford (1952-1956). He earned professional qualifications as an Interpreter of Russian (1956-8) as a Statistician (1958-9). He exercised his Russian as an intern at Moscow State University (1959-60), and on many subsequent visits to the Soviet Union (or Russia) and to Armenia.

His first job was in the UK Computer Industry at a small computer manufacturer, where he held posts as Programmer, Chief Engineer, and Researcher (1960-68). He led a team (including his wife Jill) in the implementation of an early compiler for ALGOL 60, which stimulated his interest in formal language definition.

He then applied for the Chair of Computing Science at the Queen's University, Belfast, and to his surprise he was appointed (1968-77). He set up the University's first undergraduate degree in Computer Science, at first Joint with mathematics. He left Belfast with regret, to return to Oxford University as Professor of Computation back at Oxford (1977-99). There he learned Denotational Semantics from Joe Stoy and Domain Theory from Dana Scott.

His first retirement job was in Cambridge with Microsoft Research (1999-2017) where he stimulated an international Grand Challenge Initiative in Verified Software. Since his second retirement, he has been an unpaid Visitor at Microsoft Research and an Honorary Member of the Cambridge University Computing Laboratory.

Program Committee




Papers will be published as an LNCS volume by Springer.

New UTP 2019 proceedings now available on-line for participants:

Springer LNCS

Proceedings from previous UTP symposia are available on-line.