7 Search Results for "Nguyen, L� Th�nh Dung"

Document
DOI: 10.4230/LIPIcs.CSL.2024.40
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
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.117
Algebraic Recognition of Regular Functions

Authors: Mikołaj Bojańczyk and Lê Thành Dũng (Tito) Nguyễn

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
We consider regular string-to-string functions, i.e. functions that are recognized by copyless streaming string transducers, or any of their equivalent models, such as deterministic two-way automata. We give yet another characterization, which is very succinct: finiteness-preserving functors from the category of semigroups to itself, together with a certain output function that is a natural transformation.
Cite as

Mikołaj Bojańczyk and Lê Thành Dũng (Tito) Nguyễn. Algebraic Recognition of Regular Functions. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 117:1-117:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bojanczyk_et_al:LIPIcs.ICALP.2023.117,
  author =	{Boja\'{n}czyk, Miko{\l}aj and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito)},
  title =	{{Algebraic Recognition of Regular Functions}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{117:1--117:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.117},
  URN =		{urn:nbn:de:0030-drops-181697},
  doi =		{10.4230/LIPIcs.ICALP.2023.117},
  annote =	{Keywords: string transducers, semigroups, category theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.32
BV and Pomset Logic Are Not the Same

Authors: Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger

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

Abstract
BV and pomset logic are two logics that both conservatively extend unit-free multiplicative linear logic by a third binary connective, which (i) is non-commutative, (ii) is self-dual, and (iii) lies between the "par" and the "tensor". It was conjectured early on (more than 20 years ago), that these two logics, that share the same language, that both admit cut elimination, and whose connectives have essentially the same properties, are in fact the same. In this paper we show that this is not the case. We present a formula that is provable in pomset logic but not in BV.
Cite as

Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.CSL.2022.32,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Stra{\ss}burger, Lutz},
  title =	{{BV and Pomset Logic Are Not the Same}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{32:1--32:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.32},
  URN =		{urn:nbn:de:0030-drops-157521},
  doi =		{10.4230/LIPIcs.CSL.2022.32},
  annote =	{Keywords: proof nets, deep inference, pomset logic, system BV, cographs, dicographs, series-parallel orders}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.139
Comparison-Free Polyregular Functions

Authors: Lê Thành Dũng (Tito) Nguyễn, Camille Noûs, and Pierre Pradic

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
This paper introduces a new automata-theoretic class of string-to-string functions with polynomial growth. Several equivalent definitions are provided: a machine model which is a restricted variant of pebble transducers, and a few inductive definitions that close the class of regular functions under certain operations. Our motivation for studying this class comes from another characterization, which we merely mention here but prove elsewhere, based on a λ-calculus with a linear type system. As their name suggests, these comparison-free polyregular functions form a subclass of polyregular functions; we prove that the inclusion is strict. We also show that they are incomparable with HDT0L transductions, closed under usual function composition - but not under a certain "map" combinator - and satisfy a comparison-free version of the pebble minimization theorem. On the broader topic of polynomial growth transductions, we also consider the recently introduced layered streaming string transducers (SSTs), or equivalently k-marble transducers. We prove that a function can be obtained by composing such transducers together if and only if it is polyregular, and that k-layered SSTs (or k-marble transducers) are closed under "map" and equivalent to a corresponding notion of (k+1)-layered HDT0L systems.
Cite as

Lê Thành Dũng (Tito) Nguyễn, Camille Noûs, and Pierre Pradic. Comparison-Free Polyregular Functions. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 139:1-139:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.ICALP.2021.139,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and No\^{u}s, Camille and Pradic, Pierre},
  title =	{{Comparison-Free Polyregular Functions}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{139:1--139:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.139},
  URN =		{urn:nbn:de:0030-drops-142087},
  doi =		{10.4230/LIPIcs.ICALP.2021.139},
  annote =	{Keywords: pebble transducers, HDT0L systems, polyregular functions}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.135
Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic

Authors: Lê Thành Dũng Nguyễn and Pierre Pradic

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

Abstract
We give a characterization of star-free languages in a λ-calculus with support for non-commutative affine types (in the sense of linear logic), via the algebraic characterization of the former using aperiodic monoids. When the type system is made commutative, we show that we get regular languages instead. A key ingredient in our approach – that it shares with higher-order model checking – is the use of Church encodings for inputs and outputs. Our result is, to our knowledge, the first use of non-commutativity in implicit computational complexity.
Cite as

Lê Thành Dũng Nguyễn and Pierre Pradic. Implicit Automata in Typed λ-Calculi I: Aperiodicity in a Non-Commutative Logic. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 135:1-135:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.ICALP.2020.135,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng and Pradic, Pierre},
  title =	{{Implicit Automata in Typed \lambda-Calculi I: Aperiodicity in a Non-Commutative Logic}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{135:1--135:20},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.135},
  URN =		{urn:nbn:de:0030-drops-125426},
  doi =		{10.4230/LIPIcs.ICALP.2020.135},
  annote =	{Keywords: Church encodings, ordered linear types, star-free languages}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.123
From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Lê Thành Dũng Nguyễn and Pierre Pradic

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.
Cite as

Lê Thành Dũng Nguyễn and Pierre Pradic. From Normal Functors to Logarithmic Space Queries (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 123:1-123:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.ICALP.2019.123,
  author =	{Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng and Pradic, Pierre},
  title =	{{From Normal Functors to Logarithmic Space Queries}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{123:1--123:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.123},
  URN =		{urn:nbn:de:0030-drops-106994},
  doi =		{10.4230/LIPIcs.ICALP.2019.123},
  annote =	{Keywords: coherence spaces, elementary linear logic, semantic evaluation}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.25
Unique perfect matchings and proof nets

Authors: Lê Thành Dung Nguyen

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
This paper establishes a bridge between linear logic and mainstream graph theory, building previous work by Retoré (2003). We show that the problem of correctness for MLL+Mix proof nets is equivalent to the problem of uniqueness of a perfect matching. By applying matching theory, we obtain new results for MLL+Mix proof nets: a linear-time correctness criterion, a quasi-linear sequentialization algorithm, and a characterization of the sub-polynomial complexity of the correctness problem. We also use graph algorithms to compute the dependency relation of Bagnol et al. (2015) and the kingdom ordering of Bellin (1997), and relate them to the notion of blossom which is central to combinatorial maximum matching algorithms.
Cite as

Lê Thành Dung Nguyen. Unique perfect matchings and proof nets. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{nguyen:LIPIcs.FSCD.2018.25,
  author =	{Nguyen, L\^{e} Th\`{a}nh Dung},
  title =	{{Unique perfect matchings and proof nets}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{25:1--25:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.25},
  URN =		{urn:nbn:de:0030-drops-91957},
  doi =		{10.4230/LIPIcs.FSCD.2018.25},
  annote =	{Keywords: correctness criteria, matching algorithms}
}
  • Refine by Author
  • 4 Nguyễn, Lê Thành Dũng (Tito)
  • 3 Pradic, Pierre
  • 2 Nguyễn, Lê Thành Dũng
  • 1 Bojańczyk, Mikołaj
  • 1 Moreau, Vincent
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Linear logic
  • 2 Theory of computation → Transducers
  • 1 Mathematics of computing → Graph algorithms
  • 1 Mathematics of computing → Matchings and factors
  • 1 Theory of computation → Algebraic language theory
  • Show More...

  • Refine by Keyword
  • 1 Church encodings
  • 1 HDT0L systems
  • 1 category theory
  • 1 cographs
  • 1 coherence spaces
  • Show More...

  • Refine by Type
  • 7 document

  • Refine by Publication Year
  • 1 2018
  • 1 2019
  • 1 2020
  • 1 2021
  • 1 2022
  • 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact