26 citations · 61 across the 14 of their papers we have counts for
8 papers · 1 filter
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…
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…
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…
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…