Troy Kaighin Astarte Researcher in the history of computing
(KAY-guhn uh-STAR-tay)
This is the homepage for Troy Astarte.
I am a research associate in computing science at Newcastle University.
My PhD research was on the history of programming language semantics.
I am now working on a research project on the history of concurrency in programming and computing systems, funded by the Leverhulme Trust.
I am sad to announce that I will be leaving Newcastle University at the end of September 2021,
but happy to announce that I am joining Swansea University as a Lecturer in Computer Science,
with a focus on teaching.
For now these web pages will continue to exist but expect a link to a new web page soon.
In Autumn 2021, I will give a talk at the sixth History and Philosophy of Computing conference.
The title is ‘From Monitors to Monitors: an Early History of Concurrency Primitives’.
You can see the abstract and extended abstract below. Slides will come later.
There will be a time-fight tomorrow: Old problems in new logics.
As computers became multi-component systems in the 1950s, handling the speed differentials efficiently was identified as a major challenge. The desire for bet- ter understanding and control of ‘concurrency’ spread into hardware, software, and formalism. This work-in-progress talk traces some early attempts to find primitives for concurrency.
Initially, system programs called ‘monitors’ were used for directly managing synchronisation. Attempts to reframe synchronisation at a higher level led to a series of algorithms; Dijkstra’s semaphores were a reaction to the algorithms’ complexity. Towards the end of the 1960s, new desires for clearer ‘structured programming’ created a milieu in which Dijkstra, Hoare, and Brinch Hansen (among others) aimed for a concurrency primitive which embodied the new view of programming. Via conditional critical regions and Dijkstra’s ‘secretaries’, the monitor appeared to provide the desired encapsulation. A few programming languages adopted the construct: we finish by considering Modula and Concurrent Pascal.
This story shows the effects of grappling with the power brought by concurrency while trying to manage greater conceptual (and textual) complexity. The actors involved sought a balance between abstraction and tolerable implementation and their work demonstrates changing priorities in programming and computer science.
In Summer 2021, I gave a talk entitled ‘There will be a time-fight tomorrow: Old problems in new logics’.
The longer and more preliminary version was given at the Oxford History of Mathematics forum,
and the more condensed version at ICHST 2021.
I think there's a good story in here, but I wasn't totally happy with how it went at ICHST—
the balance of timings was somewhat off.
This is an advantage to the reader of the slides, linked below, as they can be read at a choice of pace!
The presenter notes give a flavour of the words spoken alongside each slide.
There will be a time-fight tomorrow: Old problems in new logics.
Consideration of temporal properties of logic and philosophy has an ancient history, stretching as far back as Aristotle’s future contingents and Diodorus Cronus’ master argument. Debate on this topic continued through the scholastic period, but saw detailed and thorough treatement only in the 1950s. A. N. Prior developed ‘tense logic’, a form of modal logic in which notions of time and contingency are expressed as modalities. Although Prior saw an immediate application to computing, the ideas broke into this field only in the 1970s, and via alternate means.
In the late 1960s Manna was working on systems for proving termination of (non-concurrent) programs. Burstall took some of Manna’s ideas and gave them a different notation in a 1974 paper—and made the connection to modal and temporal operators. Meanwhile, Pnueli, who had worked alongside Manna and Francez on cyclical programs, took Burstall’s ideas and applied them to concurrent behaviour, naming this ‘The temporal logic of programs’. Handling the behaviour of concurrent programs has been recognised as a difficult task since at least the 1960s and the 70s saw the emergence of various theoretical frameworks for modelling and reasoning about concurrent behaviour.
The case of temporal logic demonstrates an example of ancient ideas considered purely philosophical ending up with serious practical applications. One interesting facet of this is the rediscovery of many old problems in new contexts. Computer scientists working with temporal logic came against and argued about issues such as whether time should be considered branching or linear; the interpretation of future tensed propositions in the present; and the creation of appropriate models for logical systems. In most cases, these computer scientists considered these problems entirely unaware of the history behind them.
This talk explores the ‘logic’ background of temporal logic and investigates how the ideas came into computing. It considers the early field of temporal logic and shows examples of old arguments recurring in new contexts.
As Spring emerges in 2021, research continues on the history of concurrency project.
I have paused working on temporal logic temporarily,
and I am now working on a chapter about programming language constructs.
I will be giving a talk about temporal logic at ICHST 2021.
I am also working towards something publishable on programming languages.
With Tim Denvir, I co-delivered the Peter Landin Semantics Seminar for the BCS Formal Aspects of Computer Science group in December 2020.
My section of the talk was called ‘ALGOL 60 @ 60: More on semantics’ and was, I immodestly admit, rather well-received.
I also thoroughly enjoyed giving it.
The abstract for the whole talk, and the slides for my part, are linked in the buttons below.
The slides include the presenter notes, which give a decent flavour of the material I delivered.
A video recording can me found online by clicking the button below.
Algol 60 @ 60: its place in formal semantics
Algol 60, an inspiration for many languages which followed it, Pascal, C, Simula, Java and others, was very carefully defined. Following its predecessor International Algorithmic Language (IAL, or later ALGOL 58), its syntax was defined in BNF, itself a formal language, in the “Report” and “Revised Report on the Algorithmic Language Algol 60”, generally known as the Algol 60 Report.
From the report, it is clear that the whole project was guided by formal considerations, even if there was no specific formal semantics in the definition. Peter Landin was one of several people who published a formal semantics for Algol 60: Landin’s came in two parts in 1965 in CACM Volume 8.
This was an early part of an emerging zeitgeist for formal semantic specification of programming languages. The talk will describe some of the history of the language’s definition and the background of its authors, and will comment upon Peter Landin’s semantics and Algol’s relation to Church's λ-calculus. Some other semantic descriptions of ALGOL 60 will be overviewed in addition. Finally, the impact and influence of ALGOL 60 will be explored.
In May 2020 I finished a draft of a paper summarising the results of my PhD research.
I am in the process of significantly revising it for submission to an edited volume;
the resultant paper is going to be rather different (and shorter!).
I have published the longer paper as a Technical Report, which is now linked in Publications.
Work on research and teaching was slowed by the COVID-19 pandemic.
However, it did not stop, and I managed to bring another year of CSC3321 to a successful close in May 2020.
Remote teaching was interesting and challenging, but my students seemed satisfied.
Remote research was equally challenging, but my work on temporal logic still progressed.
An abstract for a talk I plan to give in 2021 can be found by clicking on the links below and will give a flavour of my current research.
There will be a time-fight tomorrow: Old problems in new logics
Consideration of temporal properties of logic and philosophy has an ancient history, stretching as far back as Aristotle’s future contingents and Diodorus Cronus’ master argument. Debate on this topic continued through the scholastic period, but saw detailed and thorough treatment by A. N. Prior, who developed ‘tense logic’ in which notions of time and contingency are expressed as modalities. Although Prior saw an immediate application to computing, the ideas broke into this field only in the 1970s, and via alternate means.
In the late 1960s Manna was working on systems for proving termination of programs; Burstall made the connection to modal and temporal operators. Pnueli took Burstall’s ideas and applied them to concurrent programming, naming this ‘The temporal logic of programs’.
The case of temporal logic demonstrates an example of ancient ideas, once considered purely philosophical, ending up with serious practical applications. One interesting facet of this is the rediscovery of many old problems. Computer scientists working with temporal logic came against and argued about issues such as whether time should be considered branching or linear; the interpretation of future tensed propositions in the present; and the creation of appropriate models for logical systems. In most cases, these computer scientists considered these problems entirely unaware of the history behind them.
This talk explores the ‘logic’ background of temporal logic and investigates how the ideas came into computing. It considers the early field of temporal logic and shows examples of old arguments recurring in new contexts.
In January 2020, I travelled to Amsterdam once again to teach on the ‘History of Digital Cultures’ course at Universiteit van Amsterdam.
A continually valuable experience, I supervised Master's students researching topics like the history of the Agile development methodology, and cyber warfare.
In November 2019, I officially started working on the Leverhulme Trust funded project “Separation and Interference: learning from the history of concurrency”.
This is an exciting project with a lot of scope; I have started by looking at the history of temporal logic.
My collaborator Cliff Jones is researching process algebras.
Later in October 2019, the History of Formal Methods 2019 (HFM2019) workshop took place,
as part of FM'19.
I was co-organiser and co-chair of the workshop, alongside my Newcastle colleague Brian Randell.
This full-day event featured talks on the history of various different kinds of formal methods,
from B to Z.
We finished the day with discussion on the topic “What have formal methods ever done for us?” which was open to the whole audience.
Proceedings are now published; see the link below.
In October 2019, I attended the SHOT annual conference in Milan,
and the SIG-CIS meeting co-located with them.
I did not give a talk there; however I did at the subsequent HaPoC 2019 conference.
The talk was entitled ‘On the difficulty of describing difficult things’ and was a summary of the findings from my PhD research.
You can see the short and extended abstracts and slides for that talk by clicking on the buttons below.
I have written a paper on this material and am in the process of finding publication.
On the Difficulty of Describing Difficult Things
In the 1960s, a full formal description was seen as a crucial and unavoidable part of creating a new programming language. A key part of that was a thorough and rigorous description of the semantics. However, in the decades since, the focus on providing this has somewhat diminished. Why was formal semantics once seen as so critical? Why did it not succeed in the ways hoped?
My PhD was spent researching the early history of programming language semantics, with a particular focus on the IBM Laboratory Vienna under Heinz Zemanek, and the Programming Research Group at Oxford University under Christopher Strachey. It could also be seen as an history of model-based (rather than algebraic or axiomatic) semantics. In this talk, I will present the key findings of my research, as a way to whet my audience’s appetite for my thesis, and argue that formal description was a crucial part of the formation of theoretical and formal computer science in the European tradition.
At the start of June 2019,
the Newcastle University Historic Computing Committee hosted an event on the history of computing at Newcastle,
specifically the acquisition of the IBM System/360-67 machine and the deployment of the Michigan Terminal System.
Together these were groundbreaking because they allowed time-sharing—the
use of the computer by multiple users at the same time.
The slides from the event and the large information handout can be found by clicking on the buttons below.
In May 2019 I wrapped up teaching the Stage 3 course ‘CSC3321: Understanding Programming Languages’,
which I took over from my colleague Cliff Jones.
This is an advanced course on the semantics of programming languages,
and teaching it was an extremely valuable and enjoyable experience.
Thanks to all of my students!
In March 2019, I was made the new chair of the Newcastle University Historic Computing Committee.
This group of volunteers from both NUIT (the University's IT Service) and the School of Computing,
curates a large collection of artefacts relating to computing at Newcastle University.
The collection was formed from Roger Broughton's collection (see the link for his web pages on the collection) gathered over many years as operations supervisor for the IT Service (in its various guises).
The Committee now is working on cataloguing every artefact in its possession
(helped by a new catalogue website designed by Lindsay Marshall),
as well as organising exhibitions in cabinets around the Urban Sciences Building.
In February 2019, I passed my viva subject to minor corrections. My examiners were Adrian Johnstone (external) and Jason Steggles (internal). My corrections were approved in June 2019 and I graduated in July 2019.
A copy of my thesis can be found below in the Publications section.
In January 2019, I returned to Amsterdam again to teach on the ‘History of Digital Cultures’ course at Universiteit van Amsterdam.
I joined the ANR research project PROGRAMme which is a historical and philoshopical investigation into the question “What is a (computer) program?”
This is an international interdisciplinary group effort and we last met in October 2018 in Bertinoro, Italy, for a few days of stimulating intellectual discussion.
During that time we launched the project wiki—not yet open to the general public—which we hope will be an interesting vehicle for collaborative work.
I took a break from thesis writing to attend the European Society for the History of Science Biennial Conference 2018.
There, I gave a talk entitled ‘Origins and Impact of Formal Semantics’,
a rather grand title for what was mostly a talk about John McCarthy's work in formal semantics.
Abstract and the slides can be found from the buttons below.
Formalising Meaning: a History of Programming Language Semantics
The emergence of high-level programming languages that began in the late 1950s brought great advantages to the programming community in terms of programmer productivity, ease of design, and the ability to use programs on different machines. However, the additional abstraction created new problems: how can a programmer be certain of the meaning of constructs in a programming language? How can a designer reason about the correctness of a program? How can one have trust that a compiler correctly reflects the semantics of a programming language?
Beginning in the 1960s, a school of study developed to address these concerns: the formal specification of programming languages. The most interesting aspect of this work concerns the semantics, or meaning, of the languages concerned. At first, the proponents of formal semantics were full of enthusiasm and ambition about their techniques. Yet, over time, the expected penetration of this work was not achieved despite continued theoretical study.
This talk will situate the field of formal semantics within the history of computing. It will explore the various motivations and expectations of the historical actors involved in formal semantics. It will then consider how well the various different proposed solutions to the semantic problem achieved these goals, before examining the other ways in which work on formal semantics impacted computing generally.
The majority of 2018 was spent writing my thesis ‘Formalising Meaning: a History of Programming Language Semantics’.
It is lengthy and goes rather in-depth in places, but I am quite pleased with it.
You can read the abstract by clicking the button below.
Once it has been submitted, I will host it here for the hordes of excited readers.
Formalising Meaning: a History of Programming Language Semantics
The emergence of high-level programming languages in the 1950s brought a series of challenges to the burgeoning computing community. Many of these centred around the difficulty of determining precisely the meaning of programming languages. This was a key issue for both those writing translators for languages and those writing programs in these languages. People in the computing and mathematics worlds attempted to address these challenges by creating a variety of ways to describe the semantics of high-level languages (the issue of defining syntax was more quickly resolved).
The history of the development of formal semantic description techniques is explored, with a particular focus on two centres of research: the IBM Laboratory in Vienna, and the Programming Research Group in Oxford. The stories of these two threads of development create interesting contrasts and similarities and discussing them—as well as the previous works that motivated them and the subsequent work inspired by them—can tell us much about programming languages and formal computing today, as well as the culture and context of computing in the 1960s and 1970s.
This work takes both a historical and technical approach. Looking at historical developments, considering the people involved in research, their motivations, the situations in which they worked, and how they interacted informs understanding of their technical outputs. Exploring the technical side, however, also helps uncover additional historical angles, such as interactions and influences both positive and negative.
I spent the month of January 2018 in Amsterdam,
teaching on the History of Digital Cultures module offered by the Universiteit van Amsterdam
(an old version of the course description can be found on the UvA website).
This wonderful opportunity was offered to me by
Gerard Alberts,
a very fine historian.
I had a great time supervising students through their month-long research projects,
and was very impressed with the quality of work produced.
I also feel I learnt a lot about the process of history, and believe I will write a better thesis as a result.
In October 2017, I went to the
Fourth International Conference on the History and Philosophy of Computing
in Brno,
an excellent conference full of interesting talks and even more interesting people.
There, I presented a talk entitled ‘Towards an Interconnected History of Semantics’,
which—as implied by the word 'towards'—was something of a work-in-progress.
The aim was to address the confluence and influence in the history of semantics rather than making comparisons,
and the talk was essentially a series of anecdotes about various events.
A short abstract and slides for the talk can be found by clicking the buttons below.
Additionally, an 'extended abstract' three pages in length is also available.
I also gave a version of the talk at the BSHM Research in Progress symposium again in February 2018.
Towards an Interconnected History of Semantics
Formal semantics is often discussed in terms of disparate approaches: operational, denotational, axiomatic, and by equivalence. Divisions are also made in terms of locations: the IBM group in Vienna and the Programming Research Group in Oxford are examples.
These are often useful distinctions to make when discussing the technicalities of semantics. To present a historical account in this siloed way, however, could be problematic. In fact there were a number of important points of interaction between the people and groups of people involved on working with formal semantics. Furthermore, these and other interactions led to the sharing and adoption of ideas between groups.
Some important interactions include the Formal Language Description Languages conference in Baden-bei-Wien in 1964; Mervyn Pragnell's unofficial reading groups in London in the early 1960s; and the IFIP Working Group 2.2 meeting in Vienna in 1969.
This talk will describe some of these interactions and attempt to explore their importance on the history and development of formal semantics.
The British Society for the History of Mathematics invited me to their Research in Progress symposium held at the Queen's College, Oxford, in February 2017.
There I gave a talk about a particularly important point in the history of programming language semantics,
the 1964 Formal Language Description Languages conference held in Baden-bei-Wien.
The slides and abstract for this talk, called ‘Formalism in the Forest: the 1964 Formal Language Description Languages IFIP Working Conference’, may be found below.
I attended the
Third Symposium for the History and Philosophy of Programming
in Paris on 25th June 2016,
and presented on the joint work I have been doing with Cliff Jones.
The title of the presentation was
‘Formal semantics of ALGOL 60: a comparison of four descriptions’.
You can read the extended abstract for the talk or see the slides by clicking the appropriate button below.
Formal semantics of ALGOL 60: a comparison of four descriptions
We are working on the history of formal descriptions of the semantics of programming languages. Semantic descriptions are structured, mathematical models or rule sets which enable reasoning about the effects of programs written in the language. Semantic descriptions offer this ability to reason by (i) providing abstract interpreters that, given a program and a starting state, either compute the final state or characterise the set of permissible final states; (ii) mapping the given language into tractable mathematical functions (in simple cases, functions from states to states); or (iii) providing rules of inference for reasoning about assertions that describe the effect of programs. These broad categorisations are usually referred to as (i) operational; (ii) denotational; and (iii) axiomatic.
One of the most frequently defined languages is ALGOL 60, which has been influential in the history of programming languages in many ways. It is a simple but powerful language, with elegant and clean concepts at the heart of its design; many important techniques in compiler design were developed as a result of ALGOL 60, such as Dijkstras display mechanism. The syntax definition method known as Backus–Naur Form (BNF), still the academic standard, was developed for ALGOL 60, and the concise natural language semantics and context conditions described the language carefully (if informally and incompletely) in the ALGOL Report.
There exist at least four reasonably complete formal semantic descriptions of ALGOL 60 in fundamentally different styles (two are operational and two denotational) and these are used as a vehicle for the comparison of the underlying approaches used in language descriptions in the period 1960–1980.
Starting with a key reference of McCarthy's paper at the 1964 Formal Language Description Languages IFIP Working Conference (which only addresses a subset of ALGOL 60 but illustrates many important ideas), we review semantic descriptions in VDL, Functional, Oxford Denotational, and VDM Denotational semantics. We attempt to present only the key aspects of the definitions, sifting away the many stylistic issues which do not relate to the underlying semantic approaches: for example, we look at handling of jumps, name spaces, and type procedure evaluation. We will also sketch the contexts in which these definitions were written.
‘The history of programming language semantics: an overview’ is a technical report.
It summarises the major findings of my PhD research,
exploring motivations for semantics work, various factors that influenced the work,
and criticism of semantics.
A conclusion is made about the impact of formal semantics work on the development of computer science.
The emphasis is on contextual factors rather than technical ones.
The history of programming language semantics: an overview
In the 1960s, a full formal description was seen as a crucial and unavoidable part of creating a new programming language. A key part of that was a thorough and rigorous description of the semantics. However, in the decades since, the focus on providing this has somewhat diminished. Why was formal semantics once seen as so critical? Why did it not succeed in the ways hoped? These questions are explored by considering the history of model-based approaches to describing programming languages, with a particular focus on the IBM Laboratory Vienna under Heinz Zemanek, and the Programming Research Group at Oxford University under Christopher Strachey. It is shown that there were a variety of different approaches to the problem, stemming from the different backgrounds of the people and groups involved. The story of formal language description is in some ways also the story of early programming languages and the integration of mathematics into the emerging new field of computer science, resulting in the formation of theoretical computing in the European style.
The history of programming language semantics: an overview
@techreport{Astarte20-TR,
Author = {Astarte, Troy K.},
Institution = {Newcastle University School of Computer Science},
Month = {jun},
Number = {CS-TR-1533},
Title = {The history of programming language semantics: an overview},
Type = {Technical Report},
Year = {2020}}
Formalising Meaning: a History of Programming Language Semantics
is my PhD thesis.
The work explores the development of formal techniques for describing the meaning of programming languages,
with a particular focus on the work done at the IBM Laboratory Vienna,
and the Programming Research Group at Oxford University.
There is some technical explication of the ideas involved as well as exploration of the motivations
of the researchers,
discussions of interactions,
and placing of formal semantics work in the broader history of computer science.
In particular, I argue that formal language description represents the core way in which theoretical
computer science developed in Europe.
The thesis will be available eventually through Newcastle University Library,
but for now, a copy can be downloaded using the buttons below.
Challenges for semantic description: comparing responses from the main approaches
@phdthesis{AstartePhD,
Author = {Astarte, Troy K.},
Month = {6},
School = {Newcastle University},
Title = {Formalising Meaning: a History of Programming Language Semantics},
Year = {2019}}
‘Challenges for semantic description:
comparing responses from the main approaches’
is a paper authored by Cliff Jones and me.
It is a technical explanation of some of the aspects of programming languages that make writing semantics tricky,
and a comparison of some of the solutions proposed.
It includes the semantics of an example core language,
and a more realistic concurrent object-oriented language.
This paper has been published as a technical report and also in the proceedings of SETSS 2017.
These proceedings are published as LNCS 11174.
Challenges for semantic description:
comparing responses from the main approaches
Although there are thousands of programming languages, most of them share common features. This paper reviews some key underlying language concepts and the challenges they present to the task of formally describing language semantics. The responses to these challenges in operational, axiomatic and denotational approaches to semantic description are reviewed. There are interesting overlaps between these responses; similarities are exposed even where accidental notational conventions disguise them so that essential differences can be pinpointed. Depending on the objectives of writing a formal semantic description of a language, one or other approach might be considered the best choice. An argument is made for increasing the use of formal semantics in language design and here it is suggested that the operational approach is the most viable for a complete language description.
Challenges for semantic description:
comparing responses from the main approaches
Although there are thousands of programming languages, many of them share common features. This paper reviews some key underlying language concepts and the challenges they present to the task of formal semantic description. Most material concerns the responses in operational, axiomatic and denotational approaches to the description of programming languages. There are interesting overlaps between the responses of these main approaches to the challenges posed by the language concepts: these similarities are exposed even where accidental details often disguise them; essential differences are also pinpointed.
Challenges for semantic description: comparing responses from the main approaches
@techreport{JonesAstarte2017-TR,
Author = {Jones, Cliff B. and Astarte, Troy K.},
Institution = {Newcastle University School of Computer Science},
Month = {November},
Number = {CS-TR-1516},
Title = {Challenges for semantic description: comparing responses from the main approaches},
Type = {Technical Report},
Year = {2017}}
Challenges for semantic description: comparing responses from the main approaches
@inproceedings{JonesAstarte2018-SC,
Author = {Jones, Cliff B. and Astarte, Troy K.},
Booktitle = {Proceedings of the 3rd School on Engineering Trustworthy Software Systems},
Editor = {Bowen, Jonathan P. and Liu, Zhiming},
Number = {11174},
Pages = {176--217},
Series = {Lecture Notes in Computer Science},
Title = {Challenges for semantic description: comparing responses from the main approaches},
Year = {2018}}
‘Formalism in the Forest: the 1964 Formal Language Description Languages IFIP Working Conference’ is a draft paper I have written connected with the talk given at the BSHM mentioned above.
The paper, for which a first draft has been written but to which extensions and corrections are yet to be made, is currently on an indefinite hiatus,
and may simply end up as content in my thesis.
The abstract can be read below, but note that it is the same as given for the BSHM event.
Formalism in the Forest: the 1964 Formal Language Description Languages IFIP Working Conference
The emergence of high-level programming languages in the 1950s brought a series of challenges to the burgeoning computing community. Many of these centred around the difficulty of determining precisely the meaning of programming languages, and programs written in these languages. A number of different people in the computing and mathematics worlds attempted to address these challenges by creating a variety of ways to describe the syntax, grammars, and especially semantics of high-level languages. Interest in this topic came together at a conference on the subject held in Baden-bei-Wien in September 1964, an extremely important event in the history of theoretical and formal computer science. The story of this conference and some of its participants will be explored.
‘Formal semantics of ALGOL 60: four descriptions in their historical context’ is a paper co-written with Cliff Jones.
It looks at technical and historical aspects of four formal descriptions of ALGOL 60.
There is also an earlier technical report version of the paper, published with a slightly different title.
An Exegesis of Four Formal Descriptions of ALGOL 60
The programming language ALGOL 60 has been used to illustrate several different styles of formal semantic description. This paper identifies the main challenges in providing a formal semantics for imperative programming languages and reviews the responses to these challenges in four relatively complete formal descriptions of ALGOL 60. The aim is to identify the key concepts rather than get bogged down in the minutiae of notational conventions adopted by their authors. As well as providing historical pointers and comparisons, the paper attempts to draw some general conclusions about semantic description styles.
An Exegesis of Four Formal Descriptions of ALGOL 60
@techreport{JonesAstarte2016-TR,
Author = {Jones, Cliff B. and Astarte, Troy K.},
Institution = {Newcastle University School of Computer Science},
Month = {September},
Note = {Forthcoming as a paper in the HaPoP 2016 proceedings.},
Number = {CS-TR-1498},
Title = {{An Exegesis of Four Formal Descriptions of ALGOL 60}},
Type = {Technical Report},
Url = {https://assets.cs.ncl.ac.uk/TRs/1498.pdf},
Year = {2016}}
Formal semantics of ALGOL 60: a comparison of four descriptions
The programming language ALGOL 60 has been used to illustrate several different styles of formal semantic description. This paper identifies the main challenges in proiding formal semantics for imperative programming languages and reviews the responses to these challenges in four relatively complete formal descriptions of ALGOL 60. The aim is to identify the key concepts rather than become distracted by the minutiae of notational conventions adopted by their authors. This paper also explores the historical reasons for the development of these descriptions in particular, and gives some general historical background of the groups involved (the IBM laboratories in Vienna and Hursley, and Oxford’s Programming Research Group).
An Exegesis of Four Formal Descriptions of ALGOL 60
@inproceedings{AstarteJones2018-A60,
Author = {Astarte, Troy K. and Jones, Cliff B.},
Booktitle = {Reflections on Programming Systems - Historical and Philosophical Aspects},
Editor = {De Mol, Liesbeth and Primiero, Giuseppe},
Pages = {71--141},
Publisher = {Springer Philosophical Studies Series},
Title = {Formal Semantics of {ALGOL 60}: Four Descriptions in their Historical Context},
Year = {2018}}
I am interested in the history of computing,
in particular the history of theoretical computer science,
as well as the history of mathematics.
I also take an interest in the formal and theoretical aspects of computer science.
This includes semantics of programming languages,
modelling of systems (including and especially concurrent systems),
and verification of programs and systems.
Beyond computing, I enjoy
drum & bass music,
tabletop games,
cooking vegan food, and
cats
and
dogs.
Lately I have also got into photography, which you can see on Twitter: @TKA_Photos.
You can contact me on the following address: troy dot astarte at ncl dot ac dot uk (replace with appropriate punctuation).
Web page last updated: 2021-09-14.