مؤتمر
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations
| العنوان: | Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations |
|---|---|
| المؤلفون: | Moreau, Vincent, Nguyễn, Lê Thành Dũng |
| المساهمون: | Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Les assistants à la démonstration au cœur du raisonnement mathématique (PICUBE), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Preuves et Langages (PLUME), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Lê Thành D˜ung (Tito) Nguy ˜ên: Supported by the LABEX MILYON (ANR-10-LABX-0070)of Université de Lyon, within the program “Investissements d’Avenir” (ANR-11-IDEX-0007) operatedby the French National Research Agency (ANR), ANR-10-LABX-0070,MILYON,Community of mathematics and fundamental computer science in Lyon(2010), ANR-11-IDEX-0007,Avenir L.S.E.,PROJET AVENIR LYON SAINT-ETIENNE(2011) |
| المصدر: | 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) https://hal.science/hal-04447910Test 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), Feb 2024, Naples, Italy. pp.40:1-40:22, ⟨10.4230/LIPIcs.CSL.2024.40⟩ |
| بيانات النشر: | HAL CCSD Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| سنة النشر: | 2024 |
| مصطلحات موضوعية: | Simple types, Denotational semantics, Logical relations, Regular languages, [INFO]Computer Science [cs] |
| جغرافية الموضوع: | Naples, Italy |
| الوصف: | International audience ; 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. |
| نوع الوثيقة: | conference object |
| اللغة: | English |
| العلاقة: | hal-04447910; https://hal.science/hal-04447910Test; https://hal.science/hal-04447910/documentTest; https://hal.science/hal-04447910/file/article.pdfTest |
| DOI: | 10.4230/LIPIcs.CSL.2024.40 |
| الإتاحة: | https://doi.org/10.4230/LIPIcs.CSL.2024.40Test https://hal.science/hal-04447910Test https://hal.science/hal-04447910/documentTest https://hal.science/hal-04447910/file/article.pdfTest |
| حقوق: | http://creativecommons.org/licenses/byTest/ ; info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.791EEADA |
| قاعدة البيانات: | BASE |
| DOI: | 10.4230/LIPIcs.CSL.2024.40 |
|---|