Category Reading

What is defunctionalization?

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 […]

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 […]