A Lattice-theoretical Basis for a Specification Language. - Ralph-Johan Back; Joakim von Wright (MPC, 1989)

Refinement Calculus, Part I: Sequential Nondeterministic Programs. - Ralph-Johan Back; Joakim von Wright (REX Workshop, 1989)

Refinement Concepts Formalized in Higher Order Logic. - Ralph-Johan Back; Joakim von Wright (Programming Concepts and Methods, 1990)

Duality in Specification Languages: A Lattice-Theoretical Approach. - Ralph-Johan Back; Joakim von Wright (Acta Informatica, 1990)

Refinement Concepts Formalised in Higher Order Logic. - Ralph-Johan Back; Joakim von Wright (Formal Aspects Comput., 1990)

Mechanising the Temporal Logic of Actions in HOL. - Joakim von Wright (TPHOLs, 1991)

Program Transformations and Refinements in HOL. - Joakim von Wright; Kaisa Sere (TPHOLs, 1991)

Program Inversion in the Refinement Calculus. - Joakim von Wright (Inf. Process. Lett., 1991)

Using a Theorem Prover for Reasoning about Concurrent Algorithms. - Joakim von Wright; Thomas Långbacka (CAV, 1992)

Predicate Transformers and Higher Order Logic. - Ralph-Johan Back; Joakim von Wright (REX Workshop, 1992)

Mechanising some Advanced Refinement Concepts. - Joakim von Wright; Jukka Hekanaho; P. Luostarinen; Thomas Långbacka (TPHOLs, 1992)

Combining Angles, Demons and Miracles in Program Specifications. - Ralph-Johan Back; Joakim von Wright (Theor. Comput. Sci., 1992)

Mechanizing Some Advanced Refinement Concepts. - Joakim von Wright; Jukka Hekanaho; P. Luostarinen; Thomas Långbacka (Formal Methods Syst. Des., 1993)

Statement Inversion and Strongest Postcondition. - Ralph-Johan Back; Joakim von Wright (Sci. Comput. Program., 1993)

Trace Refinement of Action Systems. - Ralph-Johan Back; Joakim von Wright (CONCUR, 1994)

Program Refinement by Theorem Prover. - Joakim von Wright (Refine, 1994)

The Lattice of Data Refinement. - Joakim von Wright (Acta Informatica, 1994)

TkWinHOL: A Tool for Window Inference in HOL. - Thomas Långbacka; Rimvydas Ruksenas; Joakim von Wright (TPHOLs, 1995)

Representing Higher-Order Logic Proofs in HOL. - Joakim von Wright (Comput. J., 1995)

Games and Winning Strategies. - Ralph-Johan Back; Joakim von Wright (Inf. Process. Lett., 1995)

Refining Reactive Systems in HOL Using Action Systems. - Thomas Långbacka; Joakim von Wright (TPHOLs, 1997)

Contracts, games and refinement. - Ralph-Johan Back; Joakim von Wright (EXPRESS, 1997)

Structured Calculational Proof. - Ralph-Johan Back; Jim Grundy; Joakim von Wright (Formal Aspects Comput., 1997)

Refinement Calculus - A Systematic Introduction. - Ralph-Johan Back; Joakim von Wright (Springer, 1998)

Proving Isomorphism of First-Order Logic Proof Systems in HOL. - Anna Mikhajlova; Joakim von Wright (TPHOLs, 1998)

A Tool for Data Refinement. - Rimvydas Ruksenas; Joakim von Wright (TPHOLs, 1998)

Extending Window Inference. - Joakim von Wright (TPHOLs, 1998)

Reasoning About Interactive Systems. - Ralph-Johan Back; Anna Mikhajlova; Joakim von Wright (World Congress on Formal Methods, 1999)

Reasoning Algebraically about Loops. - Ralph-Johan Back; Joakim von Wright (Acta Informatica, 1999)

Distance tutorials in a systems design course. - Joakim von Wright (ITiCSE, 2000)

Functional Procedures in Higher-Order Logic. - Linas Laibinis; Joakim von Wright (TPHOLs, 2000)

Class Refinement as Semantics of Correct Object Substitutability. - Ralph-Johan Back; Anna Mikhajlova; Joakim von Wright (Formal Aspects Comput., 2000)

Encoding, Decoding and Data Refinement. - Ralph-Johan Back; Joakim von Wright (Formal Aspects Comput., 2000)

Theorem Prover Support for Precondition and Correctness Calculation. - Orieta Celiku; Joakim von Wright (ICFEM, 2002)

From Kleene Algebra to Refinement Algebra. - Joakim von Wright (MPC, 2002)

Preface. - John Derrick; Eerke A. Boiten; Jim Woodcock 001; Joakim von Wright (Refine, 2002)

Implementing Angelic Nondeterminism. - Orieta Celiku; Joakim von Wright (APSEC, 2003)

Compositional Action System Refinement. - Ralph-Johan Back; Joakim von Wright (Formal Aspects Comput., 2003)

Towards a refinement algebra. - Joakim von Wright (Sci. Comput. Program., 2004)

Refinement Algebra with Operators for Enabledness and Termination. - Kim Solin; Joakim von Wright (MPC, 2006)

Enabledness and termination in refinement algebra. - Kim Solin; Joakim von Wright (Sci. Comput. Program., 2009)