@article{Lammich_2017,
    doi = {10.1007/s10817-017-9437-1},
    url = {https://doi.org/10.1007%2Fs10817-017-9437-1},
    year = {2017},
    month = {oct},
    publisher = {Springer Science and Business Media {LLC}},
    volume = {62},
    number = {4},
    pages = {481--503},
    author = {Peter Lammich},
    title = {Refinement to Imperative {HOL}},
    journal = {Journal of Automated Reasoning}
}

@article{Lammich_2017, doi = {10.1007/s10817-017-9437-1}, url = {https://doi.org/10.1007%2Fs10817-017-9437-1}, year = {2017}, month = {oct}, publisher = {Springer Science and Business Media {LLC}}, volume = {62}, number = {4}, pages = {481--503}, author = {Peter Lammich}, title = {Refinement to Imperative {HOL}}, journal = {Journal of Automated Reasoning} }