BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Silvia Ghilezan

Silvia Ghilezan contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
Logic in Computer Sciencemath.LOProgramming LanguagesDistributed, Parallel, and Cluster ComputingCryptography and Security

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
7works
0followers
5topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

7 published item(s)

preprint2026arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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.

0 citations0 reviewsNo code linkedOpen access