Imperative Functional Programming with Isabelle/HOL

This publication has 15 references indexed in Scilit:

• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
  2007
• A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
  Lecture Notes in Computer Science, 2007
• A machine-checked model for a Java-like language, virtual machine, and compiler
  ACM Transactions on Programming Languages and Systems, 2006
• Axiomatic Constructor Classes in Isabelle/HOLCF
  Lecture Notes in Computer Science, 2005
• A Verification Environment for Sequential Imperative Programs in Isabelle/HOL
  Lecture Notes in Computer Science, 2005
• An Extensible SAT-solver
  2004
• Verifying BDD Algorithms through Monadic Interpretation
  2002
• Single-Threaded Objects in ACL2
  2001
• HOLCF = HOL + LCF
  Journal of Functional Programming, 1999
• Lazy functional state threads
  ACM SIGPLAN Notices, 1994