162 Search Results for "Sangiorgi, Davide"

Volume

LIPIcs, Volume 55

43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

ICALP 2016, July 11-15, 2016, Rome, Italy

Editors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Document
DOI: 10.4230/LIPIcs.FSCD.2023.28
Concurrent Realizability on Conjunctive Structures

Authors: Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
This work aims at exploring the algebraic structure of concurrent processes and their behavior independently of a particular formalism used to define them. We propose a new algebraic structure called conjunctive involutive monoidal algebra (CIMA) as a basis for an algebraic presentation of concurrent realizability, following ideas of the algebrization program already developed in the realm of classical and intuitionistic realizability. In particular, we show how any CIMA provides a sound interpretation of multiplicative linear logic. This new structure involves, in addition to the tensor and the orthogonal map, a parallel composition. We define a reference model of this structure as induced by a standard process calculus and we use this model to prove that parallel composition cannot be defined from the conjunctive structure alone.
Cite as

Emmanuel Beffara, Félix Castro, Mauricio Guillermo, and Étienne Miquey. Concurrent Realizability on Conjunctive Structures. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 28:1-28:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{beffara_et_al:LIPIcs.FSCD.2023.28,
  author =	{Beffara, Emmanuel and Castro, F\'{e}lix and Guillermo, Mauricio and Miquey, \'{E}tienne},
  title =	{{Concurrent Realizability on Conjunctive Structures}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{28:1--28:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.28},
  URN =		{urn:nbn:de:0030-drops-180124},
  doi =		{10.4230/LIPIcs.FSCD.2023.28},
  annote =	{Keywords: Realizability, Process Algebras, Concurrent Processes, Linear Logic}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2023.4
Enhanced Induction in Behavioural Relations (Invited Talk)

Authors: Davide Sangiorgi

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i.e., relations defined from inductive observables, and discuss relevant literature.
Cite as

Davide Sangiorgi. Enhanced Induction in Behavioural Relations (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 4:1-4:6, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{sangiorgi:LIPIcs.CSL.2023.4,
  author =	{Sangiorgi, Davide},
  title =	{{Enhanced Induction in Behavioural Relations}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{4:1--4:6},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.4},
  URN =		{urn:nbn:de:0030-drops-174658},
  doi =		{10.4230/LIPIcs.CSL.2023.4},
  annote =	{Keywords: coinduction, induction, semantics, behavioural relations}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2022.1
CONCUR Test-Of-Time Award 2022 (Invited Paper)

Authors: Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.
Cite as

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
  author =	{Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
  title =	{{CONCUR Test-Of-Time Award 2022}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1:1--1:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.1},
  URN =		{urn:nbn:de:0030-drops-170644},
  doi =		{10.4230/LIPIcs.CONCUR.2022.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2022.130
Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques

Authors: Enguerrand Prebet

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
We present a fully abstract encoding of λ^{ref}, the call-by-value λ-calculus with references, in the π-calculus. By contrast with previous full abstraction results for sequential languages in the π-calculus, the characterisation of contextual equivalence in the source language uses a labelled bisimilarity. To define the latter equivalence, we refine existing notions of typed bisimulation in the π-calculus, and introduce in particular a specific component to handle divergences. We obtain a proof technique that allows us to prove equivalences between λ^{ref} programs via the encoding. The resulting proofs correspond closely to normal form bisimulations in the λ-calculus, making proofs in the π-calculus expressible as if reasoning in λ^{ref}. We study how standard and new up-to techniques can be used to reason about diverging terms and simplify proofs of equivalence using the bisimulation we introduce. This shows how the π-calculus theory can be used to prove interesting equivalences between λ^{ref} programs, using algebraic reasoning and up-to techniques.
Cite as

Enguerrand Prebet. Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 130:1-130:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{prebet:LIPIcs.ICALP.2022.130,
  author =	{Prebet, Enguerrand},
  title =	{{Functions and References in the Pi-Calculus: Full Abstraction and Proof Techniques}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{130:1--130:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.130},
  URN =		{urn:nbn:de:0030-drops-164715},
  doi =		{10.4230/LIPIcs.ICALP.2022.130},
  annote =	{Keywords: Call-by-value \lambda-calculus, imperative Programming, \pi-calculus, Bisimulation, Type System}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.25
Games, Mobile Processes, and Functions

Authors: Guilhem Jaber and Davide Sangiorgi

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS. We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide. These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.
Cite as

Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and Functions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 25:1-25:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jaber_et_al:LIPIcs.CSL.2022.25,
  author =	{Jaber, Guilhem and Sangiorgi, Davide},
  title =	{{Games, Mobile Processes, and Functions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.25},
  URN =		{urn:nbn:de:0030-drops-157450},
  doi =		{10.4230/LIPIcs.CSL.2022.25},
  annote =	{Keywords: \lambda-calculus, \pi-calculus, game semantics}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.5
The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service

Authors: Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ- and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence. Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )
Cite as

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:OASIcs.Gabbrielli.5,
  author =	{Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Sangiorgi, Davide and Zingaro, Stefano Pio},
  title =	{{The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{5:1--5:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.5},
  URN =		{urn:nbn:de:0030-drops-132271},
  doi =		{10.4230/OASIcs.Gabbrielli.5},
  annote =	{Keywords: Serverless computing, Process calculi, Pi-calculus}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.34
On the Representation of References in the Pi-Calculus

Authors: Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
The π-calculus has been advocated as a model to interpret, and give semantics to, languages with higher-order features. Often these languages make use of forms of references (and hence viewing a store as set of references). While translations of references in π-calculi (and CCS) have appeared, the precision of such translations has not been fully investigated. In this paper we address this issue. We focus on the asynchronous π-calculus (Aπ), where translations of references are simpler. We first define π^ref, an extension of Aπ with references and operators to manipulate them, and illustrate examples of the subtleties of behavioural equivalence in π^ref. We then consider a translation of π^ref into Aπ. References of π^ref are mapped onto names of Aπ belonging to a dedicated "reference" type. We show how the presence of reference names affects the definition of barbed congruence. We establish full abstraction of the translation w.r.t. barbed congruence and barbed equivalence in the two calculi. We investigate proof techniques for barbed equivalence in Aπ, based on two forms of labelled bisimilarities. For one bisimilarity we derive both soundness and completeness; for another, more efficient and involving an inductive "game" on reference names, we derive soundness, leaving completeness open. Finally, we discuss examples of uses of the bisimilarities.
Cite as

Daniel Hirschkoff, Enguerrand Prebet, and Davide Sangiorgi. On the Representation of References in the Pi-Calculus. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 34:1-34:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2020.34,
  author =	{Hirschkoff, Daniel and Prebet, Enguerrand and Sangiorgi, Davide},
  title =	{{On the Representation of References in the Pi-Calculus}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{34:1--34:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.34},
  URN =		{urn:nbn:de:0030-drops-128466},
  doi =		{10.4230/LIPIcs.CONCUR.2020.34},
  annote =	{Keywords: Process calculus, Bisimulation, Asynchrony, Imperative programming}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.10
Conditional Bisimilarity for Reactive Systems

Authors: Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Reactive systems à la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to obtain a compositional semantics. We enrich the notion of reactive systems by conditions on two levels: first, as in earlier work, we consider rules enriched with application conditions and second, we investigate the notion of conditional bisimilarity. Conditional bisimilarity allows us to say that two system states are bisimilar provided that the environment satisfies a given condition. We present several equivalent definitions of conditional bisimilarity, including one that is useful for concrete proofs and that employs an up-to-context technique, and we compare with related behavioural equivalences. We instantiate reactive systems in order to obtain DPO graph rewriting and consider a case study in this setting.
Cite as

Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lara Stoltenow. Conditional Bisimilarity for Reactive Systems. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 10:1-10:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hulsbusch_et_al:LIPIcs.FSCD.2020.10,
  author =	{H\"{u}lsbusch, Mathias and K\"{o}nig, Barbara and K\"{u}pper, Sebastian and Stoltenow, Lara},
  title =	{{Conditional Bisimilarity for Reactive Systems}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.10},
  URN =		{urn:nbn:de:0030-drops-123322},
  doi =		{10.4230/LIPIcs.FSCD.2020.10},
  annote =	{Keywords: conditional bisimilarity, reactive systems, up-to context, graph transformation}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.11
Divergence and Unique Solution of Equations

Authors: Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We study proof techniques for bisimilarity based on unique solution of equations. We draw inspiration from a result by Roscoe in the denotational setting of CSP and for failure semantics, essentially stating that an equation (or a system of equations) whose infinite unfolding never produces a divergence has the unique-solution property. We transport this result onto the operational setting of CCS and for bisimilarity. We then exploit the operational approach to: refine the theorem, distinguishing between different forms of divergence; derive an abstract formulation of the theorems, on generic LTSs; adapt the theorems to other equivalences such as trace equivalence, and to preorders such as trace inclusion. We compare the resulting techniques to enhancements of the bisimulation proof method (the ‘up-to techniques’). Finally, we study the theorems in name-passing calculi such as the asynchronous pi-calculus, and revisit the completeness proof of Milner’s encoding of the lambda-calculus into the pi-calculus for Lévy-Longo Trees.
Cite as

Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and Unique Solution of Equations. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 11:1-11:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{durier_et_al:LIPIcs.CONCUR.2017.11,
  author =	{Durier, Adrien and Hirschkoff, Daniel and Sangiorgi, Davide},
  title =	{{Divergence and Unique Solution of Equations}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{11:1--11:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.11},
  URN =		{urn:nbn:de:0030-drops-77849},
  doi =		{10.4230/LIPIcs.CONCUR.2017.11},
  annote =	{Keywords: Bisimilarity, unique solution of equations, termination, process calculi}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.ICALP.2016
LIPIcs, Volume 55, ICALP'16, Complete Volume

Authors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
LIPIcs, Volume 55, ICALP'16, Complete Volume
Cite as

Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi. LIPIcs, Volume 55, ICALP'16, Complete Volume. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Proceedings{chatzigiannakis_et_al:LIPIcs.ICALP.2016,
  title =	{{LIPIcs, Volume 55, ICALP'16, Complete Volume}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016},
  URN =		{urn:nbn:de:0030-drops-65844},
  doi =		{10.4230/LIPIcs.ICALP.2016},
  annote =	{Keywords: Theory of Computation}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ICALP.2016.0
Front Matter, Table of Contents, Preface, Organization, List of Authors

Authors: Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Front Matter, Table of Contents, Preface, Organization, List of Authors
Cite as

Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi. Front Matter, Table of Contents, Preface, Organization, List of Authors. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 0:i-0:xliv, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chatzigiannakis_et_al:LIPIcs.ICALP.2016.0,
  author =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  title =	{{Front Matter, Table of Contents, Preface, Organization, List of Authors}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{0:i--0:xliv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.0},
  URN =		{urn:nbn:de:0030-drops-61917},
  doi =		{10.4230/LIPIcs.ICALP.2016.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Organization, List of Authors}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2016.1
Compute Choice (Invited Talk)

Authors: Devavrat Shah

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
In this talk, we shall discuss the question of learning distribution over permutations of n choices based on partial observations. This is central to capturing the so called "choice" in a variety of contexts: understanding preferences of consumers over a collection of products based on purchasing and browsing data in the setting of retail and e-commerce, learning public opinion amongst a collection of socio-economic issues based on sparse polling data, and deciding a ranking of teams or players based on outcomes of games. The talk will primarily discuss the relationship between the ability to learn, nature of partial information and number of available observations. Connections to the classical theory of social choice and behavioral psychology, as well as modern literature in Statistics, learning theory and operations research will be discussed.
Cite as

Devavrat Shah. Compute Choice (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 1:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{shah:LIPIcs.ICALP.2016.1,
  author =	{Shah, Devavrat},
  title =	{{Compute Choice}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.1},
  URN =		{urn:nbn:de:0030-drops-63374},
  doi =		{10.4230/LIPIcs.ICALP.2016.1},
  annote =	{Keywords: Decision Systems, Learning Distributions, Partial observations}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2016.2
Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk)

Authors: Xavier Leroy

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
Compilers, and especially optimizing compilers, are complicated programs. Bugs in compilers happen, and can lead to miscompilation: the production of wrong executable code from a correct source program. Miscompilation is documented in the literature and a concern for high-assurance software, as it endangers the guarantees obtained by source-level formal verification of programs. Compiler verification is a radical solution to the miscompilation problem: by applying program proof to the compiler itself, we can obtain mathematically strong guarantees that the generated executable code is faithful to the semantics of the source program. The state of the art in this line of research is arguably the CompCert verified compiler. This talk will give an overview of this optimizing C compiler and of its formal verification, conducted with the Coq proof assistant. A formal verification is as good as the specifications it uses. In other words, verification reduces the problem of trusting a large implementation to that of ensuring that its formal specification enforce the intended correctness properties. In the case of CompCert, the correctness statement that is proved is rather complex, as it involves large operational semantics (for the C language and for the assembly languages of the target architectures) and simulations between these semantics that support both choice refinement and behavior refinement. The talk will review and discuss these elements of the specification, along with some of the accompanying proof principles.
Cite as

Xavier Leroy. Formally Verifying a Compiler: What Does It Mean, Exactly? (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 2:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{leroy:LIPIcs.ICALP.2016.2,
  author =	{Leroy, Xavier},
  title =	{{Formally Verifying a Compiler: What Does It Mean, Exactly?}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.2},
  URN =		{urn:nbn:de:0030-drops-63384},
  doi =		{10.4230/LIPIcs.ICALP.2016.2},
  annote =	{Keywords: Compilers, Compiler Optimization, Compiler Verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2016.3
Hardness of Approximation (Invited Talk)

Authors: Subhash Khot

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
The talk will present connections between approximability of NP-complete problems, analysis, and geometry, and the role played by the Unique Games Conjecture in facilitating these connections.
Cite as

Subhash Khot. Hardness of Approximation (Invited Talk). In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, p. 3:1, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{khot:LIPIcs.ICALP.2016.3,
  author =	{Khot, Subhash},
  title =	{{Hardness of Approximation}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{3:1--3:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.3},
  URN =		{urn:nbn:de:0030-drops-63395},
  doi =		{10.4230/LIPIcs.ICALP.2016.3},
  annote =	{Keywords: NP-completeness, Approximation algorithms, Inapproximability, Probabilistically Checkable Proofs, Discrete Fourier analysis}
}
  • Refine by Author
  • 8 Sangiorgi, Davide
  • 3 Galanis, Andreas
  • 3 Goldberg, Leslie Ann
  • 3 Hajiaghayi, Mohammad Taghi
  • 3 Mitzenmacher, Michael
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Concurrency
  • 2 Theory of computation → Program semantics
  • 2 Theory of computation → Semantics and reasoning
  • 1 Computer systems organization → Cloud computing
  • 1 Theory of computation → Linear logic
  • Show More...

  • Refine by Keyword
  • 5 Approximation Algorithms
  • 5 communication complexity
  • 3 Approximation algorithms
  • 3 Bisimulation
  • 3 complexity
  • Show More...

  • Refine by Type
  • 161 document
  • 1 volume

  • Refine by Publication Year
  • 153 2016
  • 3 2020
  • 3 2022
  • 2 2023
  • 1 2017

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact