License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2018.24
URN: urn:nbn:de:0030-drops-91944
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9194/
Go to the corresponding LIPIcs Volume Portal

New, Max S. ; Licata, Daniel R.

Call-by-Name Gradual Type Theory

pdf-format:
LIPIcs-FSCD-2018-24.pdf (0.5 MB)

Abstract

We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgments for gradual type and term dynamism. These dynamism judgements build on prior work in blame calculi and on the "gradual guarantee" theorem of gradual typing. Combined with the ordinary extensionality (eta) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of the interpretation of gradual typing using contracts, and use it to build some concrete domain-theoretic models of gradual typing.

BibTeX - Entry

@InProceedings{new_et_al:LIPIcs:2018:9194,
  author =	{Max S. New and Daniel R. Licata},
  title =	{{Call-by-Name Gradual Type Theory}},
  booktitle =	{3rd International Conference on Formal Structures for  Computation and Deduction (FSCD 2018)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{H{\'e}l{\`e}ne Kirchner},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9194},
  URN =		{urn:nbn:de:0030-drops-91944},
  doi =		{10.4230/LIPIcs.FSCD.2018.24},
  annote =	{Keywords: Gradual Typing, Type Systems, Program Logics, Category Theory, Denotational Semantics}
}

Keywords: Gradual Typing, Type Systems, Program Logics, Category Theory, Denotational Semantics
Collection: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Issue Date: 2018
Date of publication: 04.07.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI