Coq http://coq.inria.fr/

1. Require supporting libraries.
   #+begin_src coq
     Require Import Bool.
     Require Import Arith.
     Require Import List.
   #+end_src

   #+RESULTS:
   : 

2. Simple function.
   #+begin_src coq
   (* Check if a list is sorted *)
   Fixpoint sortp (l : list nat) := match l with
       a :: b :: rst => if leb a b then sortp rst else false
     | a :: nil => true
     | nil => true
   end
   #+end_src

   #+RESULTS:
   : sortp is recursively defined (decreasing on 1st argument)
   : 

3. Run the above function.
   #+begin_src coq
     Eval compute in sortp (1::2::3::nil)
   #+end_src

   #+RESULTS:
   :      = true
   :      : bool
   :