Edinburgh Day One

[purplecat]

Achieved:

• Volunteered to give a Dream Talk on Friday


• Printed out and read my papers on Program Slicing which I said I'd talk about in the Dream Talk


• Long talk with LD about proof specification languages and control rules. Sent him draft paper on control rules by myself MJa and MP.

To Do:

• Write an abstract to go with the title for my Dream Talk, decide what I'm going to say and prepare a handout.


• Try and find the beginnings of a Note JG and I started writing on proof specification languages and recall what we were thinking and how it relates to LD's work.


• Talk to LD about Induction Challenge Problems - in particular their specification in TPTP Typed Higher-Order Form.


• Implement at least one proof critic for program correctness in IsaPlanner.


• Talk to DA about implementing program slicing in ProofGeneral.

Plan for Tomorrow:

• AM: Work with MJo on writing proof critics in IsaPlanner.


• PM: Prepare Dream Talk


• Evening: Write more gibberish in my blog