Search Results

Documents authored by Faggian, Claudia

Document
DOI: 10.4230/LIPIcs.CSL.2025.47
A Rewriting Theory for Quantum λ-Calculus

Authors: Claudia Faggian, Gaetan Lopez, and Benoît Valiron

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.
Cite as

Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{faggian_et_al:LIPIcs.CSL.2025.47,
  author =	{Faggian, Claudia and Lopez, Gaetan and Valiron, Beno\^{i}t},
  title =	{{A Rewriting Theory for Quantum \lambda-Calculus}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{47:1--47:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.47},
  URN =		{urn:nbn:de:0030-drops-228046},
  doi =		{10.4230/LIPIcs.CSL.2025.47},
  annote =	{Keywords: quantum lambda-calculus, probabilistic rewriting, operational semantics, asymptotic normalization, principles of quantum programming languages}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.8
The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic

Authors: Thomas Ehrhard, Claudia Faggian, and Michele Pagani

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

Abstract
We consider an extension of multiplicative linear logic which encompasses bayesian networks and expresses samples sharing and marginalisation with the polarised rules of contraction and weakening. We introduce the necessary formalism to import exact inference algorithms from bayesian networks, giving the sum-product algorithm as an example of calculating the weighted relational semantics of a multiplicative proof-net improving runtime performance by storing intermediate results.
Cite as

Thomas Ehrhard, Claudia Faggian, and Michele Pagani. The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ehrhard_et_al:LIPIcs.FSCD.2023.8,
  author =	{Ehrhard, Thomas and Faggian, Claudia and Pagani, Michele},
  title =	{{The Sum-Product Algorithm For Quantitative Multiplicative Linear Logic}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{8:1--8:18},
  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.8},
  URN =		{urn:nbn:de:0030-drops-179926},
  doi =		{10.4230/LIPIcs.FSCD.2023.8},
  annote =	{Keywords: Linear Logic, Proof-Nets, Denotational Semantics, Probabilistic Programming}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2023.1
Asymptotic Rewriting (Invited Talk)

Authors: Claudia Faggian

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

Abstract
Rewriting is a foundation for the operational theory of programming languages. The process of rewriting describes the computation of a result (typically, a normal form), with lambda-calculus being the paradigmatic example for rewriting as an abstract form of program execution. Taking this view, the execution of a program is formalized as a specific evaluation strategy, while the general rewriting theory allows for program transformations, optimizations, parallel/distributed implementations, and provides a base on which to reason about program equivalence. In this talk, we discuss what happens when the notion of termination is asymptotic, that is, the result of computation appears as a limit, as opposed to reaching a normal form in a finite number of steps. - Example 1. A natural example is probabilistic computation. A probabilistic program P is a stochastic model generating a distribution over all possible outputs of P. Even if the termination probability is 1 (almost sure termination), that degree of certitude is typically not reached in a finite number of steps, but as a limit. A standard example is a term M that reduces to either a normal form or M itself, with equal probability 1/2. After n steps, M is in normal form with probability 1/2 + 1/(2²) + … + 1/(2ⁿ). Only at the limit this computation terminates with probability 1. - Example 2. Infinitary lambda-calculi (where the limits are infinitary terms such as Böhm trees), streams, algebraic rewriting systems, effectful computation (e.g. computation with outputs), quantum lambda-calculi provide several other relevant examples. Instances of asymptotic computation are quite diverse, and moreover the specific syntax of each system may be rather complex. In the talk, we present asymptotic rewriting in a way which is independent of the specific details of each calculus, and we provide a toolkit of proof-techniques which are of general application. To do so, we rely on Quantitative Abstract Rewriting System [Claudia Faggian, 2022; Claudia Faggian and Giulio Guerrieri, 2022], building on work by Ariola and Blom [Ariola and Blom, 2002], which enrich with quantitative information the theory of Abstract Rewriting Systems (ARS) (see e.g. [Terese, 2003] or [Baader and Nipkow, 1998]). ARS are indeed the core of finitary rewriting, capturing the common substratum of rewriting theory and term transformation, independently from the particular structure of the objects. It seems then natural to seek a similar foundation for asymptotic computation. The issue is that the arguments relying on finitary termination do not transfer, in general, to limits (a game changer being that asymptotic termination does not provide a well-founded order): we need to develope an opportune formalization and suitable proof techniques. The goal is then to identify and develop methods which only rely on the asymptotic argument - abstracting from structure specific to a setting - and so will apply to any concrete instance. For example, in infinitary lambda calculus, the limit is usually a (possibly infinite) limit term, while in probabilistic lambda calculus, the limit is a distribution over (finite) terms. The former is concerned with the depth of the redexes, the latter with the probability of reaching a result. The abstract notions of limit and of normalization subsumes both, and so abstract results apply to either setting.
Cite as

Claudia Faggian. Asymptotic Rewriting (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{faggian:LIPIcs.CSL.2023.1,
  author =	{Faggian, Claudia},
  title =	{{Asymptotic Rewriting}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{1:1--1:2},
  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.1},
  URN =		{urn:nbn:de:0030-drops-174621},
  doi =		{10.4230/LIPIcs.CSL.2023.1},
  annote =	{Keywords: rewriting, probabilistic rewriting, confluence, strategies, asymptotic normalization, lambda calculus}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.17
Strategies for Asymptotic Normalization

Authors: Claudia Faggian and Giulio Guerrieri

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
We present an abstract technique to study normalizing strategies when termination is asymptotic, that is, it appears as a limit. Asymptotic termination occurs in several settings, such as effectful, and in particular probabilistic computation - where the limits are distributions over the possible outputs - or infinitary lambda-calculi - where the limits are infinitary terms such as Böhm trees. As a concrete application, we obtain a result which is of independent interest: a normalization theorem for Call-by-Value (and - in a uniform way - for Call-by-Name) probabilistic lambda-calculus.
Cite as

Claudia Faggian and Giulio Guerrieri. Strategies for Asymptotic Normalization. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 17:1-17:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{faggian_et_al:LIPIcs.FSCD.2022.17,
  author =	{Faggian, Claudia and Guerrieri, Giulio},
  title =	{{Strategies for Asymptotic Normalization}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{17:1--17:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.17},
  URN =		{urn:nbn:de:0030-drops-162987},
  doi =		{10.4230/LIPIcs.FSCD.2022.17},
  annote =	{Keywords: rewriting, strategies, normalization, lambda calculus, probabilistic rewriting}
}
Document
DOI: 10.4230/LIPIcs.CSL.2021.6
Factorize Factorization

Authors: Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
We present a new technique for proving factorization theorems for compound rewriting systems in a modular way, which is inspired by the Hindley-Rosen technique for confluence. Specifically, our approach is well adapted to deal with extensions of the call-by-name and call-by-value λ-calculi. The technique is first developed abstractly. We isolate a sufficient condition (called linear swap) for lifting factorization from components to the compound system, and which is compatible with β-reduction. We then closely analyze some common factorization schemas for the λ-calculus. Concretely, we apply our technique to diverse extensions of the λ-calculus, among which de' Liguoro and Piperno’s non-deterministic λ-calculus and - for call-by-value - Carraro and Guerrieri’s shuffling calculus. For both calculi the literature contains factorization theorems. In both cases, we give a new proof which is neat, simpler than the original, and strikingly shorter.
Cite as

Beniamino Accattoli, Claudia Faggian, and Giulio Guerrieri. Factorize Factorization. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.CSL.2021.6,
  author =	{Accattoli, Beniamino and Faggian, Claudia and Guerrieri, Giulio},
  title =	{{Factorize Factorization}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.6},
  URN =		{urn:nbn:de:0030-drops-134407},
  doi =		{10.4230/LIPIcs.CSL.2021.6},
  annote =	{Keywords: Lambda Calculus, Rewriting, Reduction Strategies, Factorization}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2020.1
Solvability in a Probabilistic Setting (Invited Talk)

Authors: Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian

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

Abstract
The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ_⊕, itself induced by the type system, which equates all the unsolvable terms.
Cite as

Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian. Solvability in a Probabilistic Setting (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ronchidellarocca_et_al:LIPIcs.FSCD.2020.1,
  author =	{Ronchi Della Rocca, Simona and Dal Lago, Ugo and Faggian, Claudia},
  title =	{{Solvability in a Probabilistic Setting}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{1:1--1:17},
  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.1},
  URN =		{urn:nbn:de:0030-drops-123237},
  doi =		{10.4230/LIPIcs.FSCD.2020.1},
  annote =	{Keywords: Probabilistic Computation, Lambda Calculus, Solvability, Intersection Types}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.19
Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms

Authors: Claudia Faggian

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. We study in this setting questions such as uniqueness of the result (unique limit distribution) and normalizing strategies (is there a strategy to find a result with greatest probability?). The goal is to have tools to analyse the operational properties of probabilistic calculi (such as probabilistic lambda-calculi) whose evaluation is also non-deterministic, in the sense that different reductions are possible.
Cite as

Claudia Faggian. Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 19:1-19:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{faggian:LIPIcs.FSCD.2019.19,
  author =	{Faggian, Claudia},
  title =	{{Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{19:1--19:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.19},
  URN =		{urn:nbn:de:0030-drops-105263},
  doi =		{10.4230/LIPIcs.FSCD.2019.19},
  annote =	{Keywords: probabilistic rewriting, PARS, abstract rewriting systems, confluence, probabilistic lambda calculus}
}
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 About DROPS Imprint Privacy Contact