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...

Full description

Bibliographic Details
Published in:Electronic Proceedings in Theoretical Computer Science
Main Authors: Gaulin, Antoine, Pientka, Brigitte
Format: Text
Language:unknown
Published: 2023
Subjects:
Computer Science - Programming Languages
D.3.1
F.3.1
Beluga
Beluga*
Online Access:http://arxiv.org/abs/2311.10577
https://doi.org/10.4204/EPTCS.396.2
id ftarxivpreprints:oai:arXiv.org:2311.10577
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:2311.10577 2023-12-24T10:15:29+01:00 Contextual Refinement Types Gaulin, Antoine Pientka, Brigitte 2023-11-17 http://arxiv.org/abs/2311.10577 https://doi.org/10.4204/EPTCS.396.2 unknown http://arxiv.org/abs/2311.10577 EPTCS 396, 2023, pp. 4-19 doi:10.4204/EPTCS.396.2 Computer Science - Programming Languages D.3.1 F.3.1 text 2023 ftarxivpreprints https://doi.org/10.4204/EPTCS.396.2 2023-11-26T02:06:59Z 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. Comment: In Proceedings LFMTP 2023, arXiv:2311.09918 Text Beluga Beluga* ArXiv.org (Cornell University Library) Electronic Proceedings in Theoretical Computer Science 396 4 19
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Computer Science - Programming Languages
D.3.1
F.3.1
spellingShingle Computer Science - Programming Languages
D.3.1
F.3.1
Gaulin, Antoine
Pientka, Brigitte
Contextual Refinement Types
topic_facet Computer Science - Programming Languages
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. Comment: 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
publishDate 2023
url http://arxiv.org/abs/2311.10577
https://doi.org/10.4204/EPTCS.396.2
genre Beluga
Beluga*
genre_facet Beluga
Beluga*
op_relation http://arxiv.org/abs/2311.10577
EPTCS 396, 2023, pp. 4-19
doi:10.4204/EPTCS.396.2
op_doi https://doi.org/10.4204/EPTCS.396.2
container_title Electronic Proceedings in Theoretical Computer Science
container_volume 396
container_start_page 4
op_container_end_page 19
_version_ 1786202381700038656

Similar Items