Date: Tue, 28 Nov 2006 13:45:38 -0600
From: Sol Swords

Hi all,

Tomorrow's ACL2 meeting will feature Konrad Slind from the University of 
Utah here to talk about formalizing functional programs in HOL.  The 
meeting is at the same time and place as usual, ACES 3.116 at 4:00 pm.  
Here is the abstract:

            FP in HOL

     I will give an overview of how functional programs are
     formalized in HOL, starting from ancient work and
     progressing to the current state of affairs. I will then
     discuss work-in-progress on a verifying compiler
     for a simple executable subset of higher order logic.