Showing 1–13 of 13 results for author: Ghilezan, S

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

Authors: Ivan Prokić, Silvia Ghilezan, Simona Kašterović, Miroslav Popovic, Marko Popovic, Ivan Kaštelan

Abstract: 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 centralise… ▽ More 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. △ Less

Submitted 26 June, 2023; originally announced June 2023.

Comments: arXiv admin note: text overlap with arXiv:2305.20027

A Simple Python Testbed for Federated Learning Algorithms

Authors: Miroslav Popovic, Marko Popovic, Ivan Kastelan, Miodrag Djukic, Silvia Ghilezan

Abstract: Nowadays many researchers are develo** 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, a… ▽ More Nowadays many researchers are develo** 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. △ Less

Submitted 18 July, 2023; v1 submitted 31 May, 2023; originally announced May 2023.

Comments: 6 pages, 7 figures, 3 algorithms, as accepted at ZINC 2023, Published by IEEE Xplore

ACM Class: D.2.11

Logic of Combinatory Logic

Authors: Simona Kašterović, Silvia Ghilezan

Abstract: 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… ▽ More 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. △ Less

Submitted 13 December, 2022; originally announced December 2022.

MSC Class: 03B40; 03B05 ACM Class: F.4.1

L-types for resource awareness: an implicit name approach

Authors: Silvia Ghilezan, Jelena Ivetić, Simona Kašterović, Pierre Lescanne

Abstract: Since the early work of Church on $λ$I-calculus and Gentzen on structural rules, the control of variable use has gained an important role in computation and logic emerging different resource aware calculi and substructural logics with applications to programming language and compiler design. This paper presents the first formalization of variable control in calculi with implicit names based on de… ▽ More Since the early work of Church on $λ$I-calculus and Gentzen on structural rules, the control of variable use has gained an important role in computation and logic emerging different resource aware calculi and substructural logics with applications to programming language and compiler design. This paper presents the first formalization of variable control in calculi with implicit names based on de Bruijn indices. We design and implement three calculi: first, a restricted calculus with implicit names; then, a restricted calculus with implicit names and explicit substitution, and finally, an extended calculus with implicit names and resource control. We propose a novel concept of L-types, which are used (a) to define terms and (b) to characterize certain classes of terms in each of the presented calculi. We have adopted to work simultaneously on the design and implementation in Haskell and Agda. The benefit of this strategy is twofold: dependent types enable to express and check properties of programs in the type system and constructive proofs of preservation enable a constructive evaluator for terms (programs). △ Less

Submitted 21 December, 2021; originally announced December 2021.

Precise Subty** for Asynchronous Multiparty Sessions

Authors: Silvia Ghilezan, Jovanka Pantović, Ivan Prokić, Alceste Scalas, Nobuko Yoshida

Abstract: This paper presents the first formalisation of the precise subty** relation for asynchronous multiparty sessions. We show that our subty** 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 choic… ▽ More This paper presents the first formalisation of the precise subty** relation for asynchronous multiparty sessions. We show that our subty** 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 subty** 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 subty** is both operationally and denotationally precise. In the asynchronous multiparty setting, finding the precise subty** 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 subty** 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 subty** relation as a composition of refinement relations between single input/output trees, and providing a simple reasoning principle for asynchronous message optimisations. △ Less

Submitted 26 October, 2020; originally announced October 2020.

ACM Class: F.3.2; F.3.3

A Typed Model for Dynamic Authorizations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: 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 e… ▽ More 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 sco** 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 ty** discipline that ensures that processes never reduce to authorization errors, even when authorizations are dynamically delegated. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: In Proceedings PLACES 2015, arXiv:1602.03254

Journal ref: EPTCS 203, 2016, pp. 73-84

Precise subty** for synchronous multiparty sessions

Authors: Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Nobuko Yoshida

Abstract: The notion of subty** 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 subty**, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with r… ▽ More The notion of subty** 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 subty**, 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 subty** for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: In Proceedings PLACES 2015, arXiv:1602.03254

ACM Class: D.3.3; F.3.2

Journal ref: EPTCS 203, 2016, pp. 29-43

Combining behavioural types with security analysis

Authors: Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou, Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Jovanka Pantovic, Jorge A. Pérez, Peter Thiemann, Bernardo Toninho, Hugo Torres Vieira

Abstract: 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 enforc… ▽ More 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. △ Less

Submitted 8 October, 2015; originally announced October 2015.

Journal ref: Journal of Logical and Algebraic Methods in Programming, Elsevier, 2015, pp.18

Resource control and intersection types: an intrinsic connection

Authors: S. Ghilezan, J. Ivetic, P. Lescanne, S. Likavec

Abstract: In this paper we investigate the $λ$ -calculus, a $λ$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rules in the type assignment system. We introduce directly the class of $λ$ -terms and we provide a new treatment of substitution by its decompo-sition into atomic… ▽ More In this paper we investigate the $λ$ -calculus, a $λ$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rules in the type assignment system. We introduce directly the class of $λ$ -terms and we provide a new treatment of substitution by its decompo-sition into atomic steps. We propose an intersection type assignment system for $λ$ -calculus which makes a clear correspondence between three roles of variables and three kinds of intersection types. Finally, we provide the characterisation of strong normalisation in $λ$ -calculus by means of an in-tersection type assignment system. This process uses typeability of normal forms, redex subject expansion and reducibility method. △ Less

Submitted 6 December, 2014; originally announced December 2014.

Comments: arXiv admin note: substantial text overlap with arXiv:1306.2283

Dynamic Role Authorization in Multiparty Conversations

Authors: Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović, Jorge A. Pérez, Hugo Torres Vieira

Abstract: 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 ru… ▽ More 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. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

ACM Class: D.3.1; F.3.2

Journal ref: EPTCS 162, 2014, pp. 1-8

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

Authors: Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, Silvia Likavec

Abstract: 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 r… ▽ More 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. △ Less

Submitted 10 June, 2013; originally announced June 2013.

Comments: arXiv admin note: text overlap with arXiv:1112.3455

Computational interpretation of classical logic with explicit structural rules

Authors: Silvia Ghilezan, Pierre Lescanne, Dragisa Zunic

Abstract: 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 fe… ▽ More 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. △ Less

Submitted 21 March, 2012; originally announced March 2012.

Resource control and strong normalisation

Authors: Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne, Silvia Likavec

Abstract: 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 i… ▽ More 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. △ Less

Submitted 17 May, 2013; v1 submitted 15 December, 2011; originally announced December 2011.