Logics of Programs : Workshop, Yorktown Heights, NY, USA

Logic design Logics and Meanings of Programs
Imprint: Springer
1982
1st ed. 1982.
EISBN 3540390472
Proof rules dealing with fairness.
Hoare's Logic is incomplete when it does not have to be.
The refinement of specifications and the stability of Hoare's Logic.
Toward a logical theory of program data.
Design and synthesis of synchronization skeletons using branching time temporal logic.
The type theory of PL/CV3.
Correctness of programs with function procedures.
A formalism for reasoning about fair termination.
Keeping a foot on the ground.
Further results on propositional dynamic logic of nonregular programs.
Some observations on compositional semantics.
Some connections between iterative programs, recursive programs, and first-order logic.
On induction vs. *-continuity.
Timesets.
Program logics and program verification.
Verification of concurrent programs: Temporal proof principles.
Synthesis of communicating processes from Temporal Logic specifications.
A note on equivalences among logics of programs.
The representation theorem for algorithmic algebras.
Nonstandard Dynamic Logic.
A critique of the foundations of Hoare-style programming logics.
Some applications of topology to program semantics.
Using graphs to understand PDL.
Critical remarks on max model of concurrency.
Transcript of panel discussion.
Hoare's Logic is incomplete when it does not have to be.
The refinement of specifications and the stability of Hoare's Logic.
Toward a logical theory of program data.
Design and synthesis of synchronization skeletons using branching time temporal logic.
The type theory of PL/CV3.
Correctness of programs with function procedures.
A formalism for reasoning about fair termination.
Keeping a foot on the ground.
Further results on propositional dynamic logic of nonregular programs.
Some observations on compositional semantics.
Some connections between iterative programs, recursive programs, and first-order logic.
On induction vs. *-continuity.
Timesets.
Program logics and program verification.
Verification of concurrent programs: Temporal proof principles.
Synthesis of communicating processes from Temporal Logic specifications.
A note on equivalences among logics of programs.
The representation theorem for algorithmic algebras.
Nonstandard Dynamic Logic.
A critique of the foundations of Hoare-style programming logics.
Some applications of topology to program semantics.
Using graphs to understand PDL.
Critical remarks on max model of concurrency.
Transcript of panel discussion.
