License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2023.4
URN: urn:nbn:de:0030-drops-188019
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18801/
Go to the corresponding LIPIcs Volume Portal

Siek, Jeremy G.

The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk)

pdf-format:
LIPIcs-CALCO-2023-4.pdf (0.3 MB)

Abstract

Gradually typed languages offer both static and dynamic checking of program invariants, from simple properties such as type safety, to more advanced ones such as information flow control (security), relational parametricity (theorems for free), and program correctness. To ensure that gradually typed languages behave as expected, researchers prove theorems about their language designs. For example, the Gradual Guarantee Theorem states that a programmer can migrate their program to become more or less statically checked and the resulting program will behave the same (modulo errors). As another example, the Noninterference Theorem (for information flow control) states that high security inputs do not affect the low security outputs of a program. These theorems are often proved using simulation arguments or via syntactic logical relations and modal logics. Sometimes the proofs are mechanized in a proof assistant, but often they are simply written in LaTeX. However, as researchers consider gradual languages of growing complexity, the time to conduct such proofs, and/or the likelihood of errors in the proofs, also grows. As a result there is a need for improved proof techniques and libraries of mechanized results that would help to streamline the development of the metatheory of gradually typed languages.

BibTeX - Entry

@InProceedings{siek:LIPIcs.CALCO.2023.4,
  author =	{Siek, Jeremy G.},
  title =	{{The Metatheory of Gradual Typing: State of the Art and Challenges}},
  booktitle =	{10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-287-7},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{270},
  editor =	{Baldan, Paolo and de Paiva, Valeria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18801},
  URN =		{urn:nbn:de:0030-drops-188019},
  doi =		{10.4230/LIPIcs.CALCO.2023.4},
  annote =	{Keywords: gradual typing, type safety, gradual guarantee, noninterference, simulation, logical relation, mechanized metatheory}
}

Keywords: gradual typing, type safety, gradual guarantee, noninterference, simulation, logical relation, mechanized metatheory
Collection: 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)
Issue Date: 2023
Date of publication: 02.09.2023

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