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

Author Jeremy G. Siek

Thumbnail PDF


  • Filesize: 328 kB
  • 1 pages

Document Identifiers

Author Details

Jeremy G. Siek
  • Computing Laboratory, Indiana University, Bloomington, IN, USA

Cite AsGet BibTex

Jeremy G. Siek. The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk). In 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 270, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Semantics
  • Theory of computation → Operational semantics
  • gradual typing
  • type safety
  • gradual guarantee
  • noninterference
  • simulation
  • logical relation
  • mechanized metatheory


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail