arXiv subjects

Silvia Ghilezan

Publications and source records attributed to Silvia Ghilezan.

15 recordsLinked to original sources

arXiv2026

Justification Logic of the Lambda Calculus

The simply typed λ-calculus is a model of computation where typed terms correspond to proofs of intuitionistic propositional logic (IPL) via the Curry-Howard correspondence. Justification logic is an operational modal logic in which the standard box modality is replaced by an explicit proof term, allowing the logic itself to reason directly about proofs of its formulas. Standard justification logics reason about proofs of IPL by embedding Hilbert-style axiomatic proofs of IPL as proof terms of the logic. We instead introduce a justification logic of the λ-calculus, in which the proof terms of the modality are exactly the typed λ-terms themselves: a modal logic that reasons about computation and proof simultaneously, as both notions coincide under the Curry-Howard interpretation. First, we provide an axiomatisation of this logic. We then propose a natural deduction system and a Curry-Howard interpretation, where a formal connection between the term calculus and the proof terms of the logic is provided. To complete the picture, we give a Gentzen-style sequent calculus for which we prove cut-elimination, and consequently obtain a normalisation result by working in the negative fragment.

cs.LO↗

arXiv2026

A-COMPASS: Formal Foundations for Anonymity Analysis in Microdata

In the information age, one of the leading problems is how to ensure individual's privacy. Depending on the context in which privacy is considered, various data privacy models have emerged. However, the domain of formal verification of these models is still not sufficiently explored even when it comes to the most basic models. An attempt to verify privacy requirements is the Compliance Assertion Language (COMPASS). In COMPASS, one can specify an anonymity condition that a table needs to satisfy, and an action that will modify the table if the condition is not satisfied. It is designed to operate on preprocessed tables in a form one record - one group of people. In this paper, we modify the COMPASS language in order to operate on microdata tables in their usual form of one record - one person. The modified language is called A-COMPASS. Along with checking of previously applied anonymity conditions, A-COMPASS enables the execution of anonymization actions as a new feature. We further provide the syntax and the semantics for the A-COMPASS language. We also prove the most important properties of the introduced semantics like determinism and compositionality. Finally, we provide a mechanism to verify anonymity properties, such as k-anonymity and l-diversity.

cs.CR↗

arXiv2026

On Asynchronous Multiparty Session Types for Federated Learning

This paper improves the session typing theory to support the modelling and verification of processes that implement federated learning protocols. To this end, we build upon the asynchronous ``bottom-up'' session typing approach by adding support for input/output operations directed towards multiple participants at the same time. We further enhance the flexibility of our typing discipline and allow for safe process replacements by introducing a session subtyping relation tailored for this setting. We formally prove safety, deadlock-freedom, liveness, and session fidelity properties for our session typing system. Moreover, we highlight the nuances of our session typing system, which (compared to previous work) reveals interesting interplays and trade-offs between safety, liveness, and the flexibility of the subtyping relation.

cs.LO↗

arXiv2026

List types for resource aware languages: an implicit name approach

A novel formalisation of variable control in languages with implicit names based on de Bruijn indices is presented. We design and implement three languages: first, a restricted language with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names, implicit substitution and resource control. We propose a novel concept of list types, which are used to give a simple and manageable definition of linearity. We develop an implementation in Haskell.

cs.LO↗

arXiv2023

A Simple Python Testbed for Federated Learning Algorithms

Nowadays many researchers are developing various distributed and decentralized frameworks for federated learning algorithms. However, development of such a framework targeting smart Internet of Things in edge systems is still an open challenge. In this paper, we present our solution to that challenge called Python Testbed for Federated Learning Algorithms. The solution is written in pure Python, and it supports both centralized and decentralized algorithms. The usage of the presented solution is both validated and illustrated by three simple algorithm examples.

cs.DC↗

arXiv2023

Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP

