title: Functional Approach to Programming
author:  Guy Cousineau 
description: "...a valuable contribution to programming practice...Cousineau and Mauny convincingly demonstrate the elegance and conciseness of the functional approach." Computing Reviews
zlib_text: Certiﬁed Programming with Dependent Types
  Adam Chlipala
  March 8, 2016
  
  A print version of this book is available from the MIT Press. For more information, see
  the book’s home page:
  http://adam.chlipala.net/cpdt/
  Copyright Adam Chlipala 2008-2013, 2015.
  This work is licensed under a Creative Commons Attribution-Noncommercial-No
  Derivative Works 3.0 Unported License. The license text is available at:
  http://creativecommons.org/licenses/by-nc-nd/3.0/
  
  Contents
  1
  Introduction
  6
  1.1
  Whence This Book?
  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
  6
  1.2
  Why Coq? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
  8
  1.2.1
  Based on a Higher-Order Functional Programming Language . . . . .
  8
  1.2.2
  Dependent Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
  8
  1.2.3
  An Easy-to-Check Kernel Proof Language
  . . . . . . . . . . . . . . .
  9
  1.2.4
  Convenient Programmable Proof Automation
  . . . . . . . . . . . . .
  9
  1.2.5
  Proof by Reﬂection . . . . . . .