General Semantic Construction of Dependent Refinement Type Systems, Categorically
Logic in Computer Science
2020-10-19 v1
Abstract
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type systems and predicate logic, that is, a construction of liftings of closed comprehension categories from given (underlying) closed comprehension categories and posetal fibrations for predicate logic. We give sufficient conditions to lift structures such as dependent products, dependent sums, computational effects, and recursion from the underlying type systems to refinement type systems. We demonstrate the usage of our construction by giving semantics to a refinement type system and proving soundness.
Cite
@article{arxiv.2010.08280,
title = {General Semantic Construction of Dependent Refinement Type Systems, Categorically},
author = {Satoshi Kura},
journal= {arXiv preprint arXiv:2010.08280},
year = {2020}
}
Comments
32 pages