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

Comments

[bunn.livejournal.com]

This posting is rendered more than usually baffling by the password on the Dream Talk link :-D It sounds vaguely Australian Aborigine... :-P

[purplecat]

The group I'm associated with in Edinburgh is prosaically referred to as the MRG (Mathematical Reasoning Group) but when feeling more fanciful we get referred to as the DReaM group (Discovery and Reasoning in Mathematics).

The Dream talk is a weekly hour-and-a-half work in progress talk, in which the use of slides and projection equipment is frowned upon (but handouts are tolerated) and audience participation is encouraged. AB also has a gong which, at least when I was a regular member of the group, he used to sound just before the Dream talk thus removing the perennial excuse that you were involved in something and had therefore forgotten that the talk was taking place.

[king-pellinor.livejournal.com]

I like the way that you're going to do a title and an abstract before you've decided what you're going to say :-)

And that you're going to decide what to say and prepare a handout on it before you try to remember anything about the subject :-D

[purplecat]

You mean most people don't prepare talks like this?

I now have a title and abstract:

Program Slicing for Proof Theories

Program Slicing is a technique used in automated debugging to narrow the search for a bug to one portion of the code base. In this Dream talk I intend to look at ways that proof can be used to perform program slicing. Leading on from that I'll also discuss how programs can be patched by removing faulty slices and then performing synthesis proofs to produce a correct slice.

[king-pellinor.livejournal.com]

Well, I'd normally at least hope to do it in largely the reverse order :-)

Although the last talk I gave consisted of someone else doing a load of slides, which I then stood in front of (and occasionally referred to) while I delivered a lively and amusing discourse on tax, how to account for it, and why HMRC thinks each member of my audience is a liar.