Federated learning (FL) is a machine learning setting where clients keep the training data decentralised and collaboratively train a model either under the coordination of a central server (centralised FL) or in a peer-to-peer network (decentralised FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralised and a decentralised one, using the CSP process calculus and the PAT model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freeness (safety property) and successful termination (liveness property). The CSP models are constructed bottom-up by hand as a faithful representation of the real Python code and is automatically checked top-down by PAT.

cs.DC↗

arXiv2022

Logic of Combinatory Logic

We develop a classical propositional logic for reasoning about combinatory logic. We define its syntax, axiomatic system and semantics. The syntax and axiomatic system are presented based on classical propositional logic, with typed combinatory terms as basic propositions, along with the semantics based on applicative structures extended with special elements corresponding to primitive combinators. Both the equational theory of untyped combinatory logic and the proposed axiomatic system are proved to be sound and complete w.r.t. the given semantics. In addition, we prove that combinatory logic is sound and complete w.r.t. the given semantics.

math.LO↗

arXiv2020

Precise Subtyping for Asynchronous Multiparty Sessions

This paper presents the first formalisation of the precise subtyping relation for asynchronous multiparty sessions. We show that our subtyping relation is sound (i.e., guarantees safe process replacement) and also complete: any extension of the relation is unsound. To achieve our results, we develop a novel session decomposition technique, from full session types (including internal/external choices) into single input/output session trees (without choices). Previous work studies precise subtyping for binary sessions (with just two participants), or multiparty sessions (with any number of participants) and synchronous interaction. Here, we cover multiparty sessions with asynchronous interaction, where messages are transmitted via FIFO queues (as in the TCP/IP protocol), and prove that our subtyping is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subtyping relation is a highly complex task: this is because, under some conditions, participants can permute the order of their inputs and outputs, by sending some messages earlier or receiving some later, without causing errors; the precise subtyping relation must capture all such valid permutations -- and consequently, its formalisation, reasoning and proofs become challenging. Our session decomposition technique overcomes this complexity, expressing the subtyping relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations.

cs.LO↗

arXiv2016

Precise subtyping for synchronous multiparty sessions

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness.

cs.LO↗

arXiv2016

A Typed Model for Dynamic Authorizations

Security requirements in distributed software systems are inherently dynamic. In the case of authorization policies, resources are meant to be accessed only by authorized parties, but the authorization to access a resource may be dynamically granted/yielded. We describe ongoing work on a model for specifying communication and dynamic authorization handling. We build upon the pi-calculus so as to enrich communication-based systems with authorization specification and delegation; here authorizations regard channel usage and delegation refers to the act of yielding an authorization to another party. Our model includes: (i) a novel scoping construct for authorization, which allows to specify authorization boundaries, and (ii) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error may consist in, e.g., performing an action along a name which is not under an appropriate authorization scope. We introduce a typing discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated.

cs.LO↗

arXiv2015

Combining behavioural types with security analysis

Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.

cs.PL↗

arXiv2014

Dynamic Role Authorization in Multiparty Conversations

Protocol specifications often identify the roles involved in communications. In multiparty protocols that involve task delegation it is often useful to consider settings in which different sites may act on behalf of a single role. It is then crucial to control the roles that the different parties are authorized to represent, including the case in which role authorizations are determined only at runtime. Building on previous work on conversation types with flexible role assignment, here we report initial results on a typed framework for the analysis of multiparty communications with dynamic role authorization and delegation. In the underlying process model, communication prefixes are annotated with role authorizations and authorizations can be passed around. We extend the conversation type system so as to statically distinguish processes that never incur in authorization errors. The proposed static discipline guarantees that processes are always authorized to communicate on behalf of an intended role, also covering the case in which authorizations are dynamically passed around in messages.

cs.LO↗

arXiv2013

A journey through resource control lambda calculi and explicit substitution using intersection types (an account)

In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda calculus with explicit substitution. All three calculi enable explicit control of resources due to the presence of weakening and contraction operators. Along this journey, we propose intersection type assignment systems for all three resource control calculi. We recognise the need for three kinds of variables all requiring different kinds of intersection types. Our main contribution is the characterisation of strong normalisation of reductions in all three calculi, using the techniques of reducibility, head subject expansion, a combination of well-orders and suitable embeddings of terms.

math.LO↗

arXiv2013

Resource control and strong normalisation

We introduce the \emph{resource control cube}, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and with either natural deduction or sequent calculus. The four calculi of the cube that correspond to natural deduction have been proposed by Kesner and Renaud and the four calculi that correspond to sequent lambda calculi are introduced in this paper. The presentation is parameterized with the set of resources (weakening or contraction), which enables a uniform treatment of the eight calculi of the cube. The simply typed resource control cube, on the one hand, expands the Curry-Howard correspondence to intuitionistic natural deduction and intuitionistic sequent logic with implicit or explicit structural rules and, on the other hand, is related to substructural logics. We propose a general intersection type system for the resource control cube calculi. Our main contribution is a characterisation of strong normalisation of reductions in this cube. First, we prove that typeability implies strong normalisation in the ''natural deduction base" of the cube by adapting the reducibility method. We then prove that typeability implies strong normalisation in the ''sequent base" of the cube by using a combination of well-orders and a suitable embedding in the ''natural deduction base". Finally, we prove that strong normalisation implies typeability in the cube using head subject expansion. All proofs are general and can be made specific to each calculus of the cube by instantiating the set of resources.

math.LO↗

arXiv2012

Computational interpretation of classical logic with explicit structural rules

We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contraction. These structural rules introduce explicit erasure and duplication of terms, respectively. We present a type system for which we prove the type-preservation under reduction. A mutual relation with classical calculus featuring implicit structural rules has been studied in detail. From this analysis we derive strong normalisation property.

cs.LO↗