|
Declarative
Semantics
for
Functional
Languages
Title: |
Declarative Semantics for Functional Languages |
Author:
|
Jeremy Siek
|
Submission date: |
2017-07-21 |
Abstract: |
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. |
BibTeX: |
@article{Decl_Sem_Fun_PL-AFP,
author = {Jeremy Siek},
title = {Declarative Semantics for Functional Languages},
journal = {Archive of Formal Proofs},
month = jul,
year = 2017,
note = {\url{http://isa-afp.org/entries/Decl_Sem_Fun_PL.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|