Email Gateway (Aug 22 2022 at 15:48): Email Gateway (Aug 22 2022 at 15:48):From: Tobias Nipkow <nipkow@in.tum.de>
Declarative Semantics for Functional Languages
Jeremy Siek
We present a semantics for an applied call-by-value lambda-calculus that is
compositional, extensional, and elementary. We present four different views of
the semantics: 1) as a relational (big-step) semantics that is not operational
but instead declarative, 2) as a denotational semantics that does not use domain
theory, 3) as a non-deterministic interpreter, and 4) as a variant of the
intersection type systems of the Torino group. We prove that the semantics is
correct by showing that it is sound and complete with respect to operational
semantics on programs and that is sound with respect to contextual equivalence.
We have not yet investigated whether it is fully abstract. We demonstrate that
this approach to semantics is useful with three case studies. First, we use the
semantics to prove correctness of a compiler optimization that inlines function
application. Second, we adapt the semantics to the polymorphic lambda-calculus
extended with general recursion and prove semantic type soundness. Third, we
adapt the semantics to the call-by-value lambda-calculus with mutable references.
The paper that accompanies these Isabelle theories is available on arXiv at
https://arxiv.org/abs/1707.03762
https://www.isa-afp.org/entries/Decl_Sem_Fun_PL.shtml
Thanks Jeremy!
smime.p7s
Last updated: Apr 26 2024 at 01:06 UTC