A Coq Library of Sets for Teaching Denotational Semantics
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_ | 1866916197715410944 |
|---|---|
| author | Cao, Qinxiang Wu, Xiwei Liang, Yalun |
| author_facet | Cao, Qinxiang Wu, Xiwei Liang, Yalun |
| contents | Sets and relations are very useful concepts for defining denotational semantics. In the Coq proof assistant, curried functions to Prop are used to represent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C -> Prop, etc. Further, the membership relation can be encoded by function applications, e.g. X a represents a in X if X: A -> Prop. This is very convenient for developing formal definitions and proofs for professional users, but it makes propositions more difficult to read for non-professional users, e.g. students of a program semantics course. We develop a small Coq library of sets and relations so that standard math notations can be used when teaching denotational semantics of simple imperative languages. This library is developed using Coq's type class system. It brings about zero proof-term overhead comparing with the existing formalization of sets. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_05459 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Coq Library of Sets for Teaching Denotational Semantics Cao, Qinxiang Wu, Xiwei Liang, Yalun Programming Languages Logic in Computer Science Sets and relations are very useful concepts for defining denotational semantics. In the Coq proof assistant, curried functions to Prop are used to represent sets and relations, e.g. A -> Prop, A -> B -> Prop, A -> B -> C -> Prop, etc. Further, the membership relation can be encoded by function applications, e.g. X a represents a in X if X: A -> Prop. This is very convenient for developing formal definitions and proofs for professional users, but it makes propositions more difficult to read for non-professional users, e.g. students of a program semantics course. We develop a small Coq library of sets and relations so that standard math notations can be used when teaching denotational semantics of simple imperative languages. This library is developed using Coq's type class system. It brings about zero proof-term overhead comparing with the existing formalization of sets. |
| title | A Coq Library of Sets for Teaching Denotational Semantics |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2404.05459 |