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 BibTeX
Jens Palsberg, Mitchell Wand, Patrick O'Keefe: Type Inference with Non-Structural Subtyping. 49-67 BibTeX
M. J. A. Caswell: Equivalence of Formal Semantics Definition Methods. 68-77 BibTeX
Susumu Nishimura: A Strict Functional Language with Cyclic Recursive Data. 78-97 BibTeX
Stein Krogdahl, Olav Lysne: Verifying a Distributed List System: A Case History. 98-118 BibTeX

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

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

Colin O'Halloran, R. D. Arthan, D. King: Using a Formal Specification Contractually. 349-358 BibTeX
Charanjit S. Jutla, Josyula R. Rao: A Methodology for Designing Proof Rules for Fair Parallel Programs. 359-378 BibTeX
Ralf Kneuper: Limits of Formal Methods. 379-394 BibTeX
Mark B. Josephs, Andrew M. Bailey: The Use of SI-Algebra in the Design of Sequencer Circuits. 395-408 BibTeX
Ekkart Kindler, Wolfgang Reisig, Hagen Völzer, Rolf Walter: Petri Net Based Verification of Distributed Algorithms: An Example. 409-424 BibTeX
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 BibTeX

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