Zobrazeno 1 - 10
of 147
pro vyhledávání: '"Marina Lenisa"'
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:
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
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:
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
Publikováno v:
Fundamenta Informaticae. 134:395-414
Joyal's categorical construction on (well-founded) Conway games and winning strategies provides a compact closed category, where tensor and linear implication are defined via Conway disjunctive sum (in combination with negation for linear implication
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d2804f8a720ce51ef89645faad6cf668
https://doi.org/10.3233/fi-2014-1107
https://doi.org/10.3233/fi-2014-1107
Autor:
Marina Lenisa, Samson Abramsky
Publikováno v:
Computer Science Logic ISBN: 9783540678953
CSL
CSL
We present a linear realizability technique for building Partial Equivalence Relations (PER) categories over Linear Combinatory Algebras. These PER categories turn out to be linear categories and to form an adjoint model with their co-Kleisli categor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f31b208df170f99aee6666cc0174e1e9
https://ora.ox.ac.uk/objects/uuid:441ad179-c2ed-4dea-ae02-15c60583daaa
https://ora.ox.ac.uk/objects/uuid:441ad179-c2ed-4dea-ae02-15c60583daaa
Publikováno v:
Programming Languages and Systems ISBN: 9783319479576
APLAS
APLAS
Set-theoretic paradoxes have made all-inclusive self-referential Foundational Theories almost a taboo. The few daring attempts in the literature to break this taboo avoid paradoxes by restricting the class of formulae allowed in Cantor’s naive Comp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b608ae103a34b67b0ec5edb54441ac2
https://doi.org/10.1007/978-3-319-47958-3_13
https://doi.org/10.1007/978-3-319-47958-3_13
Publikováno v:
Journal of Logic and Computation
Journal of Logic and Computation, 2013, 25 (2), 43 p. ⟨10.1093/logcom/ext028⟩
Journal of Logic and Computation, 2013, 25 (2), 43 p. ⟨10.1093/logcom/ext028⟩
International audience; The LFP Framework is an extension of the Harper-Honsell-Plotkin's Edinburgh Logical Framework LF with external predicates, hence the name Open Logical Framework. This is accomplished by defining lock type constructors, which a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e6324dc8d6c343ae0c8767dfb85fc864
http://hdl.handle.net/11390/1025349
http://hdl.handle.net/11390/1025349