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 |