Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Operational semantics for functional languages...

Email Gateway (Aug 22 2022 at 13:37):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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,
Andreas

Last updated: Apr 25 2024 at 01:08 UTC