DSpace-CRIS - Univerzitet u Novom Saduhttps://open.uns.ac.rsThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Fri, 02 Dec 2022 19:12:37 GMT2022-12-02T19:12:37Z50411- Lambda calculus with typeshttps://open.uns.ac.rs/handle/123456789/7058Title: Lambda calculus with types
Authors: Barendregt H.; Dekkers W.; Statman R.; Alessi F.; Bezem M.; Cardone F.; Coppo M.; Dezani-Ciancaglini M.; Dowek G.; Gilezan, Silvia; Honsell F.; Moortgat M.; Severi P.; Urzyczyn P.
Abstract: © Association for Symbolic Logic 2013. This handbook with exercises reveals in formalisms, hitherto mainly used for hardware and software design and verification, unexpected mathematical beauty. The lambda calculus forms a prototype universal programming language, which in its untyped version is related to Lisp, and was treated in the first author's classic The Lambda Calculus (1984). The formalism has since been extended with types and used in functional programming (Haskell, Clean) and proof assistants (Coq, Isabelle, HOL), used in designing and verifying IT products and mathematical proofs. in this book, the authors focus on three classes of typing for lambda terms: Simple types, recursive types and intersection types. it is in these three formalisms of terms and types that the unexpected mathematical beauty is revealed. The treatment is authoritative and comprehensive, complemented by an exhaustive bibliography, and numerous exercises are provided to deepen the readers' understanding and increase their confidence using types.
Sat, 01 Jan 2011 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/70582011-01-01T00:00:00Z
- The Duality of Classical Intersection and Union Typeshttps://open.uns.ac.rs/handle/123456789/11319Title: The Duality of Classical Intersection and Union Types
Authors: Downen P.; Ariola Z.; Gilezan, Silvia
Abstract: © 2019 - IOS Press and the authors. All rights reserved. For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest - soundness, completeness, and type safety - we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems - one for call-by-value and one for call-by-name evaluation - which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.
Tue, 01 Jan 2019 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/113192019-01-01T00:00:00Z
- Linked data privacyhttps://open.uns.ac.rs/handle/123456789/5816Title: Linked data privacy
Authors: Jakšić, Svetlana; Pantović, Jovanka; Gilezan, Silvia
Abstract: Copyright © Cambridge University Press 2015. Web of Linked Data introduces common format and principles for publishing and linking data on the Web. Such a network of linked data is publicly available and easily consumable. This paper introduces a calculus for modelling networks of linked data with encoded privacy preferences. In that calculus, a network is a parallel composition of users, where each user is named and consists of data, representing the user's profile, and a process. Data is a parallel composition of triples with names (resources) as components. Associated with each name and each triple of names are their privacy protection policies, that are represented by queries. A data triple is accessible to a user if the user's data satisfies the query assigned to that triple. The main contribution of this model lies in the type system which together with the introduced query order ensures that static type-checking prevents privacy violations. We say that a network is well behaved if-access to a triple is more restrictive than access to its components and less restrictive than access to the user name it is enclosed with,-each user can completely access their own profile,-each user can update or partly delete profiles that they own (can access the whole profiles), and-each user can update the privacy preference policy of data of another profile that they own or write data to another profile only if the newly obtained profile stays fully accessible to their owner. We prove that any well-Typed network is well behaved.
Sun, 01 Jan 2017 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/58162017-01-01T00:00:00Z
- Security types for dynamic web datahttps://open.uns.ac.rs/handle/123456789/10507Title: Security types for dynamic web data
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia; Pantović, Jovanka; Varacca D.
Abstract: We describe a type system for the X d π calculus of Gardner and Maffeis. An X d π-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at different locations) and a process, for modeling process interaction, process migration and interaction between processes and data. Our type system is based on types for locations, data and processes, expressing security levels. A tree can store data of different security level, independently from the security level of the enclosing location. The access and mobility rights of a process depend on the security level of the "source" location of the process itself, i.e. of the location where the process was in the initial network or where the process was created by the activation of a script. The type system enjoys type preservation under reduction (subject reduction). In consequence of subject reduction we prove the following security properties. In a well-typed X d π-network, a process P whose source location is of level h can copy data of security level at most h and update data of security level less than h. Moreover, the process P can only communicate data and go to locations of security level equal or less than h. © 2008 Elsevier B.V. All rights reserved.
Fri, 08 Aug 2008 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/105072008-08-08T00:00:00Z
- Dynamic role authorization in multiparty conversationshttps://open.uns.ac.rs/handle/123456789/5191Title: Dynamic role authorization in multiparty conversations
Authors: Gilezan, Silvia; Jakšić, Svetlana; Pantović, Jovanka; Pérez J.; Vieira H.
Abstract: © 2016. Protocols in distributed settings usually rely on the interaction of several parties and often identify the roles involved in communications. Roles may have a behavioral interpretation, as they do not necessarily correspond to sites or physical devices. Notions of role authorization thus become necessary to consider settings in which, e.g., different sites may be authorized to act on behalf of a single role, or in which one site may be authorized to act on behalf of different roles. This flexibility must be equipped with ways of controlling the roles that the different parties are authorized to represent, including the challenging case in which role authorizations are determined only at runtime. We present a typed framework for the analysis of multiparty interaction with dynamic role authorization and delegation. Building on previous work on conversation types with role assignment, our formal model is based on an extension of the π-calculus in which the basic resources are pairs channel-role, which denote the access right of interacting along a given channel representing the given role. To specify dynamic authorization control, our process model includes (1) a novel scoping construct for authorization domains, and (2) communication primitives for authorizations, which allow to pass around authorizations to act on a given channel. An authorization error then corresponds to an action involving a channel and a role not enclosed by an appropriate authorization scope. We introduce a typing discipline that ensures that processes never reduce to authorization errors, including when parties dynamically acquire authorizations.
Fri, 01 Jan 2016 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/51912016-01-01T00:00:00Z
- Formal verification of python software transactional memory based on timed automatahttps://open.uns.ac.rs/handle/123456789/12783Title: Formal verification of python software transactional memory based on timed automata
Authors: Kordić, Branislav; Popović, Miroslav; Gilezan, Silvia
Abstract: © 2019, Budapest Tech Polytechnical Institution. All rights reserved. Nowadays Software Transactional Memories (STMs) are used in safety-critical software, such as computational-chemistry simulation programs. To the best of our knowledge, the existing STMs were not developed using rigorous model-driven development process, on the contrary, the majority of proposed STMs are directly implemented in a target programming language and formally verified STMs are proven against more general models. This may result in some key aspects of implementation being omitted or interpreted incorrectly. In this paper, we demonstrate an approach to the formal verification of one particular STM, for the Python language, named Python Software Transactional Memory (PSTM), which is based on a STM design and implementation details. Based on these details, faithful models of a PSTM based system, are developed and verified. The PSTM system components are modeled as timed automata utilizing UPPAAL tool. Finally, it is verified that PSTM satisfies deadlock-freeness, safety, liveness, and reachability properties.
Tue, 01 Jan 2019 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/127832019-01-01T00:00:00Z
- Combining behavioural types with security analysishttps://open.uns.ac.rs/handle/123456789/5316Title: Combining behavioural types with security analysis
Authors: Bartoletti M.; Castellani I.; Deniélou P.; Dezani-Ciancaglini M.; Gilezan, Silvia; Pantović, Jovanka; Pérez J.; Thiemann P.; Toninho B.; Vieira H.
Abstract: © 2015 Elsevier Inc. 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.
Sun, 01 Nov 2015 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/53162015-11-01T00:00:00Z
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritagehttps://open.uns.ac.rs/handle/123456789/15499Title: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage
Authors: Dougherty D.; Gilezan, Silvia; Lescanne P.
Abstract: We develop an intersection type system for the over(λ, -) μ over(μ, ̃) calculus of Curien and Herbelin. This calculus provides a symmetric computational interpretation of classical sequent style logic and gives a simple account of call-by-name and call-by-value. The present system improves upon earlier type disciplines for over(λ, -) μ over(μ, ̃): in addition to characterizing the over(λ, -) μ over(μ, ̃) expressions that are strongly normalizing under free (unrestricted) reduction, the system enjoys the Subject Reduction and the Subject Expansion properties. © 2008 Elsevier Ltd. All rights reserved.
Wed, 28 May 2008 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/154992008-05-28T00:00:00Z
- Lambda terms for natural deduction, sequent calculus and cut eliminationhttps://open.uns.ac.rs/handle/123456789/14235Title: Lambda terms for natural deduction, sequent calculus and cut elimination
Authors: Barendregt H.; Gilezan, Silvia
Abstract: It is well known that there is an isomorphism between natural deduction derivations and typed lambda terms. Moreover, normalising these terms corresponds to eliminating cuts in the equivalent sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-one map, which causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (λN) and the other to sequent calculus (λL). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a 'cut-free' fragment (λL cf ). This fragment generates exactly the typeable lambda terms in normal form. The cut elimination theorem becomes a simple consequence of the fact that typed lambda terms posses a normal form.
Sat, 01 Jan 2000 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/142352000-01-01T00:00:00Z
- Separating points by parallel hyperplanes-characterization problemhttps://open.uns.ac.rs/handle/123456789/16095Title: Separating points by parallel hyperplanes-characterization problem
Authors: Gilezan, Silvia; Pantović, Jovanka; Žunić J.
Abstract: This paper deals with partitions of a discrete set S of points in a d-dimensional space, by h parallel hyperplanes. Such partitions are in a direct correspondence with multilinear threshold functions which appear in the theory of neural networks and multivalued logic. The characterization (encoding) problem is studied. We show that a unique characterization (encoding) of such multilinear partitions of S = {0, 1,..., m -1}d is possible within O(h · d2 · log m) bit rate per encoded partition. The proposed characterization (code) consists of (d+1) · (h+1) discrete moments having the order no bigger than 1. The obtained bit rate is evaluated depending on the mutual relations between h; d, and m. The optimality is reached in some cases. © 2007 IEEE.
Sat, 01 Sep 2007 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/160952007-09-01T00:00:00Z
- Classical Proofs, Typed Processes, and Intersection Types Extended Abstracthttps://open.uns.ac.rs/handle/123456789/11210Title: Classical Proofs, Typed Processes, and Intersection Types Extended Abstract
Authors: Gilezan, Silvia; Lescanne P.
Abstract: Curien and Herbelin provided a Curry and Howard correspondence between classical prepositional logic and a computational model called λ̄μμμ which is a calculus for interpreting classical sequents. A new terminology for λ̄μμ̄ in terms of pairs of callers-callees which we name capsules enlightens a natural link between λ̄μμ̄ and process calculi. In this paper we propose an intersection type system λ̄μμ̄ which is an extension of λ̄μμ̄ with intersection types. We prove that all strongly normalizing λ̄μμ̄-terms are typeable in the new system, which was not the case in λ̄μμ̃. Also, we prove that all typeable μ̃-free terms are strongly normalizing. © Springer-Verlag 2004.
Wed, 01 Dec 2004 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/112102004-12-01T00:00:00Z
- An approach to call-by-name delimited continuationshttps://open.uns.ac.rs/handle/123456789/12214Title: An approach to call-by-name delimited continuations
Authors: Herbelin H.; Gilezan, Silvia
Abstract: We show that a variant of Parigot's λ;μ-calculus, originally due to de Groote and proved to satisfy Böhm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λ;μ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λ;μ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus. Copyright © 2008 ACM.
Tue, 01 Jan 2008 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/122142008-01-01T00:00:00Z
- Binary relations and algebras on multisetshttps://open.uns.ac.rs/handle/123456789/7547Title: Binary relations and algebras on multisets
Authors: Gilezan, Silvia; Pantović, Jovanka; Vojvodić G.
Abstract: Contrary to the notion of a set or a tuple, a multiset is an unordered collection of elements which do not need to be different. As multisets are already widely used in combinatorics and computer science, the aim of this paper is to get on track to algebraic multiset theory. We consider generalizations of known results that hold for equivalence and order relations on sets and get several properties that are specific to multisets. Furthermore, we exemplify the novelty that brings this concept by showing that multisets are suitable to represent partial orders. Finally, after introducing the notion of an algebra on multisets, we prove that two algebras on multisets, whose root algebras are isomorphic, are in general not isomorphic.
Wed, 01 Jan 2014 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/75472014-01-01T00:00:00Z
- Encoding of multilevel S-threshold functionshttps://open.uns.ac.rs/handle/123456789/5138Title: Encoding of multilevel S-threshold functions
Authors: Pantović, Jovanka; Gilezan, Silvia; Žunić J.
Abstract: © 2016 Old City Publishing, Inc. We consider the encoding problem for the multilevel S-threshold functions. Multilevel S-threshold functions correspond to partitions of a finite-dimensional integer grid into a given finite number of levels, by parallel hypersurfaces. These hypersurfaces are representable as linear combinations of monomials from a predefined set S. We describe and analyze an encoding scheme applicable to all multilevel S-threshold functions, based on the use discrete moments. Even though the proposed encoding scheme is very general, there are situations where it outperforms the existing ones and, as a by product, gives a sharper upper bound for the number of certain threshold functions. Also, several existing encoding schemes, for particular classes of threshold functions, are special cases of this, very general, encoding scheme considered in this paper. Initial results of this paper were presented at the ISMVL 2014, and published in [17].
Fri, 01 Jan 2016 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/51382016-01-01T00:00:00Z
- The “Relevance” of intersection and union typeshttps://open.uns.ac.rs/handle/123456789/11696Title: The “Relevance” of intersection and union types
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia; Venneri B.
Abstract: The aim of this paper is to investigate a Curry-Howard interpretation of the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas of a Hilbert-style logic L, which turns out to be an extension of the intuitionistic logic with respect to provable disjunctive formulas (because of new equivalence relations on formulas), while the implicational-conjunctive fragment of L is still a fragment of intuitionisticlogic. Moreover, typable terms are translated in a typed version, so that ∨-∧-typed combinatory logic terms are proved to completely codify the associated logical proofs. © 1997 by the University of Notre Dame. All rights reserved.
Wed, 01 Jan 1997 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/116961997-01-01T00:00:00Z
- Partitioning finite d-dimensional integer grids with applicationshttps://open.uns.ac.rs/handle/123456789/2574Title: Partitioning finite d-dimensional integer grids with applications
Authors: Gilezan, Silvia; Pantović, Jovanka; Žunić J.
Abstract: © 2007 by Taylor & Francis Group, LLC. In this chapter we will consider partitions of finite d-dimensional integer grids, that is, sets of the form {0, 1, …, m−1}d, by lines in two-dimensional space or by hyperplanes and hypersurfaces in an arbitrary dimension. Different aspects of the problem depending on m, d, and the type of hypersurfaces used have been widely studied in different areas of computer science and mathematics. In this chapter we will focus on problems arising in the areas of digital image processing (analysis) and neural networks. For brevity, related problems arising in other areas of computing (e.g., multivalued logic) and in pure mathematics areas (e.g., group theory) will not be analyzed.
Mon, 01 Jan 2007 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/25742007-01-01T00:00:00Z
- Two behavioural lambda modelshttps://open.uns.ac.rs/handle/123456789/14342Title: Two behavioural lambda models
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia
Abstract: We build two inverse limit lambda models which characterize completely sets of terms having similar computational behaviour. More precisely for each one of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. This is proved by using the finitary logical description of the models obtained by defining suitable intersection type assignment systems. © Springer-Verlag Berlin Heidelberg 2003.
Mon, 01 Dec 2003 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/143422003-12-01T00:00:00Z
- Inhabitation in intersection and union type assignment systemshttps://open.uns.ac.rs/handle/123456789/13540Title: Inhabitation in intersection and union type assignment systems
Authors: Gilezan, Silvia
Abstract: Union does not correspond to intuitionistic disjunction and intersection does not correspond to intuitionistic conjunction. The Curry-Howard isomorphism between types inhabited in the intersection and union type assignment system and formulae provable in intuitionistic propositional logic with implication, conjunction, disjunction and truth does not hold. This is shown semantically. The extension of the simply typed lambda calculus with conjunction and disjunction types and the corresponding elimination and introduction rules is considered. By the Curry-Howard isomorphism types inhabited in this extension of the simply typed lambda calculus correspond to the intuitionistically provable formulae. We shall link the inhabitation in the intersection and union type assignment system with the inhabitation in this extension of the simply typed lambda calculus. © Oxford University Press.
Wed, 01 Dec 1993 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/135401993-12-01T00:00:00Z
- Full intersection types and topologies in lambda calculushttps://open.uns.ac.rs/handle/123456789/15560Title: Full intersection types and topologies in lambda calculus
Authors: Gilezan, Silvia
Abstract: Topologies are introduced on the set of lambda terms by their typeability in the full intersection type assignment system. These topologies give rise to simple proofs of some fundamental results of the lambda calculus such as the continuity theorem and the genericity lemma. We show that application is continuous, unsolvable terms are bottoms, and normal forms are isolated points with respect to these topologies. The restriction of all these topologies to the set of closed lambda terms appears to be unique. We compare the introduced topology with the filter topology on the set of (closed) lambda terms and show that they coincide. © 2001 Academic Press.
Mon, 01 Jan 2001 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/155602001-01-01T00:00:00Z
- Strong normalization and typability with intersection typeshttps://open.uns.ac.rs/handle/123456789/13811Title: Strong normalization and typability with intersection types
Authors: Gilezan, Silvia
Abstract: A simple proof is given of the property that the set of strongly normalizing lambda terms coincides with the set of lambda terms typable in certain intersection type assignment systems. © 1996 by the University of Notre Dame. All rights reserved.
Mon, 01 Jan 1996 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/138111996-01-01T00:00:00Z
- Prefacehttps://open.uns.ac.rs/handle/123456789/9440Title: Preface
Authors: Gilezan, Silvia; Paolini L.
Sat, 01 Dec 2012 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/94402012-12-01T00:00:00Z
- Otvorena nauka: praksa i perspektivehttps://open.uns.ac.rs/handle/123456789/16297Title: Otvorena nauka: praksa i perspektive
Authors: Snežana Smederevac; Dejan Pajić; Sanja Radovanović; Silvia Gilezan; Petar Čolović; Branko Milosavljević
Thu, 02 Apr 2020 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/162972020-04-02T00:00:00Z
- Preciseness of subtyping on intersection and union typeshttps://open.uns.ac.rs/handle/123456789/5562Title: Preciseness of subtyping on intersection and union types
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia
Abstract: 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: denotational and operational. The former 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 latter 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. We propose a technique for formalising and proving operational preciseness of the subtyping relation in the setting of a concurrent lambda calculus with intersection and union types. The key feature is the link between typings and the operational semantics. We then prove soundness and completeness getting that the subtyping relation of this calculus enjoys both denotational and operational preciseness. © 2014 Springer International Publishing Switzerland.
Wed, 01 Jan 2014 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/55622014-01-01T00:00:00Z
- Characterization of strong normalizability for a sequent lambda calculus with co-controlhttps://open.uns.ac.rs/handle/123456789/2892Title: Characterization of strong normalizability for a sequent lambda calculus with co-control
Authors: Santo J.; Gilezan, Silvia
Abstract: © 2017 Copyright held by the owner/author(s). We study strong normalization in a lambda calculus of proof-terms with co-control for the intuitionistic sequent calculus. In this sequent lambda calculus, the management of formulas on the left hand side of typing judgements is "dual" to the management of formulas on the right hand side of the typing judgements in Parigot's lambdamu calculus - that is why our system has first-class "co-control". The characterization of strong normalization is by means of intersection types, and is obtained by analyzing the relationship with another sequent lambda calculus, without co-control, for which a characterization of strong normalizability has been obtained before. The comparison of the two formulations of the sequent calculus, with or without co-control, is of independent interest. Finally, since it is known how to obtain bidirectional natural deduction systems isomorphic to these sequent calculi, characterizations are obtained of the strongly normalizing proof-terms of such natural deduction systems.
Mon, 09 Oct 2017 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/28922017-10-09T00:00:00Z
- On the number of S-threshold functions on not necessarily binary inputhttps://open.uns.ac.rs/handle/123456789/7676Title: On the number of S-threshold functions on not necessarily binary input
Authors: Pantović, Jovanka; Gilezan, Silvia; Žunić J.
Abstract: In this paper we consider S-threshold functions defined on not necessarily binary input. By S-threshold function, in an arbitrary dimension we mean a function which can be written as a linear combination of monomials from a predefined set. First, we determine sets of discrete moments which uniquely determine such functions. Based on these, we derive a generic formula for the upper bound of the functions considered. The formula is generic because it works in all dimensions, on any input size, and for any set of monomials used to define certain S-threshold function. Even though the formula is very generic it gives some improvements of the well-known results. © 2014 IEEE.
Wed, 01 Jan 2014 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/76762014-01-01T00:00:00Z
- Behavioural inverse limit λ-modelshttps://open.uns.ac.rs/handle/123456789/10355Title: Behavioural inverse limit λ-models
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia; Likavec S.
Abstract: We construct two inverse limit λ-models which completely characterise sets of terms with similar computational behaviours: the sets of normalising, head normalising, weak head normalising λ-terms, those corresponding to the persistent versions of these notions, and the sets of closable, closable normalising, and closable head normalising λ-terms. More precisely, for each of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. We use the finitary logical description of the models, obtained by defining suitable intersection type assignment systems, to prove this. © 2004 Elsevier B.V. All rights reserved.
Fri, 28 May 2004 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/103552004-05-28T00:00:00Z
- Application of typed lambda calculi in the untyped lambda calculushttps://open.uns.ac.rs/handle/123456789/10031Title: Application of typed lambda calculi in the untyped lambda calculus
Authors: Gilezan, Silvia
Abstract: © 1994, Springer Verlag. All rights reserved. We discuss some properties of typed lambda calculi which can be related and applyed to the proofs of some properties of the untyped lambda calculus. The strong normalization property of the intersection type assignment system is used in order to prove the finitness of developments property of the untyped lambda calculus in Krivine (1990). Similarly, the strong normalization property of the simply typed lambda calculus can be used for the same reason. Typability in various intersection type assignment systems characterizes tambda terms in normal form, normalizing, solvable and unsolvable terms. Hence, its application in the proof of the Genericity Lemma turns out to be appropriate.
Sat, 01 Jan 1994 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/100311994-01-01T00:00:00Z
- An approach to formal verification of python software transactional memoryhttps://open.uns.ac.rs/handle/123456789/3016Title: An approach to formal verification of python software transactional memory
Authors: Kordić, Branislav; Popović, Miroslav; Gilezan, Silvia; Bašičević, Ilija
Abstract: © 2017 ACM. Although Python is one of the most widely used programming languages, and it is a foundation for a variety of parallel and distributed computing frameworks, it still lacks an applicable and reliable software transactional memory. In this paper, we present an approach to formal verification of a Python Software Transactional Memory (PSTM) solution using UPPAAL tool. The aims are (i) to apply a formal verification process to a real STM implementation in order to derive a faithful STM model based on a PSTM design and (ii) to use developed PSTM model for automated machine-checked formal verification of core system properties such as safety and liveness using a model checker tool. Firstly, an architecture of PSTM solution is introduced. Secondly, formalization and a PSTM system model are analyzed. Finally, core PSTM system's properties are verified, namely safety, liveness, and reachability. Utilizing a UPPAAL's model checker tool it is successfully verified that the PSTM system model satisfies each of the three formerly mentioned properties.
Thu, 31 Aug 2017 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/30162017-08-31T00:00:00Z
- Security types for dynamic web datahttps://open.uns.ac.rs/handle/123456789/16014Title: Security types for dynamic web data
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia; Pantović, Jovanka
Abstract: We describe a type system for the Xdπ calculus, introduced in [8]. An Xdπ-network is a network of locations, where each location consists of both a data tree (which contains scripts and pointers to nodes in trees at different locations) and a process, for modelling process interaction, process migration and interaction between processes and data. Our type system is based on types for locations, trees and processes, expressing security levels. The type system enjoys type preservation under reduction (subject reduction). In consequence of subject reduction we prove the following security properties. In a well-typed Xdπ-network, data in a location are accessible only to processes in locations of equal or higher security level. Moreover, processes originating in a location can only go to locations of equal or less security level, with the exception of movements which are returns to the "source" location. © Springer-Verlag Berlin Heidelberg 2007.
Sat, 01 Dec 2007 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/160142007-12-01T00:00:00Z
- An approach to call-by-name delimited continuationshttps://open.uns.ac.rs/handle/123456789/10904Title: An approach to call-by-name delimited continuations
Authors: Herbelin H.; Gilezan, Silvia
Abstract: We show that a variant of Parigot's λμ-calculus, originally due to de Groote and proved to satisfy Boehm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λμ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λμ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus. © 2008 ACM.
Mon, 01 Dec 2008 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/109042008-12-01T00:00:00Z
- Reducibility: A ubiquitous method in lambda calculus with intersection typeshttps://open.uns.ac.rs/handle/123456789/14047Title: Reducibility: A ubiquitous method in lambda calculus with intersection types
Authors: Gilezan, Silvia; Likavec S.
Abstract: A general reducibility method is developed for proving reduction properties of lambda terms typeable in intersection type systems with and without the universal type Ω. Sufficient conditions for its application are derived. This method leads to uniform proofs of confluence, standardization, weak head normalization of terms typeable in the system with the universal type Ω. The method extends Tait's reducibility method for the proof of strong normalization of the simply typed lambda calculus, Krivine's extension of the same method for the strong normalization of intersection type system without Ω, and Statman-Mitchell's logical relation method for the proof of confluence of β-η-reduction on the simply typed lambda terms. As a consequence, the confluence and the standardization of all (untyped) lambda terms is obtained. © 2002 Published by Elsevier Science B.V.
Sat, 01 Feb 2003 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/140472003-02-01T00:00:00Z
- Characterizing strong normalization in a language with control operatorshttps://open.uns.ac.rs/handle/123456789/11432Title: Characterizing strong normalization in a language with control operators
Authors: Dougherty D.; Gilezan, Silvia; Lescanne P.
Abstract: We investigate some fundamental properties of the reduction relation in the untyped term alculus derived from Curien and Herbelin's λμμ The original λμμ has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic; the significance of the untyped calculus of raw terms is that it is a Turing-complete language for computation with explicit representation of control as well as code. We define a type assignment system for the raw terms satisfying: a term is typable if and only if it is strongly normalizing. The intrinsic symmetry in the λμμ calculus leads to an essential use of both intersection and union types; in contrast to other union-types systems in the literature, our system enjoys the Subject Reduction property.
Thu, 01 Jan 2004 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/114322004-01-01T00:00:00Z
- Strong normalization of the dual classical sequent calculushttps://open.uns.ac.rs/handle/123456789/13898Title: Strong normalization of the dual classical sequent calculus
Authors: Dougherty D.; Gilezan, Silvia; Lescanne P.; Likavec S.
Abstract: We investigate some syntactic properties of Wadler's dual calculus, a term calculus which corresponds to classical sequent logic in the same way that parigot's λμ calculus corresponds to classical natural deduction. Our main result is strong normalization theoren for reduction in the dual calculus; we also prove some confluence results for the typed and untyped versions of the system. © Springer-Verlag Berlin Heidelberg 2005.
Sat, 01 Jan 2005 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/138982005-01-01T00:00:00Z
- Intersection and union types in the λ̄μμ̃-calculushttps://open.uns.ac.rs/handle/123456789/11141Title: Intersection and union types in the λ̄μμ̃-calculus
Authors: Dougherty D.; Gilezan, Silvia; Lescanne P.
Abstract: The original λ̄μμ̃ of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of λ̄μμ̃ with intersection and union types. The intrinsic symmetry in the λ̄μ μ̃ calculus leads to an essential use of both intersection and union types. © 2005 Published by Elsevier B.V.
Tue, 19 Jul 2005 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/111412005-07-19T00:00:00Z
- Confluence of untyped lambda calculus via simple typeshttps://open.uns.ac.rs/handle/123456789/12689Title: Confluence of untyped lambda calculus via simple types
Authors: Gilezan, Silvia; Kunčak V.
Abstract: © Springer-Verlag Berlin Heidelberg 2001. We present a new proof of confluence of the untyped lambda calculus by reducing the confluence of β-reduction in the untyped lambda calculus to the confluence of β-reduction in the simply typed lambda calculus. This is achieved by embedding typed lambda terms into simply typed lambda terms. Using this embedding, an auxiliary reduction, and β-reduction on simply typed lambda terms we define a new reduction on all lambda terms. The transitive closure of the reduction defined is β-reduction on all lambda terms. This embedding allows us to use the confluence of β-reduction on simply typed lambda terms and thus prove the confluence of the reduction defined. As a consequence we obtain the confluence of β-reduction in the untyped lambda calculus.
Mon, 01 Jan 2001 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/126892001-01-01T00:00:00Z
- Types for role-based access control of dynamic web datahttps://open.uns.ac.rs/handle/123456789/15610Title: Types for role-based access control of dynamic web data
Authors: Dezani-Ciancaglini M.; Gilezan, Silvia; Jakšić, Svetlana; Pantović, Jovanka
Abstract: We introduce a role-based access control calculus for modelling dynamic web data and a corresponding type system. It is an extension of the Xdπ calculus proposed by Gardner and Maffeis. In our framework, a network is a parallel composition of locations, where each location contains processes with roles and a data tree whose edges are associated with roles. Processes can communicate, migrate from a location to another, use the data, change the data and the roles in the local tree. In this way, we obtain a model that controls process access to data. We propose a type system which ensures that a specified network policy is respected during computations. Finally, we show that our calculus obeys the following security properties: (1) all data trees and processes with roles in a location agree with the location policy; (2) a process can migrate only to a location with whose policy it agrees; (3) a process with roles can read and modify only data which are accessible to it; (4) a process with roles can enable and disable roles in agreement with the location policy. © 2011 Springer-Verlag.
Wed, 01 Jun 2011 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/156102011-06-01T00:00:00Z
- A typed model for dynamic authorizationshttps://open.uns.ac.rs/handle/123456789/4847Title: A typed model for dynamic authorizations
Authors: Gilezan, Silvia; Jakšić, Svetlana; Pantović, Jovanka; Pérez J.; Vieira H.
Abstract: © Ghilezan, Jakšić, Pantović, Pérez, Vieira. 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 π-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.
Wed, 10 Feb 2016 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/48472016-02-10T00:00:00Z
- Intersection types for the resource control lambda calculihttps://open.uns.ac.rs/handle/123456789/13741Title: Intersection types for the resource control lambda calculi
Authors: Gilezan, Silvia; Ivetić, Jelena; Lescanne P.; Likavec S.
Abstract: We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, λ® and λ®Gtz, respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in λ® by adapting the reducibility method. Then we prove that typability implies strong normalisation in λ®Gtz by using a combination of well-orders and a suitable embedding of λ®Gtz-terms into λ®-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the λ®-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion. © 2011 Springer-Verlag.
Mon, 19 Sep 2011 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/137412011-09-19T00:00:00Z
- Probabilistic reasoning about simply typed lambda termshttps://open.uns.ac.rs/handle/123456789/2204Title: Probabilistic reasoning about simply typed lambda terms
Authors: Gilezan, Silvia; Ivetić, Jelena; Kašterović, Simona; Ognjanović, Zoran; Savić, Nenad
Abstract: © Springer International Publishing AG 2018. Reasoning with uncertainty has gained an important role in computer science, artificial intelligence and cognitive science. These applications urge for development of formal models which capture reasoning of probabilistic features. We propose a formal model for reasoning about probabilities of simply typed lambda terms. We present its syntax, Kripke-style semantics and axiomatic system. The main results are the corresponding soundness and strong completeness, which rely on two key facts: the completeness of simple type assignment and the existence of a maximal consistent extension of a consistent set.
Mon, 01 Jan 2018 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/22042018-01-01T00:00:00Z
- Characterising strongly normalising intuitionistic sequent termshttps://open.uns.ac.rs/handle/123456789/11184Title: Characterising strongly normalising intuitionistic sequent terms
Authors: Espírito Santo J.; Gilezan, Silvia; Ivetić, Jelena
Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. This paper's sequent term calculus integrates smoothly the λ-terms with generalised application or explicit substitution. Strong normalisability of these terms as sequent terms characterises their typeability in certain "natural" typing systems with intersection types. The latter are in the natural deduction format, like systems previously studied by Matthes and Lengrand et al., except that they do not contain any extra, exceptional rules for typing generalised applications or substitution. © 2008 Springer-Verlag Berlin Heidelberg.
Mon, 09 Jun 2008 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/111842008-06-09T00:00:00Z
- Intuitionistic sequent-style calculus with explicit structural ruleshttps://open.uns.ac.rs/handle/123456789/13655Title: Intuitionistic sequent-style calculus with explicit structural rules
Authors: Gilezan, Silvia; Ivetić, Jelena; Lescanne P.; Žunić, D.
Abstract: In this paper we extend the Curry-Howard correspondence to intuitionistic sequent calculus with explicit structural rules of weakening and contraction. We present a linear term calculus derived from the calculus of Espírito Santo, which captures the computational content of the intuitionistic sequent logic, by adding explicit operators for weakening and contraction. For the proposed calculus we introduce the type assignment system with simple types and prove some operational properties, including the subject reduction and strong normalisation property. We then relate the proposed linear type calculus to the simply typed intuitionistic calculus of Kesner and Lengrand, which handles explicit operators of weakening and contraction in the natural deduction framework. © 2011 Springer-Verlag.
Mon, 01 Aug 2011 00:00:00 GMThttps://open.uns.ac.rs/handle/123456789/136552011-08-01T00:00:00Z