6 Search Results for "Zappa Nardelli, Francesco"

Document
DOI: 10.4230/LIPIcs.ITP.2024.36
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

Authors: Andrew Tolmach, Chris Chhak, and Sean Anderson

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.
Cite as

Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36,
  author =	{Tolmach, Andrew and Chhak, Chris and Anderson, Sean},
  title =	{{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36},
  URN =		{urn:nbn:de:0030-drops-207643},
  doi =		{10.4230/LIPIcs.ITP.2024.36},
  annote =	{Keywords: Compiler verification, C language semantics, Coq proof assistant}
}
Document
Artifact
DOI: 10.4230/DARTS.5.2.8
On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact)

Authors: Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek

Published in: DARTS, Volume 5, Issue 2, Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
This is the artifact for the pearl paper "On Julia’s efficient algorithm for subtyping union types and covariant tuples."
Cite as

Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples (Artifact). In Special Issue of the 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Dagstuhl Artifacts Series (DARTS), Volume 5, Issue 2, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{chung_et_al:DARTS.5.2.8,
  author =	{Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
  title =	{{On Julia’s Efficient Algorithm for Subtyping Union Types and Covariant Tuples}},
  pages =	{8:1--8:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2019},
  volume =	{5},
  number =	{2},
  editor =	{Chung, Benjamin and Nardelli, Francesco Zappa and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.5.2.8},
  URN =		{urn:nbn:de:0030-drops-107855},
  doi =		{10.4230/DARTS.5.2.8},
  annote =	{Keywords: Type systems, subtyping, algorithmic type systems, distributive unions}
}
Document
Pearl
DOI: 10.4230/LIPIcs.ECOOP.2019.24
Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl)

Authors: Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Abstract
The Julia programming language supports multiple dispatch and provides a rich type annotation language to specify method applicability. When multiple methods are applicable for a given call, Julia relies on subtyping between method signatures to pick the correct method to invoke. Julia’s subtyping algorithm is surprisingly complex, and determining whether it is correct remains an open question. In this paper, we focus on one piece of this problem: the interaction between union types and covariant tuples. Previous work normalized unions inside tuples to disjunctive normal form. However, this strategy has two drawbacks: complex type signatures induce space explosion, and interference between normalization and other features of Julia’s type system. In this paper, we describe the algorithm that Julia uses to compute subtyping between tuples and unions - an algorithm that is immune to space explosion and plays well with other features of the language. We prove this algorithm correct and complete against a semantic-subtyping denotational model in Coq.
Cite as

Benjamin Chung, Francesco Zappa Nardelli, and Jan Vitek. Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.ECOOP.2019.24,
  author =	{Chung, Benjamin and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{Julia’s Efficient Algorithm for Subtyping Unions and Covariant Tuples}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{24:1--24:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.24},
  URN =		{urn:nbn:de:0030-drops-108165},
  doi =		{10.4230/LIPIcs.ECOOP.2019.24},
  annote =	{Keywords: Type systems, Subtyping, Union types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.12
KafKa: Gradual Typing for Objects

Authors: Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems embody fundamentally different ideas of what it means to be well-typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. We present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.
Cite as

Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 12:1-12:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chung_et_al:LIPIcs.ECOOP.2018.12,
  author =	{Chung, Benjamin and Li, Paley and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{KafKa: Gradual Typing for Objects}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{12:1--12:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.12},
  URN =		{urn:nbn:de:0030-drops-92170},
  doi =		{10.4230/LIPIcs.ECOOP.2018.12},
  annote =	{Keywords: Gradual typing, object-orientation, language design, type systems}
}
Document
DOI: 10.4230/DARTS.4.3.10
KafKa: Gradual Typing for Objects (Artifact)

Authors: Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
A wide range of gradual type systems have been proposed, providing many languages with the ability to mix typed and untyped code. However, hiding under language details, these gradual type systems have fundamentally different ideas of what it means to be typed. In this paper, we show that four of the most common gradual type systems provide distinct guarantees, and we give a formal framework for comparing gradual type systems for object-oriented languages. First, we show that the different gradual type systems are practically distinguishable via a three-part litmus test. Then, we present a formal framework for defining and comparing gradual type systems. Within this framework, different gradual type systems become translations between a common source and target language, allowing for direct comparison of semantics and guarantees.
Cite as

Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{chung_et_al:DARTS.4.3.10,
  author =	{Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
  title =	{{KafKa: Gradual Typing for Objects (Artifact)}},
  pages =	{10:1--10:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.10},
  URN =		{urn:nbn:de:0030-drops-92411},
  doi =		{10.4230/DARTS.4.3.10},
  annote =	{Keywords: Gradual typing, object-orientation, language design, type systems}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.76
Concrete Types for TypeScript

Authors: Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
Typescript extends JavaScript with optional type annotations that are, by design, unsound and, that the Typescript compiler discards as it emits code. This design point preserves programming idioms developers are familiar with, and allows them to leave their legacy code unchanged, while offering a measure of static error checking in parts of the program that have type annotations. We present an alternative design for TypeScript, one where it is possible to support the same degree of dynamism, but where types can be strengthened to provide hard guarantees. We report on an implementation, called StrongScript, that improves runtime performance of typed programs when run on a modified version of the V8 JavaScript engine.
Cite as

Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek. Concrete Types for TypeScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 76-100, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{richards_et_al:LIPIcs.ECOOP.2015.76,
  author =	{Richards, Gregor and Zappa Nardelli, Francesco and Vitek, Jan},
  title =	{{Concrete Types for TypeScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{76--100},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.76},
  URN =		{urn:nbn:de:0030-drops-52185},
  doi =		{10.4230/LIPIcs.ECOOP.2015.76},
  annote =	{Keywords: Gradual typing, dynamic languages}
}
  • Refine by Author
  • 5 Vitek, Jan
  • 4 Chung, Benjamin
  • 3 Zappa Nardelli, Francesco
  • 2 Li, Paley
  • 2 Nardelli, Francesco Zappa
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Semantics
  • 2 Theory of computation → Type theory
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → General programming languages

  • Refine by Keyword
  • 3 Gradual typing
  • 2 Type systems
  • 2 language design
  • 2 object-orientation
  • 2 type systems
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2018
  • 2 2019
  • 1 2015
  • 1 2024

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