@book(Bertot04,
 author       = "Yves Bertot and Pierre Cast\'eran",
 year         = "2004",
 title        = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
 series       = "Texts in Theoretical Computer Science",
 publisher    = "Springer Verlag",
 doi          = "10.1007/978-3-662-07964-5",
)
@book(Bird98,
 author       = "Richard Bird",
 year         = "1998",
 title        = "Introduction to Functional Programming using Haskell",
 edition      = "second",
 publisher    = "Prentice-Hall",
)
@article(Burstall69,
 author       = "R. M. Burstall",
 year         = "1969",
 title        = "Proving Properties of Programs by Structural Induction",
 journal      = "The Computer Journal",
 volume       = "12",
 number       = "1",
 pages        = "41--48",
 doi          = "10.1093/comjnl/12.1.41",
)
@unpublished(Chlipala13,
 author       = "Adam Chlipala",
 title        = "Certified Programming with Dependent Types",
 note         = "Feb. 12, 2013, availabe online {\tt {http://adam.chlipala.net/cpdt/}}",
)
@book(Cousineau95,
 author       = "Guy Couineau and Michel Mauny",
 year         = "1995",
 title        = "The Functional Approach to Programming",
 publisher    = "Cambridge University Press",
)
@book(Felleisen_design,
 author       = "Matthias Felleisen and Robert Bruce Findler and Matthew Flatt and Shriram Krishnamurthi",
 year         = "2001",
 title        = "How to design programs: an introduction to programming and computing",
 publisher    = "MIT Press",
 address      = "Cambridge, MA, USA",
)
@book(Gallier85,
 author       = "Jean H. Gallier",
 year         = "1985",
 title        = "Logic for computer science: foundations of automatic theorem proving",
 publisher    = "Harper \& Row Publishers, Inc.",
 address      = "New York, NY, USA",
)
@book(Hudak00,
 author       = "Paul Hudak",
 year         = "2000",
 title        = "The {H}askell School of Expression: Learning Functional Programming theough Multimedia",
 publisher    = "Cambridge University Press",
)
@book(Hutton07,
 author       = "Graham Hutton",
 year         = "2007",
 title        = "Programming in {H}askell",
 publisher    = "Cambridge University Press",
 doi          = "10.1017/CBO9780511813672",
)
@book(Lipovaca11,
 author       = "Miran Lipovaca",
 year         = "2011",
 title        = "Learn You a {H}askell for Great Good: A Beginner's Guide",
 publisher    = "No Starch Press",
)
@book(Mitchell96,
 author       = "John Mitchell",
 year         = "1996",
 title        = "Foundations for Programming Langauges",
 publisher    = "MIT Press",
)
@book(Nipkow02,
 author       = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
 year         = "2002",
 title        = "Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
 series       = "LNCS",
 volume       = "2283",
 publisher    = "Springer",
)
@book(paulson90,
 author       = "Lawrence C Paulson",
 year         = "1990",
 title        = "Logic and computation: interactive proof with Cambridge LCF",
 publisher    = "Cambridge University Press",
)
@book(Pierce02,
 author       = "Benjamin Pierce",
 year         = "2002",
 title        = "Types and Programming Langauges",
 publisher    = "MIT Press",
)
@book(Reade89,
 author       = "Chris Reade",
 year         = "1989",
 title        = "Elements of Functional Programming",
 publisher    = "Addison Wesley",
)
@article(Haskell98,
 author       = "et. al. Simon {Peyton Jones}",
 year         = "2003",
 title        = "The {Haskell} 98 Language and Libraries: The Revised Report",
 journal      = "Journal of Functional Programming",
 volume       = "13",
 number       = "1",
 pages        = "1--255",
)
@book(Thompson99,
 author       = "Simon Thompson",
 year         = "1999",
 title        = "Haskell: The Craft of Functional Programming",
 edition      = "second",
 publisher    = "Addison Wesley",
)
@book(Winskel93,
 author       = "Glynn Winskel",
 year         = "1993",
 title        = "The Formal Semantics of Programming Langauges: An Introduction",
 publisher    = "MIT Press",
)