3 Search Results for "Siek, Jeremy G."

Document
Invited Talk
DOI: 10.4230/LIPIcs.CALCO.2023.4
The Metatheory of Gradual Typing: State of the Art and Challenges (Invited Talk)

Authors: Jeremy G. Siek

Published in: LIPIcs, Volume 270, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO 2023)

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.
Cite as

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)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2023.4},
  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}
}
Document
DOI: 10.4230/LIPIcs.IPEC.2020.16
Approximation Algorithms for Steiner Tree Based on Star Contractions: A Unified View

Authors: Radek Hušek, Dušan Knop, and Tomáš Masařk

Published in: LIPIcs, Volume 180, 15th International Symposium on Parameterized and Exact Computation (IPEC 2020)

Abstract
In the Steiner Tree problem, we are given an edge-weighted undirected graph G = (V,E) and a set of terminals R ⊆ V. The task is to find a connected subgraph of G containing R and minimizing the sum of weights of its edges. Steiner Tree is well known to be NP-complete and is undoubtedly one of the most studied problems in (applied) computer science. We observe that many approximation algorithms for Steiner Tree follow a similar scheme (meta-algorithm) and perform (exhaustively) a similar routine which we call star contraction. Here, by a star contraction, we mean finding a star-like subgraph in (the metric closure of) the input graph minimizing the ratio of its weight to the number of contained terminals minus one; and contract. It is not hard to see that the well-known MST-approximation seeks the best star to contract among those containing two terminals only. Zelikovsky’s approximation algorithm follows a similar workflow, finding the best star among those containing three terminals. We perform an empirical study of star contractions with the relaxed condition on the number of terminals in each star contraction motivated by a recent result of Dvořák et al. [Parameterized Approximation Schemes for Steiner Trees with Small Number of Steiner Vertices, STACS 2018]. Furthermore, we propose two improvements of Zelikovsky’s 11/6-approximation algorithm and we empirically confirm that the quality of the solution returned by any of these is better than the one returned by the former algorithm. However, such an improvement is exchanged for a slower running time (up to a multiplicative factor of the number of terminals).
Cite as

Radek Hušek, Dušan Knop, and Tomáš Masařk. Approximation Algorithms for Steiner Tree Based on Star Contractions: A Unified View. In 15th International Symposium on Parameterized and Exact Computation (IPEC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 180, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{husek_et_al:LIPIcs.IPEC.2020.16,
  author =	{Hu\v{s}ek, Radek and Knop, Du\v{s}an and Masa\v{r}k, Tom\'{a}\v{s}},
  title =	{{Approximation Algorithms for Steiner Tree Based on Star Contractions: A Unified View}},
  booktitle =	{15th International Symposium on Parameterized and Exact Computation (IPEC 2020)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-172-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{180},
  editor =	{Cao, Yixin and Pilipczuk, Marcin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.IPEC.2020.16},
  URN =		{urn:nbn:de:0030-drops-133193},
  doi =		{10.4230/LIPIcs.IPEC.2020.16},
  annote =	{Keywords: Steiner tree, approximation, star contractions, minimum spanning tree}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.274
Refined Criteria for Gradual Typing

Authors: Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Siek and Taha [2006] coined the term gradual typing to describe a theory for integrating static and dynamic typing within a single language that 1) puts the programmer in control of which regions of code are statically or dynamically typed and 2) enables the gradual evolution of code between the two typing disciplines. Since 2006, the term gradual typing has become quite popular but its meaning has become diluted to encompass anything related to the integration of static and dynamic typing. This dilution is partly the fault of the original paper, which provided an incomplete formal characterization of what it means to be gradually typed. In this paper we draw a crisp line in the sand that includes a new formal property, named the gradual guarantee, that relates the behavior of programs that differ only with respect to their type annotations. We argue that the gradual guarantee provides important guidance for designers of gradually typed languages. We survey the gradual typing literature, critiquing designs in light of the gradual guarantee. We also report on a mechanized proof that the gradual guarantee holds for the Gradually Typed Lambda Calculus.
Cite as

Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 274-293, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{siek_et_al:LIPIcs.SNAPL.2015.274,
  author =	{Siek, Jeremy G. and Vitousek, Michael M. and Cimini, Matteo and Boyland, John Tang},
  title =	{{Refined Criteria for Gradual Typing}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{274--293},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.274},
  URN =		{urn:nbn:de:0030-drops-50312},
  doi =		{10.4230/LIPIcs.SNAPL.2015.274},
  annote =	{Keywords: gradual typing, type systems, semantics, dynamic languages}
}
  • Refine by Author
  • 2 Siek, Jeremy G.
  • 1 Boyland, John Tang
  • 1 Cimini, Matteo
  • 1 Hušek, Radek
  • 1 Knop, Dušan
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 2 gradual typing
  • 1 Steiner tree
  • 1 approximation
  • 1 dynamic languages
  • 1 gradual guarantee
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2015
  • 1 2020
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact