Explicit Refinement Types

We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a r...

Full description

Bibliographic Details
Published in:Proceedings of the ACM on Programming Languages
Main Authors: Ghalayini, Jad Elkhaleq, Krishnaswami, Neel
Format: Text
Language:unknown
Published: 2023
Subjects:
Computer Science - Programming Languages
D.3.1
D.3.4
F.3.2
F.3.1
DML
Online Access:http://arxiv.org/abs/2311.13995
https://doi.org/10.1145/3607837
id ftarxivpreprints:oai:arXiv.org:2311.13995
record_format openpolar
spelling ftarxivpreprints:oai:arXiv.org:2311.13995 2023-12-31T10:06:17+01:00 Explicit Refinement Types Ghalayini, Jad Elkhaleq Krishnaswami, Neel 2023-11-23 http://arxiv.org/abs/2311.13995 https://doi.org/10.1145/3607837 unknown http://arxiv.org/abs/2311.13995 doi:10.1145/3607837 Computer Science - Programming Languages D.3.1 D.3.4 F.3.2 F.3.1 text 2023 ftarxivpreprints https://doi.org/10.1145/3607837 2023-12-03T02:07:05Z We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4. Comment: 31 pages, published at ICFP 2023 Text DML ArXiv.org (Cornell University Library) Proceedings of the ACM on Programming Languages 7 ICFP 187 214
institution Open Polar
collection ArXiv.org (Cornell University Library)
op_collection_id ftarxivpreprints
language unknown
topic Computer Science - Programming Languages
D.3.1
D.3.4
F.3.2
F.3.1
spellingShingle Computer Science - Programming Languages
D.3.1
D.3.4
F.3.2
F.3.1
Ghalayini, Jad Elkhaleq
Krishnaswami, Neel
Explicit Refinement Types
topic_facet Computer Science - Programming Languages
D.3.1
D.3.4
F.3.2
F.3.1
description We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs of properties within the program text, letting us support a rich logic of properties including quantifiers and induction. We show that the type system is sound by showing that every refined program erases to a simply-typed program, and by means of a denotational semantics, we show that every erased program has all of the properties demanded by its refined type. All of our proofs are formalised in Lean 4. Comment: 31 pages, published at ICFP 2023
format Text
author Ghalayini, Jad Elkhaleq
Krishnaswami, Neel
author_facet Ghalayini, Jad Elkhaleq
Krishnaswami, Neel
author_sort Ghalayini, Jad Elkhaleq
title Explicit Refinement Types
title_short Explicit Refinement Types
title_full Explicit Refinement Types
title_fullStr Explicit Refinement Types
title_full_unstemmed Explicit Refinement Types
title_sort explicit refinement types
publishDate 2023
url http://arxiv.org/abs/2311.13995
https://doi.org/10.1145/3607837
genre DML
genre_facet DML
op_relation http://arxiv.org/abs/2311.13995
doi:10.1145/3607837
op_doi https://doi.org/10.1145/3607837
container_title Proceedings of the ACM on Programming Languages
container_volume 7
container_issue ICFP
container_start_page 187
op_container_end_page 214
_version_ 1786838268934881280

Similar Items