Martin Henson (computer scientist)

Last updated

Martin C. Henson
MartinHenson.jpg
Born14 October 1954 (1954-10-14) (age 69)
Reading, UK
NationalityBritish
Alma mater University of Southampton, University of Reading, University of Essex
Scientific career
Fields Computer science, formal methods, academic accreditation, international development
Institutions University of Essex

Professor Martin C. Henson FBCS FRSA (born 14 October 1954) is an English computer scientist based at the University of Essex. [1] He is dean for international affairs and is affiliated to the School of Computer Science & Electronic Engineering. [2] [3] Henson was head of the department of computer science from 2000 to 2006.

Contents

Education

Martin Henson was educated at The Bulmershe School in Woodley, Berkshire, at the University of Southampton (BSc, 1976), at the University of Reading (PGCE, 1977), and the University of Essex (MSc, 1981).

Academic research

Henson's academic work is in the area of formal methods to aid software engineering. His early work was in programming language semantics, especially using algebraic approaches for structuring compiler and interpreter generation from semantic descriptions. He moved on to work in functional languages, focusing on program verification and transformation, pioneering an approach to program transformation, adapted from work in semantic equivalences, using higher-order generalisations and relational constraints. Since the late 1990s, he has undertaken research into the design and use of logic in specification and program development. With Steve Reeves, he has studied the formal semantics of the Z notation in detail. This work was used in the international ISO standard for the Z notation. [4] Most recently he has proposed a new approach to specification, based on specification theories, developing the specification logic nuZ – a Z-like specification language with a monotonic schema calculus. This was first presented in a talk in the BCS-FACS seminar series at the British Computer Society in London in 2005. [5] [6]

Henson has been a Fellow of the British Computer Society since 2009 [7] and holds a Visiting Professorship at the University of Waikato in New Zealand. [8]

International development

Henson ran a blog on his activities as Dean at Essex University. [9] He has worked internationally on academic accreditation, institutional licensure and strategic planning, with a focus on the Middle East and particularly for the Commission for Academic Accreditation in the United Arab Emirates. [10] He is an external reviewer for the Oman Academic Accreditation Authority [10] in Muscat, Oman, and has been a Fellow of the Royal Society of Arts since 2010.

Professor Henson has given keynote addresses on outcomes-based curriculum development, [11] in Saudi Arabia, on institutional research strategic planning [12] in Indonesia, and on the internationalisation of higher education [13] in China. His other international consultancy has included Jordan, Kuwait, the West Indies, and Sweden.

Selected publications

Books

Related Research Articles

In computer science, pseudocode is a description of the steps in an algorithm using a mix of conventions of programming languages with informal, usually self-explanatory, notation of actions and conditions. Although pseudocode shares features with regular programming languages, it is intended for human reading rather than machine control. Pseudocode typically omits details that are essential for machine implementation of the algorithm. The programming language is augmented with natural language description details, where convenient, or with compact mathematical notation. The purpose of using pseudocode is that it is easier for people to understand than conventional programming language code, and that it is an efficient and environment-independent description of the key principles of an algorithm. It is commonly used in textbooks and scientific publications to document algorithms and in planning of software and other algorithms.

<span class="mw-page-title-main">Z notation</span> Formal specification language used for describing and modelling computing systems

The Z notation is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer-based systems in general.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Peter Landin</span> British computer scientist (1930–2009)

Peter John Landin was a British computer scientist. He was one of the first to realise that the lambda calculus could be used to model a programming language, an insight that is essential to the development of both functional programming and denotational semantics.

<span class="mw-page-title-main">Samson Abramsky</span> British computer scientist

Samson Abramsky is Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 to 2021.

<span class="mw-page-title-main">Jonathan Bowen</span> British computer scientist

Jonathan P. Bowen FBCS FRSA is a British computer scientist and an Emeritus Professor at London South Bank University, where he headed the Centre for Applied Formal Methods. Prof. Bowen is also the Chairman of Museophile Limited and has been a Professor of Computer Science at Birmingham City University, Visiting Professor at the Pratt Institute, University of Westminster and King's College London, and a visiting academic at University College London.

The B method is a method of software development based on B, a tool-supported formal method based on an abstract machine notation, used in the development of computer software.

<span class="mw-page-title-main">Cliff Jones (computer scientist)</span> British computer scientist (born 1944)

Clifford "Cliff" B. Jones is a British computer scientist, specializing in research into formal methods. He undertook a late DPhil at the Oxford University Computing Laboratory under Tony Hoare, awarded in 1981. Jones' thesis proposed an extension to Hoare logic for handling concurrent programs, rely/guarantee.

<span class="mw-page-title-main">Dines Bjørner</span> Danish computer scientist

Professor Dines Bjørner is a Danish computer scientist.

The Z User Group (ZUG) was established in 1992 to promote use and development of the Z notation, a formal specification language for the description of and reasoning about computer-based systems. It was formally constituted on 14 December 1992 during the ZUM'92 Z User Meeting in London, England.

<span class="mw-page-title-main">BCS-FACS</span> Specialist Group of the BCS

BCS-FACS is the BCS Formal Aspects of Computing Science Specialist Group.

<span class="mw-page-title-main">John C. Reynolds</span> American computer scientist (1935–2013)

John Charles Reynolds was an American computer scientist.

<span class="mw-page-title-main">Programming language theory</span> Branch of computer science

Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.

Algebraic specification is a software engineering technique for formally specifying system behavior. It was a very active subject of computer science research around 1980.

Steve Reeves is a computer scientist based at the University of Waikato in New Zealand. He has been in the various roles of Associate Dean, Programme Co-ordinator and Head of Department of Software Engineering. He has undertaken research work on the Z notation, formal methods for GUI design, a general theory of refinement and logic for veracity.

Professor Raymond Turner is an English logician, philosopher, and theoretical computer scientist based at the University of Essex. He is best known for his work on logic in computer science and for his pioneering work in the philosophy of computer science. He is on the editorial boards for the Journal of Logic and Computation and the Stanford Encyclopedia of Philosophy, for Logic, Computation, and Agency.

Michael ("Mike") William Shields, January 20, 1950 - September 24, 2023 (aged 73) was a British computer scientist.

<span class="mw-page-title-main">Hussein Zedan</span>

Hussein S. M. Zedan was a computer scientist of Egyptian descent, mainly based in the United Kingdom.

Tim Denvir is a British software engineer, specialising in formal methods.

<span class="mw-page-title-main">Ken Robinson (computer scientist)</span> Australian computer scientist (1938–2020)

Kenneth ("Ken") Arthur Robinson was an Australian computer scientist. He has been called "The Father of Formal Methods in Australia".

References