« Theorem Proving for Verification | Main | Galois Open House »

Pretty-Printing a Really Long Formula (or, "What a Mathematician Could Learn from Haskell")

The next Galois Tech Talk will be Tuesday September 9th, 10.30am, with Lee Pike, talking about how to visually present proofs and formal notation.(.pdf slides):What Mathematicians can learn from HaskellAbstract

To the typical engineer or evaluator, mathematics can be scary, logic can be scarier, and really long specifications can simply be overwhelming. This talk is about the problem of the visual presentation of formal specifications clearly and concisely. We take as our initial inspiration Leslie Lamport's brief papers, "How to Write a Long Formula" and "How to Write a Proof" in which he proposes methods for writing the long and tedious formulas and proofs that appear in formal specification and verification.I will describe the problem and present one particular solution, as implemented in a simple pretty-printer I've written (in Haskell), that uses indentation and labels to more easily visually parse long formulas. Ultimately, I propose a "HOL Normal Form" for presenting specifications, much like BNF is used for presenting language definitions.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free.

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.

My response is on my own website »
Author Email (optional):
Author URL (optional):
Some HTML allowed: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <code> <em> <i> <strike> <strong>