9 Search Results for "Mellies, Paul-Andre"


Document
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations

Authors: Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn

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


Abstract
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed λ-terms, defined using denotational semantics in finite sets. We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic λ-definability. Second, we show that any finitary extensional model of the simply typed λ-calculus, when used in Salvati’s definition, recognizes exactly the same class of languages of λ-terms as the category of finite sets does. The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.

Cite as

Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn. Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 40:1-40:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{moreau_et_al:LIPIcs.CSL.2024.40,
  author =	{Moreau, Vincent and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito)},
  title =	{{Syntactically and Semantically Regular Languages of \lambda-Terms Coincide Through Logical Relations}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{40:1--40:22},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.40},
  URN =		{urn:nbn:de:0030-drops-196831},
  doi =		{10.4230/LIPIcs.CSL.2024.40},
  annote =	{Keywords: regular languages, simple types, denotational semantics, logical relations}
}
Document
Convolution Products on Double Categories and Categorification of Rule Algebras

Authors: Nicolas Behr, Paul-André Melliès, and Noam Zeilberger

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


Abstract
Motivated by compositional categorical rewriting theory, we introduce a convolution product over presheaves of double categories which generalizes the usual Day tensor product of presheaves of monoidal categories. One interesting aspect of the construction is that this convolution product is in general only oplax associative. For that reason, we identify several classes of double categories for which the convolution product is not just oplax associative, but fully associative. This includes in particular framed bicategories on the one hand, and double categories of compositional rewriting theories on the other. For the latter, we establish a formula which justifies the view that the convolution product categorifies the rule algebra product.

Cite as

