arXiv
Open Access
2023
Contextual Refinement Types
Antoine Gaulin
Brigitte Pientka
Abstrak
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.
Topik & Kata Kunci
Penulis (2)
A
Antoine Gaulin
B
Brigitte Pientka
Akses Cepat
Informasi Jurnal
- Tahun Terbit
- 2023
- Bahasa
- en
- Sumber Database
- arXiv
- Akses
- Open Access ✓