.

 Timestamp List of topics from the day that you feel comfortable with: List of topics from the day that you don't quite feel comfortable with: Things it would have been better to leave out: Things you would like to have seen included that weren't: Overall assessment of the day:

.

 5/14/2008 15:28:25 doing I/O, the use of append and break-at the use of the functions fro the crypto project ok+

.

 5/14/2008 15:39:16 File I/O
defthm and the need for supporting lemmas

acl2
let needed to be discussed more, especially the understanding of let*
cond
 A book, reference for acl2 theorem proving or more of an introduction to how acl2 proves theorems and deals with errors.
Even when some theorems seemed easy to prove the addition of extra predicate logic so that the predicate was exactly what you needed.
Example: proving that a list you created using endp when defining a predicate list and not being able to prove that it was a true list without using consp. 		ok+

.

 5/14/2008 15:40:51 The feeling of utter ineptitude that surrounded me yesterday is gone :) I was able to write the Crypto part 2 program without assistance. Proving it is a different story. GUI stuff and state handling. Convincing ACL2 that my solution is correct. Today went well. Nothing to leave out. nil ok+

.

 5/14/2008 15:43:40 file io
GUI
defthm 		develop theorems ok+

.

 5/14/2008 16:02:29 rewrite rules file i/o, teachpacks I wouldn't really leave it out, but ACL2 has such a steep learning curve, I'm afraid it's too ambitious to tackle it in a three-day workshop more information on the primitives ok+

.

 5/14/2008 16:02:37 project of crypto .. .mainly because of learning acl2 not an issue of the program NA as I am currently not instructing a class No comment ok+

.

 5/14/2008 16:03:49 Using ACL2 to state and prove theorems about Scheme programs Still not very good with the sceme interfase but getting better. ok+

.

 5/15/2008 6:57:09 GUI proofing error messages
DrACuLA/Scheme/ACL2/teachpacks/etc divisions (what is what) 		file i/o larger GUI exercise ok

.

 5/15/2008 7:07:13 applicative scheme programming, defproperty, defthm, tail recursion GUI and graphics in ACL2 ok+