26 citations · 61 across the 14 of their papers we have counts for
14 papers
Justification Logic of the Lambda Calculus
Silvia Ghilezan, Paaras Padhiar
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. Justif…
Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP
Ivan Prokić, Silvia Ghilezan, Simona Kašterović +3
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 centra…
A Simple Python Testbed for Federated Learning Algorithms
Miroslav Popovic, Marko Popovic, Ivan Kastelan +2
Nowadays many researchers are developing various distributed and decentralized frameworks for federated learning algorithms. However, development of such a framework targeting smar…
Logic of Combinatory Logic
Simona Kašterović, Silvia Ghilezan
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 presente…
List types for resource aware languages: an implicit name approach
Silvia Ghilezan, Jelena Ivetić, Pierre Lescanne +1
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 lan…
Precise Subtyping for Asynchronous Multiparty Sessions
Silvia Ghilezan, Jovanka Pantović, Ivan Prokić +2
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 s…
A Typed Model for Dynamic Authorizations
Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović +2
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,…
Precise subtyping for synchronous multiparty sessions
Mariangiola Dezani-Ciancaglini, Silvia Ghilezan, Svetlana Jakšić +2
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 soundnes…
Combining behavioural types with security analysis
Massimo Bartoletti, Ilaria Castellani, Pierre-Malo Deniélou +7
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 a…
Resource control and intersection types: an intrinsic connection
S. Ghilezan, J. Ivetic, P. Lescanne +1
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 o…
Dynamic Role Authorization in Multiparty Conversations
Silvia Ghilezan, Svetlana Jakšić, Jovanka Pantović +2
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 d…
A journey through resource control lambda calculi and explicit substitution using intersection types (an account)
Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne +1
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 e…
Computational interpretation of classical logic with explicit structural rules
Silvia Ghilezan, Pierre Lescanne, Dragisa Zunic
We present a calculus providing a Curry-Howard correspondence to classical logic represented in the sequent calculus with explicit structural rules, namely weakening and contractio…
Resource control and strong normalisation
Silvia Ghilezan, Jelena Ivetic, Pierre Lescanne +1
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 natu…