Search

Your search keyword '"LIQUORI, LUIGI"' showing total 241 results
Start Over Author "LIQUORI, LUIGI"

Refine your results

241 results on '"LIQUORI, LUIGI"'

1. Strong Priority and Determinacy in Timed CCS

Author

Liquori, Luigi and Mendler, Michael

Subjects
Computer Science - Programming Languages, Computer Science - Computation and Language
Abstract

Building on the standard theory of process algebra with priorities, we identify a new scheduling mechanism, called "constructive reduction" which is designed to capture the essence of synchronous programming. The distinctive property of this evaluation strategy is to achieve determinacy-by-construction for multi-cast concurrent communication with shared memory. In the technical setting of CCS extended by clocks and priorities, we prove for a large class of "coherent" processes a confluence property for constructive reductions. We show that under some restrictions, called "pivotability", coherence is preserved by the operators of prefix, summation, parallel composition, restriction and hiding. Since this permits memory and sharing, we are able to cover a strictly larger class of processes compared to those in Milner's classical confluence theory for CCS without priorities.

Published
2024

2. A Type Checker for a Logical Framework with Union and Intersection Types

Author

Liquori, Luigi and Stolze, Claude

Subjects
Computer Science - Logic in Computer Science, Computer Science - Programming Languages, F.3.1, F.4.1
Abstract

We present the syntax, semantics, and typing rules of Bull, a prototype theorem prover based on the Delta-Framework, i.e. a fully-typed lambda-calculus decorated with union and intersection types, as described in previous papers by the authors. Bull also implements a subtyping algorithm for the Type Theory Xi of Barbanera-Dezani-de'Liguoro. Bull has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi's Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow the user to write Delta-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard's parametric one.

Published
2020

3. The Delta-framework

Author

Honsell, Furio, Liquori, Luigi, Stolze, Claude, and Scagnetto, Ivan

Subjects
Computer Science - Logic in Computer Science
Abstract

We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF-Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF-Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.

Published
2018

4. The Delta-calculus: syntax and types

Author

Liquori, Luigi and Stolze, Claude

Subjects
Computer Science - Logic in Computer Science
Abstract

We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Salle', the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection type systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems a` la Curry and the corresponding intersection type systems a` la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.

Published
2018

5. $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Author

Honsell, Furio, Liquori, Luigi, Maksimovic, Petar, and Scagnetto, Ivan

Subjects
Computer Science - Logic in Computer Science, F.4.1
Abstract

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,\sigma}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory., Comment: Accepted for publication in LMCS

Published
2017
Full Text
View/download PDF

6. A Network Aware Resource Discovery Service

Author

Liquori, Luigi, Gaeta, Rossano, Sereno, Matteo, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Gribaudo, Marco, editor, Iacono, Mauro, editor, Phung-Duc, Tuan, editor, and Razumchik, Rostislav, editor

Published
2020
Full Text
View/download PDF

7. Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks

Author

Honsell, Furio, Liquori, Luigi, Maksimović, Petar, and Scagnetto, Ivan

Subjects
Computer Science - Logic in Computer Science, D.2.4, F.3.1, F.4.1
Abstract

We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for gluing together diverse Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms., Comment: In Proceedings LFMTP 2015, arXiv:1507.07597

Published
2015
Full Text
View/download PDF

9. A Decidable Subtyping Logic for Intersection and Union Types

Author

Liquori, Luigi, Stolze, Claude, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Mousavi, Mohammad Reza, editor, and Sgall, Jiří, editor

Published
2017
Full Text
View/download PDF

10. Implementing Cantor’s Paradise

Author

Honsell, Furio, Lenisa, Marina, Liquori, Luigi, Scagnetto, Ivan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Igarashi, Atsushi, editor

Published
2016
Full Text
View/download PDF

11. A Realizability Interpretation for Intersection and Union Types

Author

