@inproceedings(drjava,
 author       = "Eric Allen and Robert Cartwright and Brian Stoler",
 year         = "2002",
 title        = "DrJava: a lightweight pedagogic environment for Java",
 booktitle    = "Proceedings of the 33rd SIGCSE technical symposium on Computer science education",
 series       = "SIGCSE '02",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "137--141",
 doi          = "10.1145/563340.563395",
)
@inproceedings(acl2s-testing,
 author       = "Harsh Raju Chamarthi and Peter C. Dillinger and Matt Kaufmann and Panagiotis Manolios",
 year         = "2011",
 title        = "Integrating Testing and Interactive Theorem Proving",
 editor       = "David Hardin and Julien Schmaltz",
 booktitle    = "{\rm Proceedings 10th International Workshop} on the ACL2 Theorem Prover and its Applications, {\rm Austin, Texas, USA, November 3-4, 2011}",
 series       = "Electronic Proceedings in Theoretical Computer Science",
 volume       = "70",
 publisher    = "Open Publishing Association",
 pages        = "4--19",
 doi          = "10.4204/EPTCS.70.1",
)
@inproceedings(acl2s,
 author       = "Peter C. Dillinger and Panagiotis Manolios and Daron Vroon and J. Strother Moore",
 year         = "2007",
 title        = "{ACL2s}: ``{T}he {ACL2} {S}edan''",
 booktitle    = "Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)",
 series       = "Electronic Notes in Theoretical Computer Science",
 volume       = "174",
 pages        = "3 -- 18",
 doi          = "10.1016/j.entcs.2006.09.018",
)
@article(modular-acl2,
 author       = "C. Eastlund and M. Felleisen",
 year         = "2009",
 title        = "Toward a practical module system for ACL2",
 journal      = "Practical Aspects of Declarative Languages",
 pages        = "46--60",
 doi          = "10.1007/978-3-540-92995-6\_4",
)
@inproceedings(doublecheck,
 author       = "Carl Eastlund",
 year         = "2009",
 title        = "{DoubleCheck} your theorems",
 booktitle    = "Proceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications",
 series       = "ACL2 '09",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "42--46",
 doi          = "10.1145/1637837.1637844",
)
@inproceedings(eastlund-acl2,
 author       = "Carl Eastlund and Dale Vaillancourt and Matthias Felleisen",
 year         = "2007",
 title        = "{ACL2} for Freshmen: First Experiences",
 booktitle    = "ACL2 ’07: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications",
 publisher    = "ACM Press",
 pages        = "200–--211",
)
@incollection(drracket,
 author       = "Robert Findler and Cormac Flanagan and Matthew Flatt and Shriram Krishnamurthi and Matthias Felleisen",
 year         = "1997",
 title        = "Dr{S}cheme: A pedagogic programming environment for scheme",
 editor       = "Hugh Glaser and Pieter Hartel and Herbert Kuchen",
 booktitle    = "Programming Languages: Implementations, Logics, and Programs",
 series       = "Lecture Notes in Computer Science",
 volume       = "1292",
 publisher    = "Springer Berlin / Heidelberg",
 pages        = "369--388",
 doi          = "10.1007/BFb0033856",
)
@book(car,
 author       = "Matt Kaufmann and J. Strother Moore and Panagiotis Manolios",
 year         = "2000",
 title        = "Computer-Aided Reasoning: An Approach",
 publisher    = "Kluwer Academic Publishers",
 address      = "Norwell, MA, USA",
 doi          = "10.1007/978-1-4615-4449-4",
)
@article(page-se,
 author       = "Rex Page",
 year         = "2007",
 title        = "Engineering Software Correctness",
 journal      = "Journal of Functional Programming",
 volume       = "17",
 pages        = "675--686",
 doi          = "10.1017/S095679680700634X",
)
@inproceedings(page-proptest,
 author       = "Rex Page",
 year         = "2011",
 title        = "Property-Based Testing and Verification: a Catalog of Classroom Examples",
 booktitle    = "Proceedings of the 2011 Symposium on Implemenation and Application of Functional Languages",
 address      = "Lawrence, KS",
 pages        = "134--147",
 doi          = "10.1007/978-3-642-34407-7\_9",
)
@inproceedings(hcw,
 author       = "Rex Page and Ruben Gamboa",
 year         = "2012",
 title        = "How Computers Work: Computational Thinking for Everyone",
 booktitle    = "Proceedings of the First International Workshop on Trends in Functional Programming in Education",
 address      = "St Andrews, UK",
 doi          = "10.4204/EPTCS.106.1",
)
@inproceedings(dracula,
 author       = "Dale Vaillancourt and Rex Page and Matthias Felleisen",
 year         = "2006",
 title        = "{ACL2} in {D}r{S}cheme",
 booktitle    = "Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications",
 series       = "ACL2 '06",
 publisher    = "ACM",
 address      = "New York, NY, USA",
 pages        = "107--116",
 doi          = "10.1145/1217975.1217999",
)
@article(subjects,
 author       = "R.A. Virzi",
 year         = "1992",
 title        = "Refining the test phase of usability evaluation: How many subjects is enough?",
 journal      = "Human Factors: The Journal of the Human Factors and Ergonomics Society",
 volume       = "34",
 number       = "4",
 pages        = "457--468",
)