25 Search Results for "Dal Lago, Ugo"

Document
DOI: 10.4230/LIPIcs.FSCD.2024.19
Semantics for a Turing-Complete Reversible Programming Language with Inductive Types

Authors: Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We show how one can encode any Reversible Turing Machine in said language. We then build a sound and adequate categorical semantics based on join inverse categories, with additional structures to capture pattern-matching and to interpret inductive types and recursion. We then derive a notion of completeness in the sense that any computable, partial, first-order injective function is the image of a term in the language.
Cite as

Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chardonnet_et_al:LIPIcs.FSCD.2024.19,
  author =	{Chardonnet, Kostia and Lemonnier, Louis and Valiron, Beno\^{i}t},
  title =	{{Semantics for a Turing-Complete Reversible Programming Language with Inductive Types}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{19:1--19:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.19},
  URN =		{urn:nbn:de:0030-drops-203487},
  doi =		{10.4230/LIPIcs.FSCD.2024.19},
  annote =	{Keywords: Reversible programming, functional programming, Computability, Denotational Semantics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.23
Mirroring Call-By-Need, or Values Acting Silly

Authors: Beniamino Accattoli and Adrienne Lancelot

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Call-by-need evaluation for the λ-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need - that is, its operational equivalence with call-by-name - showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
Cite as

Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23,
  author =	{Accattoli, Beniamino and Lancelot, Adrienne},
  title =	{{Mirroring Call-By-Need, or Values Acting Silly}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.23},
  URN =		{urn:nbn:de:0030-drops-203527},
  doi =		{10.4230/LIPIcs.FSCD.2024.23},
  annote =	{Keywords: Lambda calculus, intersection types, call-by-value, call-by-need}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.24
IMELL Cut Elimination with Linear Overhead

Authors: Beniamino Accattoli and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Recently, Accattoli introduced the Exponential Substitution Calculus (ESC) given by untyped proof terms for Intuitionistic Multiplicative Exponential Linear Logic (IMELL), endowed with rewriting rules at-a-distance for cut elimination. He also introduced a new cut elimination strategy, dubbed the good strategy, and showed that its number of steps is a time cost model with polynomial overhead for ESC/IMELL, and the first such one. Here, we refine Accattoli’s result by introducing an abstract machine for ESC and proving that it implements the good strategy and computes cut-free terms/proofs within a linear overhead.
Cite as

Beniamino Accattoli and Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 24:1-24:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.24,
  author =	{Accattoli, Beniamino and Sacerdoti Coen, Claudio},
  title =	{{IMELL Cut Elimination with Linear Overhead}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{24:1--24:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.24},
  URN =		{urn:nbn:de:0030-drops-203539},
  doi =		{10.4230/LIPIcs.FSCD.2024.24},
  annote =	{Keywords: Lambda calculus, linear logic, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.29
Böhm and Taylor for All!

Authors: Aloÿs Dufour and Damiano Mazza

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Böhm approximations, used in the definition of Böhm trees, are a staple of the semantics of the lambda-calculus. Introduced more recently by Ehrhard and Regnier, Taylor approximations provide a quantitative account of the behavior of programs and are well-known to be connected to intersection types. The key relation between these two notions of approximations is a commutation theorem, roughly stating that Taylor approximations of Böhm trees are the same as Böhm trees of Taylor approximations. Böhm and Taylor approximations are available for several variants or extensions of the lambda-calculus and, in some cases, commutation theorems are known. In this paper, we define Böhm and Taylor approximations and prove the commutation theorem in a very general setting. We also introduce (non-idempotent) intersection types at this level of generality. From this, we show how the commutation theorem and intersection types may be applied to any calculus embedding in a sufficiently nice way into our general calculus. All known Böhm-Taylor commutation theorems, as well as new ones, follow by this uniform construction.
Cite as

Aloÿs Dufour and Damiano Mazza. Böhm and Taylor for All!. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{dufour_et_al:LIPIcs.FSCD.2024.29,
  author =	{Dufour, Alo\"{y}s and Mazza, Damiano},
  title =	{{B\"{o}hm and Taylor for All!}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.29},
  URN =		{urn:nbn:de:0030-drops-203582},
  doi =		{10.4230/LIPIcs.FSCD.2024.29},
  annote =	{Keywords: Linear logic, Differential linear logic, Taylor expansion of lambda-terms, B\"{o}hm trees, Process calculi}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.14
Two-Dimensional Kripke Semantics I: Presheaves

Authors: G. A. Kavvos

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
The study of modal logic has witnessed tremendous development following the introduction of Kripke semantics. However, recent developments in programming languages and type theory have led to a second way of studying modalities, namely through their categorical semantics. We show how the two correspond.
Cite as

G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kavvos:LIPIcs.FSCD.2024.14,
  author =	{Kavvos, G. A.},
  title =	{{Two-Dimensional Kripke Semantics I: Presheaves}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.14},
  URN =		{urn:nbn:de:0030-drops-203438},
  doi =		{10.4230/LIPIcs.FSCD.2024.14},
  annote =	{Keywords: modal logic, categorical semantics, Kripke semantics, duality, open maps}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.10
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories

Authors: Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T, where T = IΔ₀+Exp is a well-studied theory based on bounded induction.
Cite as

Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone. Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{antonelli_et_al:LIPIcs.CSL.2024.10,
  author =	{Antonelli, Melissa and Dal Lago, Ugo and Davoli, Davide and Oitavem, Isabel and Pistone, Paolo},
  title =	{{Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.10},
  URN =		{urn:nbn:de:0030-drops-196538},
  doi =		{10.4230/LIPIcs.CSL.2024.10},
  annote =	{Keywords: Bounded Arithmetic, Randomized Computation, Implicit Computational Complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.38
Contextual Behavioural Metrics

Authors: Ugo Dal Lago and Maurizio Murgia

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and contextual information. This way, process distances by construction take the environment into account: two (non-equivalent) processes may still exhibit very similar behaviour in some contexts, e.g., when certain actions are never performed. We first show how CBMs capture many well-known notions of equivalence and metric, including Larsen’s environmental parametrized bisimulation. We then study compositional properties of CBMs with respect to some common process algebraic operators, namely prefixing, restriction, non-deterministic sum, parallel composition and replication.
Cite as

Ugo Dal Lago and Maurizio Murgia. Contextual Behavioural Metrics. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.CONCUR.2023.38,
  author =	{Dal Lago, Ugo and Murgia, Maurizio},
  title =	{{Contextual Behavioural Metrics}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{38:1--38:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.38},
  URN =		{urn:nbn:de:0030-drops-190320},
  doi =		{10.4230/LIPIcs.CONCUR.2023.38},
  annote =	{Keywords: Behavioural metrics, Labelled Transition Systems, Differential Semantics}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.3
On Dynamic Lifting and Effect Typing in Circuit Description Languages

Authors: Andrea Colledan and Ugo Dal Lago

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, which models the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.
Cite as

Andrea Colledan and Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{colledan_et_al:LIPIcs.TYPES.2022.3,
  author =	{Colledan, Andrea and Dal Lago, Ugo},
  title =	{{On Dynamic Lifting and Effect Typing in Circuit Description Languages}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.3},
  URN =		{urn:nbn:de:0030-drops-184468},
  doi =		{10.4230/LIPIcs.TYPES.2022.3},
  annote =	{Keywords: Circuit-Description Languages, \lambda-calculus, Dynamic lifting, Type and effect systems}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.20
On the Lattice of Program Metrics

Authors: Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone

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

Abstract
In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based on the interpretation of terms in metric spaces and those obtained by generalizing observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric refines another, in analogy with corresponding well-studied problems about program equivalences. The results we obtain are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie in between the observational and equational metrics and that in some cases, these inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, revealing that the former is less discriminating than the latter. All our results are given for a linear lambda-calculus, and some of them can be generalized to calculi with graded comonads, in the style of Fuzz.
Cite as

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Lattice of Program Metrics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2023.20,
  author =	{Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
  title =	{{On the Lattice of Program Metrics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{20:1--20:19},
  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.20},
  URN =		{urn:nbn:de:0030-drops-180049},
  doi =		{10.4230/LIPIcs.FSCD.2023.20},
  annote =	{Keywords: Metrics, Lambda Calculus, Linear Types}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.10
The Functional Machine Calculus II: Semantics

Authors: Chris Barrett, Willem Heijltjes, and Guy McCusker

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

Abstract
The Functional Machine Calculus (FMC), recently introduced by the second author, is a generalization of the lambda-calculus which may faithfully encode the effects of higher-order mutable store, I/O and probabilistic/non-deterministic input. Significantly, it remains confluent and can be simply typed in the presence of these effects. In this paper, we explore the denotational semantics of the FMC. We have three main contributions: first, we argue that its syntax - in which both effects and lambda-calculus are realised using the same syntactic constructs - is semantically natural, corresponding closely to the structure of a Scott-style domain theoretic semantics. Second, we show that simple types confer strong normalization by extending Gandy’s proof for the lambda-calculus, including a small simplification of the technique. Finally, we show that the typed FMC (without considering the specifics of encoded effects), modulo an appropriate equational theory, is a complete language for Cartesian closed categories.
Cite as

Chris Barrett, Willem Heijltjes, and Guy McCusker. The Functional Machine Calculus II: Semantics. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{barrett_et_al:LIPIcs.CSL.2023.10,
  author =	{Barrett, Chris and Heijltjes, Willem and McCusker, Guy},
  title =	{{The Functional Machine Calculus II: Semantics}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{10:1--10:18},
  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.10},
  URN =		{urn:nbn:de:0030-drops-174716},
  doi =		{10.4230/LIPIcs.CSL.2023.10},
  annote =	{Keywords: lambda-calculus, computational effects, denotational semantics, strong normalization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.17
Open Higher-Order Logic

Authors: Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen

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

Abstract
We introduce a variation on Barthe et al.’s higher-order logic in which formulas are interpreted as predicates over open rather than closed objects. This way, concepts which have an intrinsically functional nature, like continuity, differentiability, or monotonicity, can be expressed and reasoned about in a very natural way, following the structure of the underlying program. We give open higher-order logic in distinct flavors, and in particular in its relational and local versions, the latter being tailored for situations in which properties hold only in part of the underlying function’s domain of definition.
Cite as

Ugo Dal Lago, Francesco Gavazzo, and Alexis Ghyselen. Open Higher-Order Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.CSL.2023.17,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco and Ghyselen, Alexis},
  title =	{{Open Higher-Order Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{17:1--17:17},
  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.17},
  URN =		{urn:nbn:de:0030-drops-174785},
  doi =		{10.4230/LIPIcs.CSL.2023.17},
  annote =	{Keywords: Formal Verification, Relational Logic, First-Order Properties}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.37
On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments

Authors: Ugo Dal Lago and Giulia Giusti

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

Abstract
A system of session types is introduced as induced by a Curry Howard correspondence applied to bounded linear logic, suitably extended with probabilistic choice operators and ground types. The resulting system satisfies some expected properties, like subject reduction and progress, but also unexpected ones, like a polynomial bound on the time needed to reduce processes. This makes the system suitable for modelling experiments and proofs from the so-called computational model of cryptography.
Cite as

Ugo Dal Lago and Giulia Giusti. On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.CONCUR.2022.37,
  author =	{Dal Lago, Ugo and Giusti, Giulia},
  title =	{{On Session Typing, Probabilistic Polynomial Time, and Cryptographic Experiments}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{37:1--37:18},
  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.37},
  URN =		{urn:nbn:de:0030-drops-171000},
  doi =		{10.4230/LIPIcs.CONCUR.2022.37},
  annote =	{Keywords: Session Types, Probabilistic Computation, Bounded Linear Logic, Cryptographic Experiments}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.4
On Quantitative Algebraic Higher-Order Theories

Authors: Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone

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

Abstract
We explore the possibility of extending Mardare et al.’s quantitative algebras to the structures which naturally emerge from Combinatory Logic and the λ-calculus. First of all, we show that the framework is indeed applicable to those structures, and give soundness and completeness results. Then, we prove some negative results clearly delineating to which extent categories of metric spaces can be models of such theories. We conclude by giving several examples of non-trivial higher-order quantitative algebras.
Cite as

Ugo Dal Lago, Furio Honsell, Marina Lenisa, and Paolo Pistone. On Quantitative Algebraic Higher-Order Theories. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2022.4,
  author =	{Dal Lago, Ugo and Honsell, Furio and Lenisa, Marina and Pistone, Paolo},
  title =	{{On Quantitative Algebraic Higher-Order Theories}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{4:1--4:18},
  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.4},
  URN =		{urn:nbn:de:0030-drops-162851},
  doi =		{10.4230/LIPIcs.FSCD.2022.4},
  annote =	{Keywords: Quantitative Algebras, Lambda Calculus, Combinatory Logic, Metric Spaces}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.35
A Recursion-Theoretic Characterization of the Probabilistic Class PP

Authors: Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
Probabilistic complexity classes, despite capturing the notion of feasibility, have escaped any treatment by the tools of so-called implicit-complexity. Their inherently semantic nature is of course a barrier to the characterization of classes like BPP or ZPP, but not all classes are semantic. In this paper, we introduce a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.
Cite as

Ugo Dal Lago, Reinhard Kahle, and Isabel Oitavem. A Recursion-Theoretic Characterization of the Probabilistic Class PP. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 35:1-35:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.MFCS.2021.35,
  author =	{Dal Lago, Ugo and Kahle, Reinhard and Oitavem, Isabel},
  title =	{{A Recursion-Theoretic Characterization of the Probabilistic Class PP}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{35:1--35:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.35},
  URN =		{urn:nbn:de:0030-drops-144754},
  doi =		{10.4230/LIPIcs.MFCS.2021.35},
  annote =	{Keywords: Implicit complexity, tree-recursion, probabilistic classes, polynomial time, PP}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.23
Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs

Authors: Ugo Dal Lago and Francesco Gavazzo

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
We investigate program equivalence for linear higher-order (sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear λ-calculus with explicit copying and algebraic effects à la Plotkin and Power. Such a calculus makes explicit the interaction between copying and linearity, which are intensional aspects of computation, with effects, which are, instead, extensional. We review some of the notions of equivalences for linear calculi proposed in the literature and show their limitations when applied to effectful calculi where copying is a first-class citizen. We then introduce resource transition systems, namely transition systems whose states are built over tuples of programs representing the available resources, as an operational semantics accounting for both intensional and extensional interactive behaviours of programs. Our main result is a sound and complete characterization of contextual equivalence as trace equivalence defined on top of resource transition systems.
Cite as

Ugo Dal Lago and Francesco Gavazzo. Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2021.23,
  author =	{Dal Lago, Ugo and Gavazzo, Francesco},
  title =	{{Resource Transition Systems and Full Abstraction for Linear Higher-Order Effectful Programs}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{23:1--23:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.23},
  URN =		{urn:nbn:de:0030-drops-142618},
  doi =		{10.4230/LIPIcs.FSCD.2021.23},
  annote =	{Keywords: algebraic effects, linearity, program equivalence, full abstraction}
}
  • Refine by Author
  • 17 Dal Lago, Ugo
  • 3 Accattoli, Beniamino
  • 3 Gavazzo, Francesco
  • 3 Pistone, Paolo
  • 2 Oitavem, Isabel
  • Show More...

  • Refine by Classification
  • 7 Theory of computation → Lambda calculus
  • 5 Theory of computation → Operational semantics
  • 4 Theory of computation → Program semantics
  • 3 Theory of computation → Process calculi
  • 2 Theory of computation → Denotational semantics
  • Show More...

  • Refine by Keyword
  • 4 Lambda Calculus
  • 2 Lambda calculus
  • 2 Probabilistic Computation
  • 2 implicit computational complexity
  • 2 polynomial time
  • Show More...

  • Refine by Type
  • 25 document

  • Refine by Publication Year
  • 6 2024
  • 5 2023
  • 3 2021
  • 2 2012
  • 2 2015
  • Show More...

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact