[isabelle] Operational semantics for functional languages in Isabelle/HOL
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Operational semantics for functional languages in Isabelle/HOL
- From: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Date: Thu, 16 Jun 2016 12:22:52 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0
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