Zobrazeno 1 - 10
of 44
pro vyhledávání: '"Alberto, Ciaffaglione"'
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
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
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
Autor:
Alberto Ciaffaglione
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 73, Iss Proc. INFINITY 2011, Pp 49-63 (2011)
We exploit (co)inductive specifications and proofs to approach the evaluation of low-level programs for the Unlimited Register Machine (URM) within the Coq system, a proof assistant based on the Calculus of (Co)Inductive Constructions type theory. Ou
Externí odkaz:
https://doaj.org/article/a5f3f18755cb42b0b2c5c95775565e9d
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
Autor:
Alberto Ciaffaglione
Publikováno v:
Science of Computer Programming. 126:31-51
We adopt corecursion and coinduction to formalize Turing Machines and their operational semantics in the Coq proof assistant. By combining the formal analysis of converging and diverging computations, via big-step and small-step predicates, our appro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::906f09e2c6fc73912a2eb4b0ef174a19
https://doi.org/10.1016/j.scico.2016.02.004
https://doi.org/10.1016/j.scico.2016.02.004
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
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
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