Richard Bornat
Encyclopedia
Richard Bornat is a noted British
author
and research
er in the field of computer science
. He is also professor
of Computer programming
at Middlesex University
. Previously he was at Queen Mary, University of London
.
. His focus is on the proof
s themselves; as opposed to any logical underpinnings. Much of the work involves discovering ways to state the properties of independent modules, in a manner that makes their composition into useful systems conducive.
Bornat (in conjunction with Bernard Sufrin of the Oxford University Computing Laboratory
) developed Jape, a proof calculator; he is involved in research on the usability of this tool for exploration of novel proofs.
Richard Bornat's PhD students have included Samson Abramsky
in the early 1980s.
In 2004, one of Bornat's students developed an aptitude test to "divide people up into programmers and non-programmers before they ever come into contact with programming." The test was first given to a group of students in 2005 during an experiment on the use of mental models in programming. At the end of the experiment, Bornat delivered a talk entitled "Dividing the Sheep from the Goats".
development. Although it has been out of print for some time, he has now made it available as an online edition.
Other publications from Bornat include:
United Kingdom
The United Kingdom of Great Britain and Northern IrelandIn the United Kingdom and Dependencies, other languages have been officially recognised as legitimate autochthonous languages under the European Charter for Regional or Minority Languages...
author
Author
An author is broadly defined as "the person who originates or gives existence to anything" and that authorship determines responsibility for what is created. Narrowly defined, an author is the originator of any written work.-Legal significance:...
and research
Research
Research can be defined as the scientific search for knowledge, or as any systematic investigation, to establish novel facts, solve new or existing problems, prove new ideas, or develop new theories, usually using a scientific method...
er in the field of computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
. He is also professor
Professor
A professor is a scholarly teacher; the precise meaning of the term varies by country. Literally, professor derives from Latin as a "person who professes" being usually an expert in arts or sciences; a teacher of high rank...
of Computer programming
Computer programming
Computer programming is the process of designing, writing, testing, debugging, and maintaining the source code of computer programs. This source code is written in one or more programming languages. The purpose of programming is to create a program that performs specific operations or exhibits a...
at Middlesex University
Middlesex University
Middlesex University is a university in north London, England. It is located in the historic county boundaries of Middlesex from which it takes its name. It is one of the post-1992 universities and is a member of Million+ working group...
. Previously he was at Queen Mary, University of London
Queen Mary, University of London
Queen Mary, University of London is a public research university located in London, United Kingdom and a constituent college of the federal University of London...
.
Research
Bornat's research interests includes program proving in separation logicSeparation logic
In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs.It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Burstall...
. His focus is on the proof
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
s themselves; as opposed to any logical underpinnings. Much of the work involves discovering ways to state the properties of independent modules, in a manner that makes their composition into useful systems conducive.
Bornat (in conjunction with Bernard Sufrin of the Oxford University Computing Laboratory
Oxford University Computing Laboratory
The Department of Computer Science, until 2011 named the Computing Laboratory , is a department of Oxford University in England...
) developed Jape, a proof calculator; he is involved in research on the usability of this tool for exploration of novel proofs.
Richard Bornat's PhD students have included Samson Abramsky
Samson Abramsky
Samson D. Abramsky FRS, FRSE is a computer scientist who currently holds the Christopher Strachey Professorship at Oxford University Computing Laboratory. He is well known for playing a leading role in the development of game semantics...
in the early 1980s.
In 2004, one of Bornat's students developed an aptitude test to "divide people up into programmers and non-programmers before they ever come into contact with programming." The test was first given to a group of students in 2005 during an experiment on the use of mental models in programming. At the end of the experiment, Bornat delivered a talk entitled "Dividing the Sheep from the Goats".
Publications
Bornat published a book entitled "Understanding and Writing Compilers: A Do It Yourself Guide", which is regarded as one of the most extensive resources on compilerCompiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
development. Although it has been out of print for some time, he has now made it available as an online edition.
Other publications from Bornat include:
- Richard Bornat and Harold Thimbleby; 1989; The life and times of ded, display editor; in J.B. Long & A. Whitefield (eds); Cognitive Ergonomics and Human-Computer Interaction; Cambridge University PressCambridge University PressCambridge University Press is the publishing business of the University of Cambridge. Granted letters patent by Henry VIII in 1534, it is the world's oldest publishing house, and the second largest university press in the world...
; pp. 225–255. - Richard Bornat and Bernard Sufrin;1999; Animating Formal Proof at the Surface: The {Jape} Proof Calculator; The Computer JournalThe Computer JournalThe Computer Journal is a journal published by the Oxford University Press on behalf of the British Computer Society. It contains peer-reviewed articles and other contributions on computer science and information systems. Its first issue appeared in 1958, and it has been published continually since...
; Vol. 42; no. 3; pp. 177–192. - Aczel, J. C., Fung, P., Bornat, R., Oliver, M., O’Shea, T., & Sufrin, B.; 1999; Influences of Software Design on Formal Reasoning; in Brewster, S., Cawsey, A. & Cockton, G. (Eds.) Proceedings of IFIP TC.13 International Conference on Human-Computer Interaction INTERACT '99; Vol. 2; pp. 3–4; Swindon, UK, British Computer SocietyBritish Computer SocietyThe British Computer Society, is a professional body and a learned society that represents those working in Information Technology in the United Kingdom and internationally...
; ISBN 1-902505-19-0. - R. Bornat; 2000; Proving Pointer Programs in Hoare Logic; in Backhouse & Oliviera (eds) MPC 2000; LNCS 1837; pp. 102–126.
- C. Calcagno, P. O’Hearn, R. Bornat; 2002; Program Logic and Equivalence in the Presence of Garbage Collection. To appear in Theoretical Computer ScienceTheoretical Computer Science (journal)Theoretical Computer Science is a computer science journal published by Elsevier, started in 1975 and covering theoretical computer science. The journal publishes 52 issues a year. It is abstracted and indexed by Scopus and the Science Citation Index...
special issue on Foundations.