Zobrazeno 1 - 10
of 86
pro vyhledávání: '"Scagnetto, Ivan"'
We show that the principal types of the closed terms of the affine fragment of $\lambda$-calculus, with respect to a simple type discipline, are structurally isomorphic to their interpretations, as partial involutions, in a natural Geometry of Intera
Externí odkaz:
http://arxiv.org/abs/2402.07230
Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
Autor:
Miller, Dale, Scagnetto, Ivan
Publikováno v:
EPTCS 307, 2019
This volume contains a selection of papers presented at LFMTP 2019, the 14th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on June 22, 2019, in Vancouver, Canada. The workshop was affiliated with t
Externí odkaz:
http://arxiv.org/abs/1910.08712
Mobile Information Retrieval (Mobile IR) is a relatively recent branch of Information Retrieval (IR) that is concerned with enabling users to carry out, using a mobile device, all the classical IR operations that they were used to carry out on a desk
Externí odkaz:
http://arxiv.org/abs/1902.01790
Autor:
Cecchinato, Niccolò1 (AUTHOR), Scagnetto, Ivan1 (AUTHOR) ivan.scagnetto@uniud.it, Toma, Andrea1 (AUTHOR), Drioli, Carlo1 (AUTHOR), Foresti, Gian Luca1 (AUTHOR)
Publikováno v:
Integrated Computer-Aided Engineering. 2024, Vol. 31 Issue 1, p59-75. 17p.
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong pr
Externí odkaz:
http://arxiv.org/abs/1808.04193
In 2005, Abramsky introduced various linear/affine combinatory algebras of partial involutions over a suitable formal language, to discuss reversible computation in a game-theoretic setting. These algebras arise as instances of the general paradigm e
Externí odkaz:
http://arxiv.org/abs/1806.06759
Publikováno v:
Logical Methods in Computer Science, Volume 13, Issue 3 (July 6, 2017) lmcs:3771
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:
http://arxiv.org/abs/1702.07214
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
EPTCS 185, 2015, pp. 3-17
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:
http://arxiv.org/abs/1507.08051