I'll be practicing my talk for PPDP (Principles and Practice of Declarative Programming) in Portugal: Making Induction Manifest in Modular ACL2. The talk has a 25-minute slot, but as always with comments and whatnot the process will probably last one-and-a-half to two hours. Carl Eastlund