Contextual Refinement Types ...
We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, which provide fine-grained classification for the structures of contexts and binders. Refinement schemas are helpful in co...
| Main Authors: | , |
|---|---|
| Format: | Text |
| Language: | unknown |
| Published: |
arXiv
2023
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.48550/arxiv.2311.10577 https://arxiv.org/abs/2311.10577 |
| id |
ftdatacite:10.48550/arxiv.2311.10577 |
|---|---|
| record_format |
openpolar |
| spelling |
ftdatacite:10.48550/arxiv.2311.10577 2023-12-31T10:05:17+01:00 Contextual Refinement Types ... Gaulin, Antoine Pientka, Brigitte 2023 https://dx.doi.org/10.48550/arxiv.2311.10577 https://arxiv.org/abs/2311.10577 unknown arXiv https://dx.doi.org/10.4204/eptcs.396.2 Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 Programming Languages cs.PL FOS Computer and information sciences D.3.1; F.3.1 ScholarlyArticle Text article-journal Article 2023 ftdatacite https://doi.org/10.48550/arxiv.2311.1057710.4204/eptcs.396.2 2023-12-01T11:20:58Z We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, which provide fine-grained classification for the structures of contexts and binders. Refinement schemas are helpful in concisely representing certain proofs that rely on relations between contexts. Our formulation of refinements combines the type checking and sort checking phases into one by viewing typing derivations as outputs of sorting derivations. This allows us to cleanly state and prove the conservativity of our extension. ... : In Proceedings LFMTP 2023, arXiv:2311.09918 ... Text Beluga Beluga* DataCite Metadata Store (German National Library of Science and Technology) |
| institution |
Open Polar |
| collection |
DataCite Metadata Store (German National Library of Science and Technology) |
| op_collection_id |
ftdatacite |
| language |
unknown |
| topic |
Programming Languages cs.PL FOS Computer and information sciences D.3.1; F.3.1 |
| spellingShingle |
Programming Languages cs.PL FOS Computer and information sciences D.3.1; F.3.1 Gaulin, Antoine Pientka, Brigitte Contextual Refinement Types ... |
| topic_facet |
Programming Languages cs.PL FOS Computer and information sciences D.3.1; F.3.1 |
| description |
We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, which provide fine-grained classification for the structures of contexts and binders. Refinement schemas are helpful in concisely representing certain proofs that rely on relations between contexts. Our formulation of refinements combines the type checking and sort checking phases into one by viewing typing derivations as outputs of sorting derivations. This allows us to cleanly state and prove the conservativity of our extension. ... : In Proceedings LFMTP 2023, arXiv:2311.09918 ... |
| format |
Text |
| author |
Gaulin, Antoine Pientka, Brigitte |
| author_facet |
Gaulin, Antoine Pientka, Brigitte |
| author_sort |
Gaulin, Antoine |
| title |
Contextual Refinement Types ... |
| title_short |
Contextual Refinement Types ... |
| title_full |
Contextual Refinement Types ... |
| title_fullStr |
Contextual Refinement Types ... |
| title_full_unstemmed |
Contextual Refinement Types ... |
| title_sort |
contextual refinement types ... |
| publisher |
arXiv |
| publishDate |
2023 |
| url |
https://dx.doi.org/10.48550/arxiv.2311.10577 https://arxiv.org/abs/2311.10577 |
| genre |
Beluga Beluga* |
| genre_facet |
Beluga Beluga* |
| op_relation |
https://dx.doi.org/10.4204/eptcs.396.2 |
| op_rights |
Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 |
| op_doi |
https://doi.org/10.48550/arxiv.2311.1057710.4204/eptcs.396.2 |
| _version_ |
1786836862143299584 |