Zobrazeno 1 - 10
of 52
pro vyhledávání: '"IVAN SCAGNETTO"'
Autor:
Angelo Odetti, Gabriele Bruzzone, Roberta Ferretti, Simona Aracri, Federico Carotenuto, Carolina Vagnoli, Alessandro Zaldei, Ivan Scagnetto
Publikováno v:
Remote Sensing, Vol 16, Iss 11, p 1998 (2024)
This article introduces the Lake Environmental Data Harvester (LED) System, a robotic platform designed for the development of an innovative solution for monitoring remote alpine lakes. LED is intended as the first step in creating portable robotic t
Externí odkaz:
https://doaj.org/article/2065f6664a104bab86316e373dfbb8ee
Autor:
Marco De Piante, Michele Midrio, Roberto Rinaldo, Ivan Scagnetto, Ruben Specogna, Francesco Trevisan
Publikováno v:
Sensors, Vol 24, Iss 8, p 2582 (2024)
This paper focuses on the characterization of radio propagation, and data communication in a marine environment. More specifically, we consider signal propagation when three different sub-gigahertz industrial, scientific, and medical (ISM) bands, i.e
Externí odkaz:
https://doaj.org/article/cc8e695fcd5048698ca4d8761ee75e4b
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 185, Iss Proc. LFMTP 2015, Pp 3-17 (2015)
We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for gluing together diverse Type Theorie
Externí odkaz:
https://doaj.org/article/8e3f193577314bf094c78715c7203a3a
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 3 (2017)
We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establis
Externí odkaz:
https://doaj.org/article/d2e7175eaf0a4b2a993c6cab3345be70
Autor:
Alberto Ciaffaglione, Ivan Scagnetto
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 113, Iss Proc. LSFA 2012, Pp 109-124 (2013)
Capitalizing on previous encodings and formal developments about nominal calculi and type systems, we propose a weak Higher-Order Abstract Syntax formalization of the type language of pure System F
Externí odkaz:
https://doaj.org/article/d2148f2987f048b69f09a16a1f43bf02
Oceanus is a hardware and software platform designed and developed to provide useful information to the crew of a racing yacht. The key features of the proposed solution are its reliability, the possibility to extend and customise it, and its context
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::56c03d31e41af9fa8389c7f8e7a9f84b
http://hdl.handle.net/11390/1204902
http://hdl.handle.net/11390/1204902
Publikováno v:
LPAR
In 2005, S. Abramsky introduced various universal models of computation based on Affine Combinatory Logic, consisting of partial involutions over a suitable formal language of moves, in order to discuss reversible computation in a game-theoretic sett
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fe23874b1a9e145d0e761e81fb964b84
https://doi.org/10.29007/ntwg
https://doi.org/10.29007/ntwg
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Autor:
Ivan Scagnetto, Dale Miller
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 307:1-2
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d813ff12c3159596a93b11e240d05117
https://doi.org/10.4204/eptcs.307.0
https://doi.org/10.4204/eptcs.307.0
Autor:
Ivan Scagnetto, Alberto Ciaffaglione
Publikováno v:
Theoretical Computer Science. 606:57-78
We provide a paradigmatic case study, about the formalization of System F < : 's type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actua
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::0291cf42778f2f205d213cc2f97270cd
https://doi.org/10.1016/j.tcs.2015.07.019
https://doi.org/10.1016/j.tcs.2015.07.019