top of page

Static and dynamic semantics of new and existing programming languages
 
My work is design and formalize programming languages, and study and conceive new programming features and expressive operational semantics and type-systems to make life simpler to the programmer daylife.
I used to mix the object-oriented paradigm with the functional paradigm and the rewriting-based paradigm one. Robin Milner slogan says that "well typed programs cannot go wrong".
Untyped languages are also useful to test new features that - after all - could be included in real typed languages. They are also good to rapid prototyping applications, especially internet-based applications.

Static and dynamic semantics of LF inspired proof-assistants
 
The Curry-Howard isomorphism says that logical propositions (theorems) are types, and logical terms (proofs) are typed-lambda terms à la Church (i.e. each bound-variable is decorated with a type). Curry-Howard is the basis of Constructive Logics and semi-automatic theorem provers, like the ones based with the dependent-type discipline (a.k.a. the Logical Framework, LF), further extended with polymophic-types, higher-order types, induction, co-induction, etc. One big branch of theorem provers are based on this principles. Different kind of logics could/should interact together, and "external oracles" can be called outside of the logical framework engine.

Screenshot 2023-10-30 at 13_edited.png

Lambda-calculus, Rewriting Calculus and Type systems
 
As Adam Chiplata wrote, with a lovely humor somewhere in his web page, "the weapons of a theoretical computer scientist are type-theory and lambda-calculus (untyped à la Curry or typed à la Church)".
I study various lambda-calculi and type-systems per se, hoping that some of those systems could produce some positive fall-back in real programming languages. As an example, enriching a simple abstraction lambda x.M with patterns, would lead to lambda P.Q. Applying lambda P.Q to R would reduce to sigma(Q), where sigma is the substitution of matching P with R.

Design of an open source platform to host Open Social Networks (myMed)
 
myMed is an experimental framework for implementing and deploying, on the top of a built-in cloud platform, many Open Social Networks (OSN) that could take advantage of sharing common software modules, hardware ressources, making inter-communication and inter-interaction simpler and improving rapid development.
The interactions between those OSN is very little, since the Application Program
ming Interfaces (API) - while existing - are very weak and limited to accessing the buddy lists, walls, or accessing OSN X with the password of OSN Y. Even worst, the possibility of programming or at least interconnecting common features (e.g. accessing on different data-bases, link user names and passwords, chats, etc.) between different OSN is quite limited.
My research try to take advantages in coordinating and in communicating different OSN built and hosted on the same framework and platform.

Screenshot 2021-10-21 at 13.13.37.png

Protocol for content-based routing (Arigatoni)

​

Arigatoni aims to give some foundations for the new paradigm of  programmable overlay networks and overlay computing systems as introduced by Luca Cardelli. Such overlays are built over a large number of distributed computational individuals, virtually organized in colonies, and ruled by a leader (broker) who is elected or imposed by system administrators. Every individual asks the broker to log in the colony by declaring the resources that can be offered (with variable guarantees). Once logged in, an individual can ask the broker for other resources. Colonies can recursively be considered as evolved individuals who can log in an outermost colony governed by another (super)-broker. Communications and routing intra-colonies goes through a broker-2-broker PKI-based negotiation. Theoretically, queries are formulæ in first-order logic equipped with a small program used to orchestrate and synchronize atomic formulæ. The proposed overlay promotes an intermittent participation in the colony, since peers can appear, disappear, and organize themselves dynamically. This implies that the routing process may lead to failures. Arigatoni is validated through simulation, and a proof-of-concept is implemented.

Screenshot 2021-10-21 at 13.13.13.png

Protocol for inter-connecting P2P networks and noSQL DB (Synapse)

​

Synapse is a scalable protocol for information retrieval over the inter-connection of heterogeneous overlay networks.

Applications on top of Synapse see those intra-overlay networks as a unique inter-overlay network. Scalability in Synapse is achieved via co-located nodes, i.e. nodes that are part of multiple overlay networks at the same time. Co-located nodes, playing the role of neural synapses and connected to several overlay networks, allow a larger search area and provide alternative routing.

Synapse can either work with “open” overlays adapting their protocol to synapse interconnection requirements, or with “closed” overlays that will not accept any change to their protocol. Thanks to alternate routing paths, Synapse also gives a practical solution to network partitions.

Screenshot 2021-10-21 at 13.26.38.png
Screenshot 2021-10-21 at 13.25.37.png

Advanced Semantic Discovery and Query (ASDQ) an ETSI SmartM2M/oneM2M IoT standard

 

ASDQ is an extension of the present oneM2M semantic discovery across a network of Common Services Entities (CSEs) statically connected among them in a tree-like topology inside a single or multiple Service Provider (SP), including non oneM2M ones and in a mesh-like topology between the root of the different SPs. The Advanced Semantic Discovery aims to discover AEs (also called Resources) that are registered/announced to some CSEs. As the Figure on top shows, the Advanced Semantic Discovery could start from any Application Entities (AE), even these ones not belonging to the same
Trusted Domain. The Advanced Resource Discovery differs from the usual one present in oneM2M in the sense that one (or many) AE could be searched for even without knowing its identifier but just knowing its TYPE or ONTOLOGY membership.

Intuitively a CSE receiving a complex query: 1) reduce a complex query into a number of unary queries; 2) route the unary queries one-by-one; and 3) aggregate and return the results (see Figure on bottom). ASDQ is an evolution of the Arigatoni protocol that, 10 year later his introduction, is now an ETSI SmartM2M/oneM2M standard.

Screenshot 2021-10-21 at 14.31.36.png

Asynchronous Contact Tracing an ETSI SmartM2M/oneM2M standard

 

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

​

 

 

 

 

 

 

​

​

