Zobrazeno 1 - 10
of 63
pro vyhledávání: '"Pistone, Paolo"'
Since their appearance in the 1950s, computational models capable of performing probabilistic choices have received wide attention and are nowadays pervasive in almost every areas of computer science. Their development was also inextricably linked wi
Externí odkaz:
http://arxiv.org/abs/2409.11999
In this paper we are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalizations of program equivalences. Some of the metrics we are interested in are well-known, such as those based
Externí odkaz:
http://arxiv.org/abs/2302.05022
We introduce a new bounded theory RS^1_2 and show that the functions which are Sigma^b_1-representable in it are precisely random functions which can be computed in polynomial time. Concretely, we pass through a class of oracle functions over string,
Externí odkaz:
http://arxiv.org/abs/2301.12028
We explore the possibility of extending Mardare et al. quantitative algebras to the structures which naturally emerge from Combinatory Logic and the lambda-calculus. First of all, we show that the framework is indeed applicable to those structures, a
Externí odkaz:
http://arxiv.org/abs/2204.13654
We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event lambda-calculus, a vehicle calculus in which both call-by-name and call-by-
Externí odkaz:
http://arxiv.org/abs/2203.11265
Publikováno v:
In Annals of Pure and Applied Logic October-November 2024 175(9)
Autor:
Pistone, Paolo
A central problem in proof-theory is that of finding criteria for identity of proofs, that is, for when two distinct formal derivations can be taken as denoting the same logical argument. In the literature one finds criteria which are either based on
Externí odkaz:
http://arxiv.org/abs/2110.02630
Autor:
Pistone, Paolo
We explore a quantitative interpretation of 2-dimensional intuitionistic type theory (ITT) in which the identity type is interpreted as a "type of differences". We show that a fragment of ITT, that we call difference type theory (dTT), yields a gener
Externí odkaz:
http://arxiv.org/abs/2107.06150
Autor:
Pistone, Paolo, Tranchini, Luca
Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate Syst
Externí odkaz:
http://arxiv.org/abs/2105.00748
Autor:
Pistone, Paolo
Generalized metrics, arising from Lawvere's view of metric spaces as enriched categories, have been widely applied in denotational semantics as a way to measure to which extent two programs behave in a similar, although non equivalent, way. However,
Externí odkaz:
http://arxiv.org/abs/2104.13324