StrategoMetaTheory

Berenike, Bernadette, and Isabelle are all doing great. I tend to put photos of my kids online when they get born, and then never again, which I admit is strange; see here and here. (There are only two links because B&B are twins.) I guess we have just so many photos of them that we don’t know which of them to put online. Also, Berenike and Bernadette are turning 9 next year, and they start to get embarrassed by their parents’ actions. Shooting and publishing photos may fail to see their approval. I missed the short window of doing so. Isabelle who turns 3 next year is a fast learner and great imitator; she is even less permissive than her big sisters.

Speaking of Isabelle and “approval”, I have uploaded a new paper (draft) to my website. It uses Isabelle/HOL to develop a sort of metatheory for traversal strategies. It is my first project on theorem proving. (I am sane enough not to count type-class-based programming in Haskell as theorem proving.) (Also, don’t get confused with the URL’s ending, “isabelle2”. There is really just one Isabelle/HOL paper so far. The URL helps me to avoid confusion with my youngest daughter’s photo directory, even though it is on a different host.) This is joint work with Markus Kaiser, a Mathematician, who has worked on theorem proving for some time (mostly in the context of cryptology) before he joined the SLE team in Koblenz.

This paper has just been submitted. Hence feedback, if any, is appreciated, and will be considered. The actual code distribution is still a bit of a mess, as of writing, but it will be fine, if the paper’s web site says so – soon, hopefully.

 

Regards,

Ralf

 

Title: A Formal Model of Traversal Strategies

Authors: Markus Kaiser and Ralf Lämmel

URL: https://www.uni-koblenz.de/~laemmel/isabelle2/

Abstract: There is an observable increase in interest in traversal expressiveness in programming: there are new rewriting languages, programming-language extensions, and combinator libraries that enable programmers to design and deploy traversals over structured data. Such traversal programs can go wrong in new ways. For instance, a traversal may suddenly fail or diverge. It is important to gain better understanding of properties of traversal programs so that programmers make more knowledgeable choices of traversal schemes, and programming environments may provide improved documentation, targeted checks, and other support. This paper presents a machine-checked, Isabelle/HOL-based, formal model of traversal strategies. Amongst others, the model provides sufficient conditions for traversal programs not to fail and not to diverge. The model with its mechanized proofs makes systematic use of Isabelle/HOL's various capabilities for dealing with recursion or induction.