The SARS-CoV-2 virus has severely impacted the life of many people. Social distancing and vaccines are currently the main countermeasure in the attempt to limit the spread of the disease but lockdown clusters are creating severe damage to the economy and to the personal life of its citizens. The role of testing is crucial. However, testing must be associated with the identification of the candidates to be tested, considering also that global testing on this scale is impracticable, with present time constraints and the need for haste.

The role of telecommunications in this area has been exploited by various contact tracing

applications that are attempting to advise people about a potential risk of infection and signal the need for a test. It is essential to respect the personal privacy and respect enshrined EU regulations in order to increase acceptance by the public at large.
Standards for these personal applications for tracing people and their contacts are crucial in order to ensure future interop- erability among the different solutions developed during this initial period of crisis.

One response to the difficulties of establishing a method for Synchronous Contact Tracing (SCT), like e.g. Inria-Fraunhofer’s Robert, or the Apple-Google’s Privacy-Preserving Contact Tracing, is to remove the time and space limitations and to trace surfaces that have been contaminated by the virus, rather than just recording the anonymous cryptokeys of persons involved in a contact. The underlying concept of SCT is based on the generic behaviour of getting a notification of a potential virus exposure in case of i) being close to an infected person at the same time and in the same space and ii) on the individual’s willingness and ability to declare his or her status as infected.

My objective is be able to monitor, detect, alert, forecast, in a nearly autonomic way, the presence of any natural and artificial pathogens, viruses and pollutants dangerous for living beings, present in things, air, and water and can thus overcome the risk of indecisions, delays or personal biased opinions which have been so disastrous in dealing with pandemics and environmentally hazardous major accidents using Internet of Things.

In solo, singular technologies have been studied for years. However, none were implemented in a coherent and coordinated and responsive way using the same format and protocols; the analogy with the pre-Internet era is apparent. One of the reasons is the lack of common standards for IoT globally adopted such as could derive as a by-product of an IoT communication standard.

My aim is to develop a breakthrough, by designing an IoT eHealth standard, and materialise it into an infrastructure and a uniform middleware based on the ETSI oneM2M standard, which can enable all detection and surveillance platforms to communicate and cooperate together. These challenges require the multidisciplinary and integrated intervention of public agencies and biotech companies specialised in all the scientific areas necessary to develop a radically new Pan-European surveillance system.

The ETSI standard Asynchronous Contact Tracing (ACT) that i recently introduced, traces an IoT connected object that may have been contaminated e.g. by the SARS-CoV-2 virus (or by any other future pandemic viruses or pollutions). The proposed standard platform clearly addresses generic needs and, on a long-term basis, may drastically and economically contribute to the development and the connection of a new real-time pathogen and pollution overlay alertness network. This shifts the paradigm, from searching for a person in the process of synchronously infecting another, to the tracing of objects which asynchronously can be a vehicle for potential contamination to humans.

ACT enables the people who have come into contact with a particular surface to be alerted to a potential contagion or pollution, and at the same time it can signal that at least one of the many persons who have been in contact with such solid or liquid objects is infected, applying de facto the well-known statistical studies of Group Testing and enabling a form of anonymous statistical screening of the population and applying to all the environments where people share the same physical space, such as a supermarket, schools, restaurants, hotels, gyms, offices, working plants, hospitals, hospices, etc. or applying to an object that is encountering people while it is in movement, such as a bus or a train, or potentially to any moving object. With ACT, the time and space synchronicity of two persons equipped with the same mobile application is not needed anymore, and, as such, more matches can be discovered between one person and its closeness to a precise location, where the presence of environmental anomalies or pathogens has been formally established by an IoT Detection Platform.

My aims are to develop a breakthrough global detection and inter-communication network focused on rapid response to bio-emergencies. This will radically change the current services already deployed by the National Public Health Institutes to monitor, alert, and advise political decision makers, public organizations, environmental Institutes and citizens by implementing new adaptable and modular automated diagnostic solutions for future pandemics and pollutions, combined with innovative technological solutions based on the concepts of inter-connected IoT. My tasks in this endeavour are to

  • improve and generalise my already published overlay protocols, such as Arigatoni, or Avanced Semantic Discovery, or ACT to the IoT case, and apply it to an extended contact and forecast tracing case.

  • software conceive, network interconnect, and envisage case studies, inside the oneM2M ETSI standard, of the ad hoc programmable real-time sensors monitoring of the spread of the infecting agent, as envisaged by research institutions and companies that have participated to the specification of the TS 103757.

  • promote an ETSI Pan-European standard capable to a real-time forecasting of any kind of pathogens and pollutions to people in the EU space, in a anonymous, resilient, and secure way ; the standard should be sufficiently flexible and customisable nation-by-nation, according to their peculiar laws.

  • I hope, with the already established ETSI partners and my Academic partners to safely and formally design and inter- connect the mentioned entities using a unique and standardised infrastructure. More precisely, we aims to design, improve, and develop an innovative and standardised oneM2M architecture able to:

  • collect the information produced by the PCD and IVD based Detection Platform.

  • correlate it to specific location and areas on the territory.

  • elaborate and augment such information, including territory diffusion forecasts, by means of data fusion.

  • share the elaborate information with the National Health System Services.

  • empower on a more solid scientific understanding the political decision makers.

  • share the elaborate information with the citizen via Web services.

  • enable the citizen to discover their individual exposition to the pathogen in areas visited in the recent past, with a full respect of privacy (all the information remains on the user smartphone without any sharing with the rest of the system). PCD and IVD convey the information into common oneM2M actuators, that elaborate and push it in a IoT overlay network using heterogeneous underlay network technologies that usually walk on specific pathways with poor or no integration at all.

Screenshot 2023-10-30 at 13.47.09.png
Screenshot 2023-10-30 at 13.49.50.png
bottom of page