Abstracting Denotational Interpreters
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866907976406663168 |
|---|---|
| author | Graf, Sebastian Jones, Simon Peyton Keidel, Sven |
| author_facet | Graf, Sebastian Jones, Simon Peyton Keidel, Sven |
| contents | We explore denotational interpreters: denotational semantics that produce coinductive traces of a corresponding small-step operational semantics. By parameterising our denotational interpreter over the semantic domain and then varying it, we recover dynamic semantics with different evaluation strategies as well as summary-based static analyses such as type analysis, all from the same generic interpreter. Among our contributions is the first denotational semantics for call-by-need that is provably adequate in a strong, compositional sense. The generated traces lend themselves well to describe operational properties such as how often a variable is evaluated, and hence enable static analyses abstracting these operational properties. Since static analysis and dynamic semantics share the same generic interpreter definition, soundness proofs via abstract interpretation decompose into showing small abstraction laws about the abstract domain, thus obviating complicated ad-hoc preservation-style proof frameworks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_02778 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Abstracting Denotational Interpreters Graf, Sebastian Jones, Simon Peyton Keidel, Sven Programming Languages We explore denotational interpreters: denotational semantics that produce coinductive traces of a corresponding small-step operational semantics. By parameterising our denotational interpreter over the semantic domain and then varying it, we recover dynamic semantics with different evaluation strategies as well as summary-based static analyses such as type analysis, all from the same generic interpreter. Among our contributions is the first denotational semantics for call-by-need that is provably adequate in a strong, compositional sense. The generated traces lend themselves well to describe operational properties such as how often a variable is evaluated, and hence enable static analyses abstracting these operational properties. Since static analysis and dynamic semantics share the same generic interpreter definition, soundness proofs via abstract interpretation decompose into showing small abstraction laws about the abstract domain, thus obviating complicated ad-hoc preservation-style proof frameworks. |
| title | Abstracting Denotational Interpreters |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2403.02778 |