### 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.

### License

BSD License

### Topics

- Computer science/Programming languages

### Session Decl_Sem_Fun_PL

- Lambda
- SmallStepLam
- BigStepLam
- ValuesFSet
- ValuesFSetProps
- RelationalSemFSet
- DeclSemAsDenotFSet
- EquivRelationalDenotFSet
- ChangeEnv
- DeclSemAsNDInterpFSet
- InterTypeSystem
- Values
- ValueProps
- DeclSemAsDenot
- DenotLam5
- EquivDenotInterTypes
- DenotSoundFSet
- DenotCompleteFSet
- DenotCongruenceFSet
- DenotEqualitiesFSet
- Optimizer
- SystemF
- MutableRef
- MutableRefProps

## Cite

×

Decl_Sem_Fun_PL-AFP

    @article{Decl_Sem_Fun_PL-AFP,
      author  = {Jeremy Siek},
      title   = {Declarative Semantics for Functional Languages},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Decl_Sem_Fun_PL.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jul 24, 2017 : Isabelle2016-1