Nicolas Behr, Paul-André Melliès, and Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{behr_et_al:LIPIcs.FSCD.2023.17,
  author =	{Behr, Nicolas and Melli\`{e}s, Paul-Andr\'{e} and Zeilberger, Noam},
  title =	{{Convolution Products on Double Categories and Categorification of Rule Algebras}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{17:1--17:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.17},
  URN =		{urn:nbn:de:0030-drops-180017},
  doi =		{10.4230/LIPIcs.FSCD.2023.17},
  annote =	{Keywords: Categorical rewriting, double pushout, sesqui-pushout, double categories, convolution product, presheaf categories, framed bicategories, opfibrations, rule algebra}
}
Document
Coderelictions for Free Exponential Modalities

Authors: Jean-Simon Pacaud Lemay

Published in: LIPIcs, Volume 211, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)


Abstract
In a categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (MELL), the exponential modality is interpreted as a comonad ! such that each cofree !-coalgebra !A comes equipped with a natural cocommutative comonoid structure. An important case is when ! is a free exponential modality so that !A is the cofree cocommutative comonoid over A. A categorical model of MELL with a free exponential modality is called a Lafont category. A categorical model of differential linear logic is called a differential category, where the differential structure can equivalently be described by a deriving transformation !A⊗A →{𝖽_A} !A or a codereliction A →{η_A} !A. Blute, Lucyshyn-Wright, and O'Neill showed that every Lafont category with finite biproducts is a differential category. However, from a differential linear logic perspective, Blute, Lucyshyn-Wright, and O'Neill’s approach is not the usual one since the result was stated in the dual setting and the proof is in terms of the deriving transformation 𝖽. In differential linear logic, it is often the codereliction η that is preferred and that plays a more prominent role. In this paper, we provide an alternative proof that every Lafont category (with finite biproducts) is a differential category, where we construct the codereliction η using the couniversal property of the cofree cocommtuative comonoid !A and show that η is unique. To achieve this, we introduce the notion of an infinitesimal augmentation k⊕A →{𝖧_A} !(k ⊕ A), which in particular is a !-coalgebra and a comonoid morphism, and show that infinitesimal augmentations are in bijective correspondence to coderelictions (and deriving transformations). As such, infinitesimal augmentations provide a new equivalent axiomatization for differential categories in terms of more commonly known concepts. For a free exponential modality, its infinitesimal augmentation is easy to construct and allows one to clearly see the differential structure of a Lafont category, regardless of the construction of !A.

Cite as

Jean-Simon Pacaud Lemay. Coderelictions for Free Exponential Modalities. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{lemay:LIPIcs.CALCO.2021.19,
  author =	{Lemay, Jean-Simon Pacaud},
  title =	{{Coderelictions for Free Exponential Modalities}},
  booktitle =	{9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},
  pages =	{19:1--19:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-212-9},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{211},
  editor =	{Gadducci, Fabio and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19},
  URN =		{urn:nbn:de:0030-drops-153742},
  doi =		{10.4230/LIPIcs.CALCO.2021.19},
  annote =	{Keywords: Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations}
}
Document
Comprehension and Quotient Structures in the Language of 2-Categories

Authors: Paul-André Melliès and Nicolas Rolland

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


Abstract
Lawvere observed in his celebrated work on hyperdoctrines that the set-theoretic schema of comprehension can be elegantly expressed in the functorial language of categorical logic, as a comprehension structure on the functor p:E→ B defining the hyperdoctrine. In this paper, we formulate and study a strictly ordered hierarchy of three notions of comprehension structure on a given functor p:E→ B, which we call (i) comprehension structure, (ii) comprehension structure with section, and (iii) comprehension structure with image. Our approach is 2-categorical and we thus formulate the three levels of comprehension structure on a general morphism p:𝐄→𝐁 in a 2-category K. This conceptual point of view on comprehension structures enables us to revisit the work by Fumex, Ghani and Johann on the duality between comprehension structures and quotient structures on a given functor p:E→B. In particular, we show how to lift the comprehension and quotient structures on a functor p:E→ B to the categories of algebras or coalgebras associated to functors F_E:E→E and F_B:B→B of interest, in order to interpret reasoning by induction and coinduction in the traditional language of categorical logic, formulated in an appropriate 2-categorical way.

Cite as

Paul-André Melliès and Nicolas Rolland. Comprehension and Quotient Structures in the Language of 2-Categories. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{mellies_et_al:LIPIcs.FSCD.2020.6,
  author =	{Melli\`{e}s, Paul-Andr\'{e} and Rolland, Nicolas},
  title =	{{Comprehension and Quotient Structures in the Language of 2-Categories}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{6:1--6:18},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.6},
  URN =		{urn:nbn:de:0030-drops-123282},
  doi =		{10.4230/LIPIcs.FSCD.2020.6},
  annote =	{Keywords: Comprehension structures, quotient structures, comprehension structures with section, comprehension structures with image, 2-categories, formal adjunctions, path objects, categorical logic, inductive reasoning on algebras, coinductive reasoning on coalgebras}
}
Document
Differentials and Distances in Probabilistic Coherence Spaces

Authors: Thomas Ehrhard

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


Abstract
In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.

Cite as

Thomas Ehrhard. Differentials and Distances in Probabilistic Coherence Spaces. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{ehrhard:LIPIcs.FSCD.2019.17,
  author =	{Ehrhard, Thomas},
  title =	{{Differentials and Distances in Probabilistic Coherence Spaces}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{17:1--17:17},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.17},
  URN =		{urn:nbn:de:0030-drops-105243},
  doi =		{10.4230/LIPIcs.FSCD.2019.17},
  annote =	{Keywords: Denotational semantics, probabilistic coherence spaces, differentials of programs}
}
Document
Relational Semantics of Linear Logic and Higher-order Model Checking

Authors: Charles Grellois and Paul-André Melliès

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)


Abstract
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higher-order model-checking. We show in particular how to reunderstand in this way the type-theoretic approach to higher-order model-checking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic second-order logic for higher-order recursion schemes.

Cite as

Charles Grellois and Paul-André Melliès. Relational Semantics of Linear Logic and Higher-order Model Checking. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 260-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{grellois_et_al:LIPIcs.CSL.2015.260,
  author =	{Grellois, Charles and Melli\`{e}s, Paul-Andr\'{e}},
  title =	{{Relational Semantics of Linear Logic and Higher-order Model Checking}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{260--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.260},
  URN =		{urn:nbn:de:0030-drops-54190},
  doi =		{10.4230/LIPIcs.CSL.2015.260},
  annote =	{Keywords: Higher-order model-checking, linear logic, relational semantics, parity games, parametric comonads.}
}
Document
On dialogue games and coherent strategies

Authors: Paul-André Melliès

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)


Abstract
We explain how to see the set of positions of a dialogue game as a coherence space in the sense of Girard or as a bistructure in the sense of Curien, Plotkin and Winskel. The coherence structure on the set of positions results from a Kripke translation of tensorial logic into linear logic extended with a necessity modality. The translation is done in such a way that every innocent strategy defines a clique or a configuration in the resulting space of positions. This leads us to study the notion of configuration designed by Curien, Plotkin and Winskel for general bistructures in the particular case of a bistructure associated to a dialogue game. We show that every such configuration may be seen as an interactive strategy equipped with a backward as well as a forward dynamics based on the interplay between the stable order and the extensional order. In that way, the category of bistructures is shown to include a full subcategory of games and coherent strategies of an interesting nature.

Cite as

Paul-André Melliès. On dialogue games and coherent strategies. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 540-562, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Copy BibTex To Clipboard

@InProceedings{mellies:LIPIcs.CSL.2013.540,
  author =	{Melli\`{e}s, Paul-Andr\'{e}},
  title =	{{On dialogue games and coherent strategies}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{540--562},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.540},
  URN =		{urn:nbn:de:0030-drops-42181},
  doi =		{10.4230/LIPIcs.CSL.2013.540},
  annote =	{Keywords: Game semantics, Stable order, Extensional order, Bistructures, Tensorial logic, Innocent strategies}
}
Document
10252 Abstracts Collection – Game Semantics and Program Verification

Authors: Paul-Andre Mellies, Andrzej S. Murawski, Andrea Schalk, and Igor Walukiewicz

Published in: Dagstuhl Seminar Proceedings, Volume 10252, Game Semantics and Program Verification (2010)


Abstract
From 20th to 25th June 2010, the Dagstuhl Seminar "Game Semantics and Program Verification'' was held in Schloss Dagstuhl - Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Paul-Andre Mellies, Andrzej S. Murawski, Andrea Schalk, and Igor Walukiewicz. 10252 Abstracts Collection – Game Semantics and Program Verification. In Game Semantics and Program Verification. Dagstuhl Seminar Proceedings, Volume 10252, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{mellies_et_al:DagSemProc.10252.1,
  author =	{Mellies, Paul-Andre and Murawski, Andrzej S. and Schalk, Andrea and Walukiewicz, Igor},
  title =	{{10252 Abstracts Collection – Game Semantics and Program Verification}},
  booktitle =	{Game Semantics and Program Verification},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10252},
  editor =	{Paul-Andre Mellies and Andrzej S. Murawski and Andrea Schalk and Igor Walukiewicz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10252.1},
  URN =		{urn:nbn:de:0030-drops-27945},
  doi =		{10.4230/DagSemProc.10252.1},
  annote =	{Keywords: Software verification, Semantics of programming languages, Game semantics, Static analysis, Model checking}
}
Document
10252 Executive Summary – Game Semantics and Program Verification

Authors: Paul-Andre Mellies, Andrzej S. Murawski, Andrea Schalk, and Igor Walukiewicz

Published in: Dagstuhl Seminar Proceedings, Volume 10252, Game Semantics and Program Verification (2010)


Abstract
The seminar took place from 20th until 25th June 2010. Its primary aim was to foster interaction between researchers working on modelling programs/proofs using games and the verification community. The meeting brought together 28 researchers from eight different countries, both junior and senior, for a systematic assessment of what the two areas have to offer to one another, critical evaluation of what has been achieved so far, with a view to establishing common research goals for the future.

Cite as

Paul-Andre Mellies, Andrzej S. Murawski, Andrea Schalk, and Igor Walukiewicz. 10252 Executive Summary – Game Semantics and Program Verification. In Game Semantics and Program Verification. Dagstuhl Seminar Proceedings, Volume 10252, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{mellies_et_al:DagSemProc.10252.2,
  author =	{Mellies, Paul-Andre and Murawski, Andrzej S. and Schalk, Andrea and Walukiewicz, Igor},
  title =	{{10252 Executive Summary – Game Semantics and Program Verification}},
  booktitle =	{Game Semantics and Program Verification},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10252},
  editor =	{Paul-Andre Mellies and Andrzej S. Murawski and Andrea Schalk and Igor Walukiewicz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10252.2},
  URN =		{urn:nbn:de:0030-drops-27938},
  doi =		{10.4230/DagSemProc.10252.2},
  annote =	{Keywords: Software verification, Semantics of programming languages, Game semantics, Static analysis, Model checking}
}
  • Refine by Author
  • 4 Melliès, Paul-André
  • 2 Mellies, Paul-Andre
  • 2 Murawski, Andrzej S.
  • 2 Schalk, Andrea
  • 2 Walukiewicz, Igor
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Linear logic
  • 2 Theory of computation → Categorical semantics
  • 1 Theory of computation → Abstract machines
  • 1 Theory of computation → Denotational semantics
  • 1 Theory of computation → Lambda calculus
  • Show More...

  • Refine by Keyword
  • 3 Game semantics
  • 2 Model checking
  • 2 Semantics of programming languages
  • 2 Software verification
  • 2 Static analysis
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 2 2010
  • 1 2013
  • 1 2015
  • 1 2019
  • 1 2020
  • Show More...

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