
.	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/13/2008 15:37:36	go over the slides and working with lab helped a lot with assistance first time working with ACL2 so the experience found in the class helped a lot				ok+
.	5/13/2008 15:38:43	Function definitions in ACL2, basic DrACuLa usage, basic doublecheck usage	fancier doublecheck usage	The discussion of The Method may have been premature. I think we were rushed heading into the testing, and I believe that a good foundation on the testing is important before trying out The Method.	More information on using doublecheck would be nice!	ok+
.	5/13/2008 15:39:05	BASIC LISP (which is a new language for me), Defining functions, solving simple problems in the language	Using defproperty and defthm to have doublecheck verify my solutions. I feel comfortable writing theorems using defthm, but I was unable to get my program to certify.	This is all valuable! Some may say the time we spent fighting to get the variance demo to work could have been used better, but watching you work with dracula helped me a lot.	I'm still looking forward to that fibonacci demo :)	ok+
.	5/13/2008 15:39:59	Definition of functions use of car, cdr, if function, nthcdr, list, append	theorems: how to write them and test them			ok+
.	5/13/2008 15:42:09	writing functions in Applicative common lisp	defproperty and defthm	so many choices for problems to do during lab time. So the problem worked in presentation, was the same as the one worked in lab.		ok
.	5/13/2008 15:44:13	ACL2 programs The theory of testing and verification	I am very tentative with the DrScheme interfaces with testing and verification.			ok+
.	5/13/2008 15:44:27	writing Scheme functions	predicate based testing, theorem proving. I get the idea but didn't finish the exercises.		focused documentation -- that is, syntax,semantics, and examples of important relevant constructs all in one document.	ok+
.	5/13/2008 15:57:59	most everything	driving DrScheme	nothing I can think of	one complete example to follow, .scm or .lisp files to download for either the examples from slides or another example (such as min/max)	ok+
.	5/13/2008 16:06:06	define functions test the functions define theorems for proofs	N/A	N/A	N/A	ok+
.	5/13/2008 16:27:31	ACL2 Double Check Random Testing Lemmas	Hints		More examples of basic theorems and building to a final theorems. Simpler.	ok+