Dougherty, Daniel J., de’Liguoro, Ugo, Liquori, Luigi, Stolze, Claude, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Igarashi, Atsushi, editor

Published
2016
Full Text
View/download PDF

12. LaxF: Side Conditions and External Evidence as Monads

Author

Honsell, Furio, Liquori, Luigi, Scagnetto, Ivan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Csuhaj-Varjú, Erzsébet, editor, Dietzfelbinger, Martin, editor, and Ésik, Zoltán, editor

Published
2014
Full Text
View/download PDF

13. Backward-Compatible Cooperation of Heterogeneous P2P Systems

Author

Ngo, Hoang Giang, Liquori, Luigi, Nguyen, Chan Hung, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Chatterjee, Mainak, editor, Cao, Jian-nong, editor, Kothapalli, Kishore, editor, and Rajsbaum, Sergio, editor

Published
2014
Full Text
View/download PDF

14. How Research meets Standardization: the Asynchronous Contact Tracing ETSI Standard and the PANDESYS Research Activity

Author

Liquori, Luigi, Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), and COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)

Subjects
IoT, [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [SDV.MHEP.MI]Life Sciences [q-bio]/Human health and pathology/Infectious diseases, oneM2M, Digital Contact Tracing, Covid-19
Abstract

International audience; The Covid-19 pandemic has shown how the mutation of a common virus can topple theworld economy in a few weeks and how public policies must react quickly to limit andeven avoid such a collapse. The existing ‘In Vitro Diagnostic’ (IVD) ICT technology hasnot always been reliable. Asynchronous Contact Tracing (ACT), standardized in ETSISmartM2M Technical Committee, offers a reliable solution to detect pathogens.

Published
2023

15. Interconnection of Large Scale Unstructured P2P Networks: Modeling and Analysis

Author

Ciancaglini, Vincenzo, Gaeta, Rossano, Loti, Riccardo, Liquori, Luigi, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Dudin, Alexander, editor, and De Turck, Koen, editor

Published
2013
Full Text
View/download PDF

16. Towards a Trust and Reputation Framework for Social Web Platforms

Author

Nguyen, Thao, Liquori, Luigi, Martin, Bruno, Hanks, Karl, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Herrero, Pilar, editor, Panetto, Hervé, editor, Meersman, Robert, editor, and Dillon, Tharam, editor

Published
2012
Full Text
View/download PDF

17. An Extension and Cooperation Mechanism for Heterogeneous Overlay Networks

Author

Ciancaglini, Vincenzo, Liquori, Luigi, Hoang, Giang Ngo, Maksimović, Petar, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Becvar, Zdenek, editor, Bestak, Robert, editor, and Kencl, Lukas, editor

Published
2012
Full Text
View/download PDF

19. Logic and Computation in a Lambda Calculus with Intersection and Union Types

Author

Dougherty, Daniel J., Liquori, Luigi, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Clarke, Edmund M., editor, and Voronkov, Andrei, editor

Published
2010
Full Text
View/download PDF

20. CarPal: Interconnecting Overlay Networks for a Community-Driven Shared Mobility

Author

Ciancaglini, Vincenzo, Liquori, Luigi, Vanni, Laurent, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Wirsing, Martin, editor, Hofmann, Martin, editor, and Rauschmayer, Axel, editor

Published
2010
Full Text
View/download PDF

21. Synapse: A Scalable Protocol for Interconnecting Heterogeneous Overlay Networks

Author

Liquori, Luigi, Tedeschi, Cédric, Vanni, Laurent, Bongiovanni, Francesco, Ciancaglini, Vincenzo, Marinković, Bojan, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Crovella, Mark, editor, Feeney, Laura Marie, editor, Rubenstein, Dan, editor, and Raghavan, S. V., editor

Published
2010
Full Text
View/download PDF

23. Asynchronous Contact Tracing, Fighting Pandemics with Internet of Things. Set up of the of oneM2M infrastructure, mobile and web applications

Author

Di Dio, Alessio, Liquori, Luigi, Liquori, Luigi, Université Côte d'Azur (UCA), Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), and Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], [SDV.MHEP] Life Sciences [q-bio]/Human health and pathology, [INFO.INFO-NI] Computer Science [cs]/Networking and Internet Architecture [cs.NI], [SDV.MHEP.MI]Life Sciences [q-bio]/Human health and pathology/Infectious diseases, [SDV.MHEP.MI] Life Sciences [q-bio]/Human health and pathology/Infectious diseases, [SDV.MHEP]Life Sciences [q-bio]/Human health and pathology
Published
2022

24. A Conditional Logical Framework

Author

Honsell, Furio, Lenisa, Marina, Liquori, Luigi, Scagnetto, Ivan, Carbonell, Jaime G., editor, Siekmann, Jörg, editor, Cervesato, Iliano, editor, Veith, Helmut, editor, and Voronkov, Andrei, editor

Published
2008
Full Text
View/download PDF

25. An Overlay Architecture for Vehicular Networks

Author

Liquori, Luigi, Borsetti, Diego, Casetti, Claudio, Chiasserini, Carla-Fabiana, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Das, Amitabha, editor, Pung, Hung Keng, editor, Lee, Francis Bu Sung, editor, and Wong, Lawrence Wai Choong, editor

Published
2008
Full Text
View/download PDF

26. Logical Networks: Towards Foundations for Programmable Overlay Networks and Overlay Computing Systems

Author

Liquori, Luigi, Cosnard, Michel, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Barthe, Gilles, editor, and Fournet, Cédric, editor

Published
2008
Full Text
View/download PDF

28. Improving Resource Discovery in the Arigatoni Overlay Network

Author

Chand, Raphaël, Liquori, Luigi, Cosnard, Michel, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Rangan, C. Pandu, editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Lukowicz, Paul, editor, Thiele, Lothar, editor, and Tröster, Gerhard, editor

Published
2007
Full Text
View/download PDF

29. Rewriting Calculus with Fixpoints: Untyped and First-Order Systems

Author

Cirstea, Horatiu, Liquori, Luigi, Wack, Benjamin, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Berardi, Stefano, editor, Coppo, Mario, editor, and Damiani, Ferruccio, editor

Published
2004
Full Text
View/download PDF

31. The Rho Cube

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Honsell, Furio, editor, and Miculan, Marino, editor

Published
2001
Full Text
View/download PDF

32. Matching Power

Author

Cirstea, Horatiu, Kirchner, Claude, Liquori, Luigi, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, and Middeldorp, Aart, editor

Published
2001
Full Text
View/download PDF

38. On object extension

Author

Liquori, Luigi, Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, and Jul, Eric, editor

Published
1998
Full Text
View/download PDF

45. Comparing cubes

Author

van Bakel, Steffen, Liquori, Luigi, della Rocca, Simona Ronchi, Urzyczyn, Paweł, Goos, Gerhard, editor, Hartmanis, Juris, editor, Nerode, Anil, editor, and Matiyasevich, Yu. V., editor

Published
1994
Full Text
View/download PDF

48. SmartM2M; Asynchronous Contact Tracing System: Fighting pandemic disease with Internet of Things

Author

Liquori, Luigi, COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA), Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), and COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)

Subjects
[SDV.MHEP.MI]Life Sciences [q-bio]/Human health and pathology/Infectious diseases, [SDV]Life Sciences [q-bio], [INFO]Computer Science [cs], [SDV.SPEE]Life Sciences [q-bio]/Santé publique et épidémiologie
Published
2020

49. A prototype-based approach to object reclassification

Author

Ciaffaglione, Alberto, Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015 - 2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), and Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2020

50. A prototype-based approach to object evolution

Author

Ciaffaglione, Alberto, Di Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France, Université Nice Sophia Antipolis (... - 2019) (UNS), and COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS)

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience; We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2020

Catalog

Books, media, physical & digital resources
See catalog results