7 Search Results for "David, Marco"


Document
Pearl
Multiparty Languages: The Choreographic and Multitier Cases (Pearl)

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)


Abstract
Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings - respectively process calculi and lambda calculus - the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.

Cite as

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. Multiparty Languages: The Choreographic and Multitier Cases (Pearl). In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:LIPIcs.ECOOP.2021.22,
  author =	{Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title =	{{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{22:1--22:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.22},
  URN =		{urn:nbn:de:0030-drops-140658},
  doi =		{10.4230/LIPIcs.ECOOP.2021.22},
  annote =	{Keywords: Distributed Programming, Choreographies, Multitier Languages}
}
Document
On Computing the Diameter of (Weighted) Link Streams

Authors: Marco Calamai, Pierluigi Crescenzi, and Andrea Marino

Published in: LIPIcs, Volume 190, 19th International Symposium on Experimental Algorithms (SEA 2021)


Abstract
A weighted link stream is a pair (V,𝔼) comprising V, the set of nodes, and 𝔼, the list of temporal edges (u,v,t,λ), where u,v are two nodes in V, t is the starting time of the temporal edge, and λ is its travel time. By making use of this model, different notions of diameter can be defined, which refer to the following distances: earliest arrival time, latest departure time, fastest time, and shortest time. After proving that any of these diameters cannot be computed in time sub-quadratic with respect to the number of temporal edges, we propose different algorithms (inspired by the approach used for computing the diameter of graphs) which allow us to compute, in practice very efficiently, the diameter of quite large real-world weighted link stream for several definitions of the diameter. Indeed, all the proposed algorithms require very often a very low number of single source (or target) best path computations. We verify the effectiveness of our approach by means of an extensive set of experiments on real-world link streams. We also experimentally prove that the temporal version of the well-known 2-sweep technique, for computing a lower bound on the diameter of a graph, is quite effective in the case of weighted link stream, by returning very often tight bounds.

Cite as

Marco Calamai, Pierluigi Crescenzi, and Andrea Marino. On Computing the Diameter of (Weighted) Link Streams. In 19th International Symposium on Experimental Algorithms (SEA 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 190, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{calamai_et_al:LIPIcs.SEA.2021.11,
  author =	{Calamai, Marco and Crescenzi, Pierluigi and Marino, Andrea},
  title =	{{On Computing the Diameter of (Weighted) Link Streams}},
  booktitle =	{19th International Symposium on Experimental Algorithms (SEA 2021)},
  pages =	{11:1--11:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-185-6},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{190},
  editor =	{Coudert, David and Natale, Emanuele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SEA.2021.11},
  URN =		{urn:nbn:de:0030-drops-137836},
  doi =		{10.4230/LIPIcs.SEA.2021.11},
  annote =	{Keywords: Temporal graph, shortest path, diameter}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
The Complexity of Verifying Loop-Free Programs as Differentially Private

Authors: Marco Gaboardi, Kobbi Nissim, and David Purser

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)


Abstract
We study the problem of verifying differential privacy for loop-free programs with probabilistic choice. Programs in this class can be seen as randomized Boolean circuits, which we will use as a formal model to answer two different questions: first, deciding whether a program satisfies a prescribed level of privacy; second, approximating the privacy parameters a program realizes. We show that the problem of deciding whether a program satisfies ε-differential privacy is coNP^#P-complete. In fact, this is the case when either the input domain or the output range of the program is large. Further, we show that deciding whether a program is (ε,δ)-differentially private is coNP^#P-hard, and in coNP^#P for small output domains, but always in coNP^{#P^#P}. Finally, we show that the problem of approximating the level of differential privacy is both NP-hard and coNP-hard. These results complement previous results by Murtagh and Vadhan [Jack Murtagh and Salil P. Vadhan, 2016] showing that deciding the optimal composition of differentially private components is #P-complete, and that approximating the optimal composition of differentially private components is in P.

Cite as

Marco Gaboardi, Kobbi Nissim, and David Purser. The Complexity of Verifying Loop-Free Programs as Differentially Private. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 129:1-129:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{gaboardi_et_al:LIPIcs.ICALP.2020.129,
  author =	{Gaboardi, Marco and Nissim, Kobbi and Purser, David},
  title =	{{The Complexity of Verifying Loop-Free Programs as Differentially Private}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{129:1--129:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.129},
  URN =		{urn:nbn:de:0030-drops-125362},
  doi =		{10.4230/LIPIcs.ICALP.2020.129},
  annote =	{Keywords: differential privacy, program verification, probabilistic programs}
}
Document
Short Paper
The DPRM Theorem in Isabelle (Short Paper)

Authors: Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
Hilbert’s 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich’s proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations.

Cite as

Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 33:1-33:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bayer_et_al:LIPIcs.ITP.2019.33,
  author =	{Bayer, Jonas and David, Marco and Pal, Abhik and Stock, Benedikt and Schleicher, Dierk},
  title =	{{The DPRM Theorem in Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{33:1--33:7},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.33},
  URN =		{urn:nbn:de:0030-drops-110883},
  doi =		{10.4230/LIPIcs.ITP.2019.33},
  annote =	{Keywords: DPRM theorem, Hilbert’s tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification}
}
Document
Invited Talk
The Power of the Terminating Chase (Invited Talk)

Authors: Markus Krötzsch, Maximilian Marx, and Sebastian Rudolph

Published in: LIPIcs, Volume 127, 22nd International Conference on Database Theory (ICDT 2019)


Abstract
The chase has become a staple of modern database theory with applications in data integration, query optimisation, data exchange, ontology-based query answering, and many other areas. Most application scenarios and implementations require the chase to terminate and produce a finite universal model, and a large arsenal of sufficient termination criteria is available to guarantee this (generally undecidable) condition. In this invited tutorial, we therefore ask about the expressive power of logical theories for which the chase terminates. Specifically, which database properties can be recognised by such theories, i.e., which Boolean queries can they realise? For the skolem (semi-oblivious) chase, and almost any known termination criterion, this expressivity is just that of plain Datalog. Surprisingly, this limitation of most prior research does not apply to the chase in general. Indeed, we show that standard - chase terminating theories can realise queries with data complexities ranging from PTime to non-elementary that are out of reach for the terminating skolem chase. A "Datalog-first" standard chase that prioritises applications of rules without existential quantifiers makes modelling simpler - and we conjecture: computationally more efficient. This is one of the many open questions raised by our insights, and we conclude with an outlook on the research opportunities in this area.

Cite as

Markus Krötzsch, Maximilian Marx, and Sebastian Rudolph. The Power of the Terminating Chase (Invited Talk). In 22nd International Conference on Database Theory (ICDT 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 127, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{krotzsch_et_al:LIPIcs.ICDT.2019.3,
  author =	{Kr\"{o}tzsch, Markus and Marx, Maximilian and Rudolph, Sebastian},
  title =	{{The Power of the Terminating Chase}},
  booktitle =	{22nd International Conference on Database Theory (ICDT 2019)},
  pages =	{3:1--3:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-101-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{127},
  editor =	{Barcelo, Pablo and Calautti, Marco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2019.3},
  URN =		{urn:nbn:de:0030-drops-103057},
  doi =		{10.4230/LIPIcs.ICDT.2019.3},
  annote =	{Keywords: Existential rules, Tuple-generating dependencies, all-instances chase termination, expressive power, data complexity}
}
Document
Agnostic Learning from Tolerant Natural Proofs

Authors: Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova

Published in: LIPIcs, Volume 81, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)


Abstract
We generalize the "learning algorithms from natural properties" framework of [CIKK16] to get agnostic learning algorithms from natural properties with extra features. We show that if a natural property (in the sense of Razborov and Rudich [RR97]) is useful also against functions that are close to the class of "easy" functions, rather than just against "easy" functions, then it can be used to get an agnostic learning algorithm over the uniform distribution with membership queries. * For AC0[q], any prime q (constant-depth circuits of polynomial size, with AND, OR, NOT, and MODq gates of unbounded fanin), which happens to have a natural property with the requisite extra feature by [Raz87, Smo87, RR97], we obtain the first agnostic learning algorithm for AC0[q], for every prime q. Our algorithm runs in randomized quasi-polynomial time, uses membership queries, and outputs a circuit for a given Boolean function f that agrees with f on all but at most polylog(n)*opt fraction of inputs, where opt is the relative distance between f and the closest function h in the class AC0[q]. * For the ideal case, a natural proof of strongly exponential correlation circuit lower bounds against a circuit class C containing AC0[2] (i.e., circuits of size exp(Omega(n)) cannot compute some n-variate function even with exp(-Omega(n)) advantage over random guessing) would yield a polynomial-time query agnostic learning algorithm for C with the approximation error O(opt).

Cite as

Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Agnostic Learning from Tolerant Natural Proofs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 81, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{carmosino_et_al:LIPIcs.APPROX-RANDOM.2017.35,
  author =	{Carmosino, Marco L. and Impagliazzo, Russell and Kabanets, Valentine and Kolokolova, Antonina},
  title =	{{Agnostic Learning from Tolerant Natural Proofs}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2017)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-044-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{81},
  editor =	{Jansen, Klaus and Rolim, Jos\'{e} D. P. and Williamson, David P. and Vempala, Santosh S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2017.35},
  URN =		{urn:nbn:de:0030-drops-75842},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2017.35},
  annote =	{Keywords: agnostic learning, natural proofs, circuit lower bounds, meta-algorithms, AC0\lbrackq\rbrack, Nisan-Wigderson generator}
}
Document
Multiparty Session Types as Coherence Proofs

Authors: Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)


Abstract
We propose a Curry-Howard correspondence between a language for programming multiparty sessions and a generalisation of Classical Linear Logic (CLL). In this framework, propositions correspond to the local behaviour of a participant in a multiparty session type, proofs to processes, and proof normalisation to executing communications. Our key contribution is generalising duality, from CLL, to a new notion of n-ary compatibility, called coherence. Building on coherence as a principle of compositionality, we generalise the cut rule of CLL to a new rule for composing many processes communicating in a multiparty session. We prove the soundness of our model by showing the admissibility of our new rule, which entails deadlock-freedom via our correspondence.

Cite as

Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. Multiparty Session Types as Coherence Proofs. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 412-426, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{carbone_et_al:LIPIcs.CONCUR.2015.412,
  author =	{Carbone, Marco and Montesi, Fabrizio and Sch\"{u}rmann, Carsten and Yoshida, Nobuko},
  title =	{{Multiparty Session Types as Coherence Proofs}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{412--426},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.412},
  URN =		{urn:nbn:de:0030-drops-53661},
  doi =		{10.4230/LIPIcs.CONCUR.2015.412},
  annote =	{Keywords: Programming languages, Type systems, Session Types, Linear Logic}
}
  • Refine by Author
  • 2 Montesi, Fabrizio
  • 1 Bayer, Jonas
  • 1 Calamai, Marco
  • 1 Carbone, Marco
  • 1 Carmosino, Marco L.
  • Show More...

  • Refine by Classification
  • 1 Security and privacy
  • 1 Software and its engineering → Concurrent programming languages
  • 1 Software and its engineering → Distributed programming languages
  • 1 Software and its engineering → Multiparadigm languages
  • 1 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 1 AC0[q]
  • 1 Choreographies
  • 1 DPRM theorem
  • 1 Diophantine predicates
  • 1 Distributed Programming
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 2 2019
  • 2 2021
  • 1 2015
  • 1 2017
  • 1 2020

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