Edinburgh Day One
Achieved:
To Do:
Plan for Tomorrow:
- 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