Zobrazeno 1 - 10
of 16
pro vyhledávání: '"Ines Margaria"'
Autor:
Mario Coppo, Mariangiola Dezani-Ciancaglini, Alejandro Díaz-Caro, Ines Margaria, Maddalena Zacchi
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 242, Iss Proc. ITRS 2016, Pp 31-47 (2017)
This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict inte
Externí odkaz:
https://doaj.org/article/af245f4b426d487faaf1482fac5ae6ef
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 53-64 (2015)
Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the
Externí odkaz:
https://doaj.org/article/f3ed4df4543a425fa82b9a8624266d64
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 121, Iss Proc. ITRS 2012, Pp 58-80 (2013)
This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms a
Externí odkaz:
https://doaj.org/article/b966f6a0e122464ba8183e60f3046c40
Publikováno v:
Mathematical Structures in Computer Science. 27:603-625
This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is we
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b1d3cb52b31af18ea91b56da679b27c9
https://doi.org/10.1017/s0960129515000304
https://doi.org/10.1017/s0960129515000304
Autor:
Maddalena Zacchi, Ines Margaria, Alejandro Díaz-Caro, Mario Coppo, Mariangiola Dezani-Ciancaglini
Publikováno v:
ITRS
Electronic Proceedings in Theoretical Computer Science, Vol 242, Iss Proc. ITRS 2016, Pp 31-47 (2017)
Electronic Proceedings in Theoretical Computer Science, Vol 242, Iss Proc. ITRS 2016, Pp 31-47 (2017)
This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict inte
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a6c6b3c98e7ef17b57ea9ef56cb33d96
http://arxiv.org/abs/1702.02274
http://arxiv.org/abs/1702.02274
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 121, Iss Proc. ITRS 2012, Pp 58-80 (2013)
ITRS
ITRS
This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ec7e5d5ea4e63a0da0554192941eb08a
https://doaj.org/article/b966f6a0e122464ba8183e60f3046c40
https://doaj.org/article/b966f6a0e122464ba8183e60f3046c40
Multiparty sessions describe the interactions among multiple agents in a distributed environment and require essentially two steps: the specification of the communication protocols and the implementation of such protocols as processes. Multiparty ses
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c2a479f63cace4ef7b2d4cb0c8ce7032
http://hdl.handle.net/2318/1577947
http://hdl.handle.net/2318/1577947
Publikováno v:
ITRS
Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 53-64 (2015)
Electronic Proceedings in Theoretical Computer Science, Vol 177, Iss Proc. ITRS 2014, Pp 53-64 (2015)
Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3efa4f2547fbc81183bb089059c4ed0e
http://hdl.handle.net/2318/1522433
http://hdl.handle.net/2318/1522433
Autor:
Maddalena Zacchi, Ines Margaria
Publikováno v:
Theoretical Computer Science. 238:363-387
In this paper, starting from filters which are a natural generalization of intersection filters (Barendregt et al., J. Symbolic Logic 48 (1983) 931–940), the existence of filter models and filter semimodels for the λ -calculus is investigated. The
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::97d28dc6735dda74dbd56c46eb191e9c
https://doi.org/10.1016/s0304-3975(99)00083-3
https://doi.org/10.1016/s0304-3975(99)00083-3
Autor:
Ines Margaria, Maddalena Zacchi
Publikováno v:
Journal of Logic and Computation. 5:367-381
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c6e134c9063828f6b4ac07a54ed8ed4d
https://doi.org/10.1093/logcom/5.3.367
https://doi.org/10.1093/logcom/5.3.367