A General Semantic Construction of Dependent Refinement Type Systems, Categorically

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

Descripción completa

Detalles Bibliográficos
Autor principal: Kura, Satoshi
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2021
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984113/
http://dx.doi.org/10.1007/978-3-030-71995-1_21
_version_ 1783668007962148864
author Kura, Satoshi
author_facet Kura, Satoshi
author_sort Kura, Satoshi
collection PubMed
description Dependent 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 dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness.
format Online
Article
Text
id pubmed-7984113
institution National Center for Biotechnology Information
language English
publishDate 2021
record_format MEDLINE/PubMed
spelling pubmed-79841132021-03-23 A General Semantic Construction of Dependent Refinement Type Systems, Categorically Kura, Satoshi Foundations of Software Science and Computation Structures Article Dependent 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 dependent refinement type systems. We demonstrate the usage of our construction by giving semantics to a dependent refinement type system and proving soundness. 2021-03-23 /pmc/articles/PMC7984113/ http://dx.doi.org/10.1007/978-3-030-71995-1_21 Text en © The Author(s) 2021 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Kura, Satoshi
A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title_full A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title_fullStr A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title_full_unstemmed A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title_short A General Semantic Construction of Dependent Refinement Type Systems, Categorically
title_sort general semantic construction of dependent refinement type systems, categorically
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7984113/
http://dx.doi.org/10.1007/978-3-030-71995-1_21
work_keys_str_mv AT kurasatoshi ageneralsemanticconstructionofdependentrefinementtypesystemscategorically
AT kurasatoshi generalsemanticconstructionofdependentrefinementtypesystemscategorically

Ejemplares similares