@article(abadi-refinement,
 author       = {Mart\'in Abadi and Leslie Lamport},
 year         = {1991},
 title        = {The Existence of Refinement Mappings},
 journal      = {Journal of Theoretical Computer Science},
 volume       = {82},
 number       = {2},
 doi          = {10.1016/0304-3975(91)90224-P},
)
@book(abrial-b,
 author       = {Jean-Raymond Abrial},
 year         = {1996},
 title        = {The {B-Book}: Assigning Programs to Meanings},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9780511624162},
)
@misc(acl2-www,
 title        = {The {ACL2} Theorem Prover},
 howpublished = {\url{http://www.cs.utexas.edu/~moore/acl2}},
)
@book(andrews-logic,
 author       = {Peter B.\ Andrews},
 year         = {2002},
 title        = {An Introduction to Mathematical Logic and Type Theory: To Thruth Through Proof},
 publisher    = {Springer},
 doi          = {10.1007/978-94-015-9934-4},
)
@techreport(boyer-instantiation,
 author       = {R. S. Boyer and D. M. Goldschlag and M. Kaufmann and J S. Moore},
 year         = {1991},
 title        = {Functional Instantiation in First Order Logic},
 type         = {Technical Report},
 number       = {44},
 institution  = {Computational Logic Inc.},
)
@article(church-types,
 author       = {Alonzo Church},
 year         = {1940},
 title        = {A Formulation of the Simple Theory of Types},
 journal      = {The Journal of Symbolic Logic},
 volume       = {5},
 number       = {2},
 doi          = {10.2307/2266170},
)
@article(clarkson-hyperproperties,
 author       = {Michael Clarkson and Fred Schneider},
 year         = {2010},
 title        = {Hyperproperties},
 journal      = {Journal of Computer Security},
 volume       = {18},
 number       = {6},
 doi          = {10.3233/JCS-2009-0393},
)
@article(coglio-pop,
 author       = {Alessandro Coglio},
 year         = {2014},
 title        = {Pop-Refinement},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://afp.sf.net/entries/Pop_Refinement.shtml}, Formal proof development},
)
@article(dijkstra-constructive,
 author       = {Edsger W.\ Dijkstra},
 year         = {1968},
 title        = {A Constructive Approach to the Problem of Program Correctness},
 journal      = {BIT},
 volume       = {8},
 number       = {3},
 doi          = {10.1007/BF01933419},
)
@inproceedings(goguen-noninterference,
 author       = {Joseph Goguen and Jos\'{e} Meseguer},
 year         = {1982},
 title        = {Security Policies and Security Models},
 booktitle    = {Proc.\ {IEEE} Symposium on Security and Privacy},
 doi          = {10.1109/SP.1982.10014},
)
@inproceedings(greve-quantified,
 author       = {David Greve},
 year         = {2009},
 title        = {Automated Reasoning with Quantified Formulae},
 booktitle    = {Proc.\ 8th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2009})},
 doi          = {10.1145/1637837.1637855},
)
@article(hoare-data,
 author       = {C. A. R. Hoare},
 year         = {1972},
 title        = {Proof of Correctness of Data Representations},
 journal      = {Acta Informatica},
 volume       = {1},
 number       = {4},
 doi          = {10.1007/BF00289507},
)
@book(jones-vdm,
 author       = {Cliff Jones},
 year         = {1990},
 title        = {Systematic Software Development using {VDM}},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@inproceedings(joosten-reusing,
 author       = {Sebastiaan J. C. Joosten and Bernard van Gastel and Julien Schmaltz},
 year         = {2013},
 title        = {A Macro for Reusing Abstract Functions and Theorems},
 booktitle    = {Proc.\ 11th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2013})},
 doi          = {10.4204/EPTCS.114.3},
)
@(kaufmann-structured,
 author       = {Matt Kaufmann and J Strother Moore},
 year         = {2001},
 title        = {Structured Theory Development for a Mechanized Logic},
 doi          = {10.1023/A:1026517200045},
)
@(manolios-partial,
 author       = {Panagiotis Manolios and J Strother Moore},
 year         = {2003},
 title        = {Partial Functions in {ACL2}},
 doi          = {10.1023/B:JARS.0000009505.07087.34},
)
@inproceedings(mateos-multiset,
 author       = {Mart\`{\i}n-Mateos, F. J. and J. A. Alonso and M. J. Hidalgo and Ruiz-Reina, J. L.},
 year         = {2002},
 title        = {A Generic Instantiation Tool and a Case Study: A Generic Multiset Theory},
 booktitle    = {Proc.\ 3rd International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2002})},
)
@techreport(milner-simulation,
 author       = {Robin Milner},
 year         = {1971},
 title        = {An Algebraic Definition of Simulation between Programs},
 type         = {Technical Report},
 number       = {CS-205},
 institution  = {Stanford University},
)
@inproceedings(moore-instantiation,
 author       = {J Strother Moore},
 year         = {2009},
 title        = {Automatically Computing Functional Instantiations},
 booktitle    = {Proc.\ 8th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2009})},
 doi          = {10.1145/1637837.1637839},
)
@book(morgan-refinement,
 author       = {Carroll Morgan},
 year         = {1998},
 title        = {Programming from Specifications},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@inproceedings(smith-mechanizing,
 author       = {Douglas R.\ Smith},
 year         = {1999},
 title        = {Mechanizing the Development of Software},
 editor       = {Manfred Broy},
 booktitle    = {Calculational System Design, Proc.\ Marktoberdorf Summer School},
 publisher    = {IOS Press},
)
@book(spivey-z,
 author       = {J. M. Spivey},
 year         = {1992},
 title        = {The {Z} Notation: A Reference Manual},
 edition      = {second},
 publisher    = {Prentice Hall},
)
@inproceedings(swords-fty,
 author       = {Sol Swords and Jared Davis},
 year         = {2015},
 title        = {Fix Your Types},
 booktitle    = {Proc.\ 13th International Workshop on the {ACL2} Theorem Prover and Its Applications ({ACL2-2015})},
)