[Revised entry by Nicolas Troquard and Philippe Balbiani on February 16, 2023.
Changes to: Main text, Bibliography]
Logics of programs are modal logics arising from the idea of associating a modality ([alpha]) with each computer program (alpha) of a programming language. The formula ([alpha]A) is then to be read as: (A) is true after the execution of the program (alpha). This idea comes from the line of works by Engeler [1967], Hoare [1969], Yanov [1959], and others who formulated and studied logical languages in which the properties of program connectives can be expressed. The algorithmic logic (AL) first developed by Salwicki…
Originally appeared on Stanford Encyclopedia of Philosophy Read More
