Formal Aspects of Computing, Volume 9

Volume 9, Number 1, 1997

Marc Bezem, Roland N. Bol, Jan Friso Groote: Formalizing Process Algebraic Verifications in the Calculus of Constructions. 1-48
Jens Palsberg, Mitchell Wand, Patrick O'Keefe: Type Inference with Non-Structural Subtyping. 49-67
M. J. A. Caswell: Equivalence of Formal Semantics Definition Methods. 68-77
Susumu Nishimura: A Strict Functional Language with Cyclic Recursive Data. 78-97
Stein Krogdahl, Olav Lysne: Verifying a Distributed List System: A Case History. 98-118

Maciej Koutny, Luigi V. Mancini, Giuseppe Pappalardo: Two Implementation Relations and the Correctness of Communicating Replicated Processes. 119-148
Qiwen Xu, Willem P. de Roever, Jifeng He: The Rely-Guarantee Method for Verifying Shared Variable Concurrent Programs. 149-174
Colin J. Fidge, Andy J. Wellings: An Action-Based Formal Model for Concurrent Real-Time Systems. 175-207
Wim H. Hesselink: A Mechanical Proof of Segall's PIF Algorithm. 208-226

Donald Sannella, Andrzej Tarlecki: Essential Concepts of Algebraic Specification and Program Development. 229-269
Rutger M. Dijkstra, Beverly A. Sanders: A Predicate Transformer for the Progress Property `To-Always'. 270-282
Michael R. Hansen, Zhou Chaochen: Duration Calculus: Logical Foundations. 283-330
Brian J. Ross: Running Programs Backwards: The Logical Inversion of Imperative Computation. 331-348

Colin O'Halloran, R. D. Arthan, D. King: Using a Formal Specification Contractually. 349-358
Charanjit S. Jutla, Josyula R. Rao: A Methodology for Designing Proof Rules for Fair Parallel Programs. 359-378
Ralf Kneuper: Limits of Formal Methods. 379-394
Mark B. Josephs, Andrew M. Bailey: The Use of SI-Algebra in the Design of Sequencer Circuits. 395-408
Ekkart Kindler, Wolfgang Reisig, Hagen Völzer, Rolf Walter: Petri Net Based Verification of Distributed Algorithms: An Example. 409-424
Christel Baier, Mila E. Majster-Cederbaum: The Connection Between Initial and Unique Solutions of Domain Equations in the Partial Order and Metric Approach. 425-445

Wim H. Hesselink: Theories for Mechanical Proofs of Imperative Programs. 448-468
Ralph-Johan Back, Jim Grundy, Joakim von Wright: Structured Calculational Proof. 469-483
Catherine Parent-Vigouroux: Verifying Programs in the Calculus of Inductive Constructions. 484-517
Peter M. W. Knijnenburg, Joost N. Kok: The Semantics of the Combination of Atomized Statements and Parallel Choice. 518-536
John O'Leary, Geoffrey Brown, Wayne Luk: Verified Compilation of Communicating Processes into Clocked Circuits. 537-559