File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Conference Paper: Type-Directed Operational Semantics for Gradual Typing

TitleType-Directed Operational Semantics for Gradual Typing
Authors
KeywordsGradual Typing
Type Systems
Operational Semantics
Issue Date2021
PublisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/
Citation
The 35th European Conference on Object-Oriented Programming (ECOOP 2021), Virtual Conference, Aarhus, Denmark, 12-16 July 2021. In Møller, A & Sridharan, M (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2021, v. 194, article no. 12, p. 12:1-12:30 How to Cite?
AbstractThe semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λ B^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λ B^r, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi, type safety is proved. Furthermore we show that the semantics of λ B^g is sound with respect to the semantics of the blame calculus, and that λ B^r comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.
DescriptionECOOP 2021 ECOOP Technical Papers: Types (time band 2) at ECOOP 1 & Potpourri (time band 3) at ECOOP 1
Persistent Identifierhttp://hdl.handle.net/10722/301311
ISSN
2023 SCImago Journal Rankings: 0.796

 

DC FieldValueLanguage
dc.contributor.authorYe, W-
dc.contributor.authorDos Santos Oliveira, BC-
dc.contributor.authorHuang, X-
dc.date.accessioned2021-07-27T08:09:15Z-
dc.date.available2021-07-27T08:09:15Z-
dc.date.issued2021-
dc.identifier.citationThe 35th European Conference on Object-Oriented Programming (ECOOP 2021), Virtual Conference, Aarhus, Denmark, 12-16 July 2021. In Møller, A & Sridharan, M (Eds.). LIPICS - Leibniz International Proceedings in Informatics, 2021, v. 194, article no. 12, p. 12:1-12:30-
dc.identifier.issn1868-8969-
dc.identifier.urihttp://hdl.handle.net/10722/301311-
dc.descriptionECOOP 2021 ECOOP Technical Papers: Types (time band 2) at ECOOP 1 & Potpourri (time band 3) at ECOOP 1-
dc.description.abstractThe semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λ B^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λ B^r, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi, type safety is proved. Furthermore we show that the semantics of λ B^g is sound with respect to the semantics of the blame calculus, and that λ B^r comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.-
dc.languageeng-
dc.publisherSchloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH. The Journal's web site is located at hhttp://www.dagstuhl.de/publikationen/lipics/-
dc.relation.ispartofLIPICS - Leibniz International Proceedings in Informatics-
dc.relation.ispartofThe 35th European Conference on Object-Oriented Programming (ECOOP 2021)-
dc.rightsThis work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.-
dc.subjectGradual Typing-
dc.subjectType Systems-
dc.subjectOperational Semantics-
dc.titleType-Directed Operational Semantics for Gradual Typing-
dc.typeConference_Paper-
dc.identifier.emailDos Santos Oliveira, BC: bruno@cs.hku.hk-
dc.identifier.authorityDos Santos Oliveira, BC=rp01786-
dc.description.naturepublished_or_final_version-
dc.identifier.doi10.4230/LIPIcs.ECOOP.2021.12-
dc.identifier.scopuseid_2-s2.0-85115203711-
dc.identifier.hkuros323744-
dc.identifier.volume194-
dc.identifier.spage12:1-
dc.identifier.epage12:30-
dc.publisher.placeGermany-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats