@misc(acl2:doc,
 author       = {{ACL2 Community}},
 year         = {accessed December, 2016},
 title        = {{ACL2+Books} Documentation},
 note         = {See URL \url{http://www.cs.utexas.edu/~moore/acl2/manuals/current/manual?topic=ACL2____ACL2}},
)
@book(DBLP:books/daglib/0096998,
 author       = {Richard S. Bird and Oege de Moor},
 year         = {1997},
 title        = {Algebra of programming},
 series       = {Prentice Hall International series in computer science},
 publisher    = {Prentice Hall},
)
@article(DBLP:journals/ibmsj/Bresenham65,
 author       = {Jack Bresenham},
 year         = {1965},
 title        = {Algorithm for Computer Control of a Digital Plotter},
 journal      = {{IBM} Systems Journal},
 volume       = {4},
 number       = {1},
 pages        = {25--30},
 doi          = {10.1147/sj.41.0025},
)
@inproceedings(soft-2015,
 author       = {Alessandro Coglio},
 year         = {2015},
 title        = {Second-Order Functions and Theorems in {ACL2}},
 booktitle    = {Proceedings of the Thirteenth International Workshop on the {ACL2} Theorem Prover and its Applications},
 doi          = {10.1145/1637837.1637839},
)
@misc(apt-web,
 author       = {{Kestrel Institute} and {University of Texas at Austin}},
 year         = {accessed January, 2017},
 title        = {{APT} ({Automated Program Transformations})},
 howpublished = {\url{http://www.kestrel.edu/home/projects/apt}},
)
@inproceedings(simplify-defun-2003,
 author       = {{Matt Kaufmann}},
 year         = {2003},
 title        = {{A Tool for Simplifying Files of {ACL2} Definitions}},
 booktitle    = {Proceedings of the Fourth International Workshop on the {ACL2} Theorem Prover and its Applications, {ACL2} 2003, Boulder, Colorado, USA, July 13-14, 2003.},
)
@article(DBLP:journals/tse/Smith90,
 author       = {Douglas R. Smith},
 year         = {1990},
 title        = {{KIDS:} {A} Semiautomatic Program Development System},
 journal      = {{IEEE} Trans. Software Eng.},
 volume       = {16},
 number       = {9},
 pages        = {1024--1043},
 doi          = {10.1109/32.58788},
)
@phdthesis(smith-axe,
 author       = {Eric W.\ Smith},
 year         = {2011},
 title        = {{Axe}: An Automated Formal Equivalence Checking Tool for Programs},
 type         = {{Ph.D.} dissertation},
 school       = {Stanford University},
)