Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)
<jats:p>Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2022
|
| Online Access: | https://hdl.handle.net/1721.1/142933 |
| _version_ | 1826218173561569280 |
|---|---|
| author | Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chlipala, Adam |
| author_sort | Chlipala, Adam |
| collection | MIT |
| description | <jats:p>Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.</jats:p> |
| first_indexed | 2024-09-23T17:15:38Z |
| format | Article |
| id | mit-1721.1/142933 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T17:15:38Z |
| publishDate | 2022 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1429332023-06-28T19:42:37Z Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory <jats:p>Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.</jats:p> 2022-06-10T15:56:04Z 2022-06-10T15:56:04Z 2021 2022-06-10T15:40:23Z Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/142933 Chlipala, Adam. 2021. "Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)." Proceedings of the ACM on Programming Languages, 5 (ICFP). en 10.1145/3473599 Proceedings of the ACM on Programming Languages Creative Commons Attribution-NoDerivatives 4.0 International https://creativecommons.org/licenses/by-nd/4.0/ application/pdf Association for Computing Machinery (ACM) ACM |
| spellingShingle | Chlipala, Adam Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title | Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title_full | Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title_fullStr | Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title_full_unstemmed | Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title_short | Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) |
| title_sort | skipping the binder bureaucracy with mixed embeddings in a semantics course functional pearl |
| url | https://hdl.handle.net/1721.1/142933 |
| work_keys_str_mv | AT chlipalaadam skippingthebinderbureaucracywithmixedembeddingsinasemanticscoursefunctionalpearl |