Max S. New ; Daniel R. Licata - Call-by-name Gradual Type Theory

lmcs:5154 - Logical Methods in Computer Science, January 31, 2020, Volume 16, Issue 1 - https://doi.org/10.23638/LMCS-16(1:7)2020
Call-by-name Gradual Type TheoryArticle

Authors: Max S. New ; Daniel R. Licata

    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, which were developed in blame calculi and to state 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 Findler and Felleisen's definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.


    Volume: Volume 16, Issue 1
    Published on: January 31, 2020
    Accepted on: January 12, 2020
    Submitted on: January 31, 2019
    Keywords: Computer Science - Programming Languages
    Funding:
      Source : OpenAIRE Graph
    • CAREER: Verified Compilers for a Multi-Language World; Funder: National Science Foundation; Code: 1453796

    1 Document citing this article

    Consultation statistics

    This page has been seen 1541 times.
    This article's PDF has been downloaded 361 times.