Search

In this position paper, we present a prototype of a visualizer for functional programs. Such programs, whose evaluation model is the reduction of an expression to a value through repeated application of rewriting rules, and which tend to make little or no use of mutable state, are amenable to visualization in the same fashion as simple mathematical expressions, with which every schoolchild is familiar. We show how such visualizations may be produced for the strict functional language OCaml, by direct interpretation of the abstract syntax tree and appropriate pretty-printing. We describe (and begin to address) the challenges of presenting such program traces in limited space and of identifying their essential elements, so that our methods will one day be practical for more than toy programs. We consider the problems posed by the parts of modern functional programming which are not purely functional such as mutable state, input/output and exceptions. We describe initial work on the use of such visualizations to address the problem of program debugging, which is our ultimate aim.

This article appeared in Homeland Security Affairs (September 2011), v.7 no.2 "Former DHS Secretary Tom Ridge reminds us of the dangers of complacency and that 'ten years is enough time to know that in the next ten years, the fight will still be with us.' He also reminds us that as new threats surface our tools, policies and security strategies must continue to evolve. 'Because after taking fifty years to win the Cold War, while we emerged as the lone superpower, we were also left with a stockpile of weapons, tactics, and diplomatic relationships that were of little utility in the new security environment.'" Approved for public release; distribution is unlimited.

We, the organizers and participants, report our experiences from the 1st Veried Software Competition, held in August 2010 in Edinburgh at the VSTTE 2010 conference

We formalise and mechanise a construtive, proof theoretic proof of Craig's Interpolation Theorem in Isabelle/HOL. We give all the definitions and lemma statements both formally and informally. We also transcribe informally the formal proofs. We detail the main features of our mechanisation, such as the formalisation of binding for first order formulae. We also give some applications of Craig's Interpolation Theorem.