Zobrazeno 1 - 10
of 67
pro vyhledávání: '"Ugo de'Liguoro"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 279, Iss Proc. ICE 2018, Pp 4-20 (2018)
Global-type formalisms enable to describe the overall behaviour of distributed systems and at the same time to enforce safety properties for communications between system components. Our goal is that of amending a weakness of such formalisms: the dif
Externí odkaz:
https://doaj.org/article/563aa74ce42841c8afd7151dae1479fe
Autor:
Franco Barbanera, Ugo de'Liguoro
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 261, Iss Proc. ICE 2017, Pp 17-36 (2017)
In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type operator of
Externí odkaz:
https://doaj.org/article/4c2349ac148f45b79b2347bd40595e9f
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 211, Iss Proc. PLACES 2016, Pp 1-12 (2016)
Multiparty session calculi have been recently equipped with security requirements, in order to guarantee properties such as access control and leak freedom. However, the proposed security requirements seem to be overly restrictive in some cases. In p
Externí odkaz:
https://doaj.org/article/b64dff4262894a6b9e91de916ccfb4ef
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 203, Iss Proc. PLACES 2015, Pp 61-72 (2016)
In calculi for modelling communication protocols, internal and external choices play dual roles. Two external choices can be viewed naturally as dual too, as they represent an agreement between the communicating parties. If the interaction fails, the
Externí odkaz:
https://doaj.org/article/3a942061158747a9a0c8027b527731e9
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
We present a method for synthesizing compositions of mixins using type inhabitation in intersection types. First, recursively defined classes and mixins, which are functions over classes, are expressed as terms in a lambda calculus with records. Inte
Externí odkaz:
https://doaj.org/article/a66a1daef1a248fe9a0629b712ed9b85
Publikováno v:
Logical Methods in Computer Science, Vol Volume 14, Issue 1 (2018)
We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebr
Externí odkaz:
https://doaj.org/article/f0e2faae28ac4d81bb03c3e750291c80
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 189, Iss Proc. ICE 2015, Pp 21-36 (2015)
We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. Devising the notion of orchestrator in such a context makes it possible to have orchestrators with unbounded buffering capabiliti
Externí odkaz:
https://doaj.org/article/d814aad7fb6046ec8a57588235f7589c
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 79-93 (2015)
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally represent mixins
Externí odkaz:
https://doaj.org/article/dcfc56705adf4c97b44b686c6221480d
Autor:
Franco Barbanera, Ugo de'Liguoro
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)
Session contracts is a formalism enabling to investigate client/server interaction protocols and to interpret session types. We extend session contracts in order to represent outputs whose actual sending in an interaction depends on a third party or
Externí odkaz:
https://doaj.org/article/e73c75ef27864c0aae2d0ec75644527a
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 121, Iss Proc. ITRS 2012, Pp 1-17 (2013)
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter and a restricted use of the type omega enable us to represent the par
Externí odkaz:
https://doaj.org/article/714e0d35f1c8439cbf844ad7e369eebf