R. J. Back and J. Wright, Duality in specification languages: a lattice-theoretical approach, Acta Informatica, vol.27, issue.7, pp.583-625, 1990.
DOI : 10.1007/bf00259469

R. Back and W. Joakim-von, Refinement calculus-a systematic introduction. Undergraduate texts in computer science, 1999.

W. Edsger and . Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs. Commun, vol.18, pp.453-457, 1975.

R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer et al., The essence of higher-order concurrent separation logic, Proceedings of the 26th European Symposium on Programming Languages and Systems, vol.10201, pp.696-723, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01633133

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens, CakeML: A verified implementation of ML, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.179-191, 2014.

K. Mamouras, Synthesis of strategies using the hoare logic of angelic and demonic nondeterminism, Logical Methods in Computer Science, vol.12, issue.3, 2016.

Z. Manna and J. Mccarthy, Properties of programs and partial function logic, Machine Intelligence, vol.5, 1970.

M. O. Myreen, J. C. Michael, and . Gordon, Hoare logic for realistically modelled machine code, Tools and Algorithms for the Construction and Analysis of Systems, pp.568-582, 2007.
DOI : 10.1007/978-3-540-71209-1_44
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-71209-1_44.pdf

K. Nakata and T. Uustalu, A hoare logic for the coinductive trace-based big-step semantics of while, Programming Languages and Systems, pp.488-506, 2010.

H. Schorr and W. M. Waite, An efficient machine-independent procedure for garbage collection in various list structures, Communications of the ACM, vol.10, pp.501-506, 1967.