Zobrazeno 1 - 10
of 109
pro vyhledávání: '"Furio Honsell"'
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:
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:
Furio Honsell, Marina Lenisa
Publikováno v:
Logical Methods in Computer Science, Vol Volume 7, Issue 3 (2011)
Using coalgebraic methods, we extend Conway's theory of games to possibly non-terminating, i.e. non-wellfounded games (hypergames). We take the view that a play which goes on forever is a draw, and hence rather than focussing on winning strategies, w
Externí odkaz:
https://doaj.org/article/5e770556121642b58320d5d89b20ab46
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
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
Given that today 60% of Internet traffic is generated by bots, ‘CAPTCHA’ (Completely Automated Public Turing Test to tell Computers and Humans Apart) tests that are supposedly impossible to be done by robots have been introduced. What are the cog
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a6260067e92dfbe49ae58df24df2b9c9
http://hdl.handle.net/11577/3296888
http://hdl.handle.net/11577/3296888
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a89d64a0791d2a00184b991db928ab6b
https://doi.org/10.5381/jot.2021.20.2.a4
https://doi.org/10.5381/jot.2021.20.2.a4