[isabelle] Operational semantics for functional languages in Isabelle/HOL

Hi list,

I am looking for formalisations of (pure) functional languages in Isabelle/HOL (with syntax and an operational semantics). They should support pattern matching and higher-order functions. I'd like to use them to assign run-time bounds to programs written in these languages and to connect these programs semantically to functions written in HOL.

I know of the formalisation by Simon Wimmer, the ongoing work of Lars Hupel and Joachim Breitner's formalisation of Sestoft's semantics for call-by-name. What others are out there that might be useful?

Thanks in advance for any pointers,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.