What is defunctionalization?

I recently gave a little demonstration entitled "What is Defunctionalization?" for UCSC TWIGS (the acronym, stolen from a similar seminar in the the U. Mass. math department, stands for The "What Is … ?" Graduate Seminar). The inspiration for this talk was just to present what I'd learned after Conor McBride's brilliant presentation at […]

Filed under: Haskell, Mathematics, Reading by Kenn
No Comments »

Debugging with Open Recursion Mixins

The call is out for submissions to the next issue of The Monad.Reader! To get an idea of the content (and because Don Stewart told us all to read every past issue) I cracked open Issue 10, which has a nice tutorial by B Pope on the GHCi debugger.

But having just finished a post using […]

Filed under: Haskell, Mathematics by Kenn
2 Comments »

CTL Model Checking in Haskell: A Classic Algorithm Explained as Memoization

As an exercise, since my reading group was discussing model checking this week, I implemented the classic model checker for CTL specifications from the 1986 paper

Automatic Verification of Concurrent Systems Using Temporal Logic Specifications by EM Clarke, EM Emerson, AP Sistla.

The "efficient algorithm" presented in the paper is, upon reflection, merely a memoized traversal of […]

Filed under: Haskell, Mathematics, Reading by Kenn
1 Comment »