Zobrazeno 1 - 10
of 29
pro vyhledávání: '"Pietro Di Gianantonio"'
Autor:
Fabio Alessi, Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, Ivan Scagnetto
Publikováno v:
Journal of Formalized Reasoning, Vol 12, Iss 1, Pp 11-51 (2019)
We develop the metatheory and the implementation of LF+, and discuss several applications. LF+ capitalizes on research work, carried out by the authors over more than a decade, on Logical Frameworks. It builds on various conservative extensions of LF
Externí odkaz:
https://doaj.org/article/bf5a22847c914ec6bcdc44be3cd63e39
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 8-23 (2019)
The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus allowing for external evidence and for postponing, delegating, or fac
Externí odkaz:
https://doaj.org/article/93247161e4974eca8cd1653cb6a5a7a1
Publikováno v:
Logical Methods in Computer Science, Vol Volume 5, Issue 3 (2009)
First, we extend Leifer-Milner RPO theory, by giving general conditions to obtain IPO labelled transition systems (and bisimilarities) with a reduced set of transitions, and possibly finitely branching. Moreover, we study the weak variant of Leifer-M
Externí odkaz:
https://doaj.org/article/29ff092dbcc546a1af64b780f3bb2d42
We investigate, in the context of functional prototype-based lan- guages, a calculus of objects which might extend themselves upon receiving a message, a capability referred to by Cardelli as a self-inflicted operation. We present a sound type system
Externí odkaz:
http://arxiv.org/abs/1808.04190
Session types are a well-established framework for the specification of interactions between components of a distributed systems. An important issue is how to determine the type for an open system, i.e., obtained by assembling subcomponents, some of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::91283ae351221af683214fab75b02bff
https://hdl.handle.net/11390/1233165
https://hdl.handle.net/11390/1233165
Publikováno v:
Formal Aspects of Component Software ISBN: 9783030906351
FACS
FACS
We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its compo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::24b5b44585aa368295db1ec28f277cf6
https://doi.org/10.1007/978-3-030-90636-8_3
https://doi.org/10.1007/978-3-030-90636-8_3
Publikováno v:
LFMTP@LICS
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 8-23 (2019)
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 8-23 (2019)
The Lax Logical Framework, LLFP, was introduced, by a team including the last two authors, to provide a conceptual framework for integrating different proof development tools, thus allowing for external evidence and for postponing, delegating, or fac
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cef204144831c9d2f0523b94c75897eb
http://arxiv.org/abs/1910.10848
http://arxiv.org/abs/1910.10848
Publikováno v:
The Journal of Object Technology. 20:4:1
We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system
Autor:
Pietro Di Gianantonio, Pier Luca Lanzi
Publikováno v:
Politecnico di Milano-IRIS
Autor:
Pietro Di Gianantonio, Abbas Edalat
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642370748
FoSSaCS
FoSSaCS
We introduce a typed lambda calculus in which real numbers, real functions, and in particular continuously differentiable and more generally Lipschitz functions can be defined. Given an expression representing a real-valued function of a real variabl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1acfc0bf2a32baecbe35381841f19cfb
https://doi.org/10.1007/978-3-642-37075-5_22
https://doi.org/10.1007/978-3-642-37075-5_22